- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat.cpp

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00009 // Organization:        Model-based Embedded and Robotic Systems Group
    00010 //                                      Massachusetts Institute of Technology
    00011 //
    00013 //# CHECKED MJP 08-07-2002
    00014
    00015 #ifdef _MSC_VER
    00016 #pragma warning( disable : 4786 )
    00017 #endif
    00018
    00019 #include "Opsat.h"
    00020
    00021 #include <cassert>
    00022
    00023 #include <Mers/Generators/AssignmentGeneratorInterface.h>
    00024
    00025 #include <Mers/Generators/BFIG/BFIGGenerator.h>
    00026 #include <Mers/Generators/BFIG/CDBFIG/CDBFIGFactory.h>
    00027 #include <Mers/Generators/BFIG/BFIGObjectiveFunction.h>
    00028 #include <Mers/Solvers/SAT/ISAT/ISATTester.h>
    00029
    00030 #include <Mers/Models/CCA/CCAModel.h>
    00031
    00032 #include <Mers/Utils/Containers/IntegerArray.h>
    00033
    00035
    00036 using namespace Mers::Solvers::SAT::GATSAT::OpSAT;
    00037 using Mers::Generators::AssignmentGeneratorInterface;
    00038 using Mers::Generators::BFIG::BFIGGenerator;
    00039 using Mers::Generators::BFIG::CDBFIG::CDBFIGFactory;
    00040 using Mers::Generators::BFIG::BFIGObjectiveFunction;
    00041 using Mers::Solvers::SAT::AssignmentTesterInterface;
    00042 using Mers::Solvers::SAT::ISAT::ISATTester;
    00043 using Mers::Models::CCA::CCAVariables;
    00044 using Mers::Models::CCA::CCAModel;
    00045 using Mers::Models::Base::BaseModelVariableArray;
    00046 using Mers::Models::Base::BaseModelVariable;
    00047 using Mers::Models::Base::BaseModelDomain;
    00048 using Mers::Models::Base::BaseModelAssignmentArray;
    00049 using Mers::Models::Base::BaseModelSentence;
    00050 using Mers::Models::Base::BaseModelClause;
    00051 using Mers::Utils::Containers::IntegerArray;
    00052 using std::ostream;
    00053 using std::endl;
    00054 using std::cerr;
    00055 using std::vector;
    00056 using std::flush;
    00057
    00059
    00060 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00061                         BFIGObjectiveFunction const * ocspObjectiveFunction,
    00062                         BaseModelVariableArray const & allVariables,
    00063                         BaseModelSentence const & constraintSet,
    00064                         bool use_dpll, double cutoffCost)
    00065 {
    00066         noExpand = false;
    00067
    00068         createBFIG(designVariables, ocspObjectiveFunction, allVariables, cutoffCost);
    00069
    00070         ISATTester * itTester = new ISATTester(allVariables, designVariables, constraintSet);
    00071         itTester->setDPLLFlag(use_dpll);
    00072         tester = itTester;
    00073 }
    00074
    00076
    00077 Opsat::Opsat(CCAVariables const & designVariables,
    00078         CCAModel const & model, bool use_dpll, double cutoffCost)
    00079 {
    00080         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00081         noExpand = false;
    00082
    00083         createBFIG(designVariables, model, cutoffCost);
    00084
    00085         //cerr << "Initializing ISAT Tester..." << endl;
    00086         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00087         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00088         itTester->setDPLLFlag(use_dpll);
    00089         tester = itTester;
    00090 }
    00091
    00093
    00094 Opsat::Opsat(CCAVariables const & designVariables,
    00095         CCAModel const & model, bool use_dpll)
    00096 {
    00097         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00098         noExpand = false;
    00099
    00100         createBFIG(designVariables, model);
    00101
    00102         //cerr << "Initializing ISAT Tester..." << endl;
    00103         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00104         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00105         itTester->setDPLLFlag(use_dpll);
    00106         tester = itTester;
    00107 }
    00108
    00110
    00111 Opsat::Opsat(CCAVariables const & designVariables,
    00112         CCAModel const & model, BaseModelSentence const & constraintSet,
    00113         bool use_dpll, double cutoffCost)
    00114 {
    00115         noExpand = false;
    00116         createBFIG(designVariables, model, cutoffCost);
    00117
    00118         //cerr << "Initializing ISAT Tester..." << endl;
    00119         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00120         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00121         itTester->setDPLLFlag(use_dpll);
    00122         tester = itTester;
    00123 }
    00124
    00126
    00127 Opsat::Opsat(CCAVariables const & designVariables,
    00128         CCAModel const & model, BaseModelSentence const & constraintSet,
    00129         bool use_dpll)
    00130 {
    00131         noExpand = false;
    00132         createBFIG(designVariables, model);
    00133
    00134         //cerr << "Initializing ISAT Tester..." << endl;
    00135         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00136         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00137         itTester->setDPLLFlag(use_dpll);
    00138         tester = itTester;
    00139 }
    00140
    00142
    00143 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00144         IntegerArray const &valueMap,
    00145         vector<double> const & designVarProbs,
    00146         BaseModelVariableArray const & allVariables,
    00147         BaseModelSentence const & constraintSet,
    00148         bool use_dpll, double cutoffCost)
    00149 {
    00150         noExpand = false;
    00151
    00152         createBFIG(designVariables, allVariables, valueMap,
    00153                 designVarProbs, cutoffCost);
    00154
    00155         //cerr << "Initializing ISAT Tester..." << endl;
    00156         ISATTester * itTester = new ISATTester(allVariables, designVariables, constraintSet);
    00157         itTester->setDPLLFlag(use_dpll);
    00158         tester = itTester;
    00159 }
    00160
    00162
    00163 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00164         IntegerArray const &valueMap,
    00165         vector<double> const & designVarProbs,
    00166         BaseModelVariableArray const & allVariables,
    00167         BaseModelSentence const & constraintSet,
    00168         bool use_dpll)
    00169 {
    00170         noExpand = false;
    00171
    00172         createBFIG(designVariables, allVariables, valueMap,
    00173                 designVarProbs);
    00174
    00175         //cerr << "Initializing ISAT Tester..." << endl;
    00176         ISATTester * itTester = new ISATTester(allVariables, designVariables, constraintSet);
    00177         itTester->setDPLLFlag(use_dpll);
    00178         tester = itTester;
    00179 }
    00180
    00182
    00183 /*#
    00184 //Opsat::Opsat(list<Variable const *> designVariables,
    00185 //             list<Variable const *> stateVariables,
    00186 //             list<Constraint const *> baseConstraintSet,
    00187 //             list<Constraint const *> satConstraintSet,
    00188 //             list<Constraint const *> unsatConstraintSet,
    00189 //             bool use_dpll, bool use_cd)
    00190 //{
    00191 //      init(designVariables, stateVariables, baseConstraintSet,
    00192 //           satConstraintSet, unsatConstraintSet);
    00193 //      useDPLL(use_dpll);
    00194 //      useCD(use_cd);
    00195 //      debug = false;
    00196 //}
    00197 */
    00198
    00200
    00201 Opsat::Opsat(BaseModelVariableArray const & variableSet,
    00202         IntegerArray const &valueMap,
    00203         vector<double> const & designVarProbs,
    00204         BaseModelSentence const & constraintSet, double cutoffCost)
    00205 {
    00206         noExpand = false;
    00207
    00208         createBFIG(variableSet, variableSet, valueMap,
    00209                 designVarProbs, cutoffCost);
    00210
    00211         //cerr << "Initializing ISAT Tester..." << endl;
    00212         ISATTester * itTester = new ISATTester(variableSet, variableSet, constraintSet);
    00213         itTester->setDPLLFlag(true);
    00214         tester = itTester;
    00215 }
    00216
    00218
    00219 Opsat::Opsat(BaseModelVariableArray const & variableSet,
    00220         IntegerArray const &valueMap,
    00221         vector<double> const & designVarProbs,
    00222         BaseModelSentence const & constraintSet)
    00223 {
    00224         noExpand = false;
    00225
    00226         createBFIG(variableSet, variableSet, valueMap,
    00227                 designVarProbs);
    00228
    00229         //cerr << "Initializing ISAT Tester..." << endl;
    00230         ISATTester * itTester = new ISATTester(variableSet, variableSet, constraintSet);
    00231         itTester->setDPLLFlag(true);
    00232         tester = itTester;
    00233 }
    00234
    00236
    00237 Opsat::Opsat(AssignmentGeneratorInterface * myGenerator, BaseModelVariableArray const & searchVariables,
    00238         BaseModelVariableArray const & allVariables,
    00239         BaseModelSentence const & constraintSet, bool use_dpll)
    00240 {
    00241         debug = false;
    00242         noExpand = false;
    00243
    00244         generator = myGenerator;
    00245
    00246         //cerr << "Initializing ISAT Tester..." << endl;
    00247         ISATTester * itTester = new ISATTester(allVariables, searchVariables, constraintSet);
    00248         itTester->setDPLLFlag(use_dpll);
    00249         tester = itTester;
    00250 }
    00251
    00253
    00254 Opsat::~Opsat()
    00255 {
    00256 }
    00257
    00259
    00260 void
    00261 Opsat::skipExpanding(bool skip)
    00262 {
    00263       noExpand = skip;
    00264 }
    00265
    00267
    00268 void
    00269 Opsat::setTemporaryConstraint(BaseModelClause const * c)
    00270 {
    00271         assert(c);
    00272         tester->setTemporaryConstraint(c);
    00273 }
    00274
    00276
    00277 void
    00278 Opsat::addConstraint(BaseModelClause const * c)
    00279 {
    00280         assert(c);
    00281         tester->addConstraint(c);
    00283 }
    00284
    00286
    00287 void
    00288 Opsat::constrainByReachability()
    00289 {
    00290         //tester->constrainByReachability();
    00291 }
    00292
    00294
    00295 void
    00296 Opsat::constrainByNextState()
    00297 {
    00298         //tester->constrainByNextValue();
    00299 }
    00300
    00302
    00303 void
    00304 Opsat::clearTemporaryConstraint()
    00305 {
    00306         tester->clearTemporaryConstraint();
    00307 }
    00308
    00310
    00311 void Opsat::testTheory()
    00312 {
    00313         BaseModelAssignmentArray conflict(false);
    00314         cerr << "Theory is " << flush;
    00315         AssignmentTesterInterface::SolutionType consistent =
    00316                 tester->tryAssignment(NULL, 0, true, conflict);
    00317         switch(consistent){
    00318         case AssignmentTesterInterface::Valid:
    00319                 cerr << "Valid";
    00320                 break;
    00321         case AssignmentTesterInterface::Satisfiable:
    00322                 cerr << "Satisfiable";
    00323                 break;
    00324         case AssignmentTesterInterface::Unsatisfiable:
    00325                 cerr << "Unsatisfiable";
    00326                 break;
    00327         };
    00328         cerr << endl;
    00329 }
    00330
    00332
    00333 #ifndef EMBEDDED
    00334
    00335 ostream & Mers::Solvers::SAT::GATSAT::OpSAT::operator <<(ostream & out, Opsat const & other)
    00336 {
    00337         out << "Opsat:" << endl;
    00338         //other.generator->print(out);
    00339         //other.tester->print(out);
    00340         return out;
    00341 }
    00342
    00343 #endif
    00344
    00346
    00347 void
    00348 Opsat::createBFIG(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00349                 Mers::Generators::BFIG::BFIGObjectiveFunction const * ocspObjectiveFunction,
    00350                 Mers::Models::Base::BaseModelVariableArray const &allVariables,
    00351                 double cutoffCost)
    00352 {
    00353         CDBFIGFactory factory;
    00354         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00355                 ocspObjectiveFunction, allVariables, cutoffCost);
    00356         generator = agGen;
    00357 }
    00358
    00360
    00361 void Opsat::createBFIG(CCAVariables const & designVariables,
    00362         CCAModel const & model, double cutoffCost)
    00363 {
    00364         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00365         IntegerArray valueMap;
    00366         vector<double> probs;
    00367
    00368         int probIndex = 0;
    00369         unsigned int varIndex;
    00370         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00371                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00372                 // Assign a uniform probability.
    00373                 double prob = 1.0 / var.getDomain()->getLength();
    00374                 BaseModelDomain const &dom = *(var.getDomain());
    00375                 valueMap.pushBack(probIndex);
    00376                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00377                         probs.push_back(prob);
    00378                         probIndex++;
    00379                 }
    00380         }
    00381
    00382         createBFIG(designVariables, variablesAll, valueMap, probs, cutoffCost);
    00383 }
    00384
    00386
    00387 void Opsat::createBFIG(CCAVariables const & designVariables,
    00388         CCAModel const & model)
    00389 {
    00390         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00391         IntegerArray valueMap;
    00392         vector<double> probs;
    00393
    00394         int probIndex = 0;
    00395         unsigned int varIndex;
    00396         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00397                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00398                 // Assign a uniform probability.
    00399                 double prob = 1.0 / var.getDomain()->getLength();
    00400                 BaseModelDomain const &dom = *(var.getDomain());
    00401                 valueMap.pushBack(probIndex);
    00402                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00403                         probs.push_back(prob);
    00404                         probIndex++;
    00405                 }
    00406         }
    00407
    00408         createBFIG(designVariables, variablesAll, valueMap, probs);
    00409 }
    00410
    00412
    00413 void Opsat::createBFIG(BaseModelVariableArray const & designVariables,
    00414         BaseModelVariableArray const &allVariables,
    00415         IntegerArray const &valueMap, vector<double> const & probabilities,
    00416         double cutoffCost)
    00417 {
    00418         CDBFIGFactory factory;
    00419         //cerr << "Initializing BFIG Generator..." << endl;
    00420         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00421                 allVariables, valueMap, probabilities, cutoffCost);
    00422         generator = agGen;
    00423 }
    00424
    00426
    00427 void Opsat::createBFIG(BaseModelVariableArray const & designVariables,
    00428         BaseModelVariableArray const &allVariables,
    00429         IntegerArray const &valueMap, vector<double> const & probabilities)
    00430 {
    00431         CDBFIGFactory factory;
    00432         //cerr << "Initializing BFIG Generator..." << endl;
    00433         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00434                 allVariables, valueMap, probabilities);
    00435         generator = agGen;
    00436 }
    00437
    00439