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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat-for-zchaff.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 #include <Mers/Solvers/SAT/ZChaff/ZChaffTester.h> //xx
    00030
    00031 #include <Mers/Models/CCA/CCAModel.h>
    00032
    00033 #include <Mers/Utils/Containers/IntegerArray.h>
    00034
    00036
    00037 using namespace Mers::Solvers::SAT::GATSAT::OpSAT;
    00038 using Mers::Generators::AssignmentGeneratorInterface;
    00039 using Mers::Generators::BFIG::BFIGGenerator;
    00040 using Mers::Generators::BFIG::CDBFIG::CDBFIGFactory;
    00041 using Mers::Generators::BFIG::BFIGObjectiveFunction;
    00042 using Mers::Solvers::SAT::AssignmentTesterInterface;
    00043 using Mers::Solvers::SAT::ISAT::ISATTester;
    00044 using Mers::Solvers::SAT::ZChaff::ZChaffTester;  //xx
    00045 //using 3rdparty::zChaff; //xx
    00046 using Mers::Models::CCA::CCAVariables;
    00047 using Mers::Models::CCA::CCAModel;
    00048 using Mers::Models::Base::BaseModelVariableArray;
    00049 using Mers::Models::Base::BaseModelVariable;
    00050 using Mers::Models::Base::BaseModelDomain;
    00051 using Mers::Models::Base::BaseModelAssignmentArray;
    00052 using Mers::Models::Base::BaseModelSentence;
    00053 using Mers::Models::Base::BaseModelClause;
    00054 using Mers::Utils::Containers::IntegerArray;
    00055 using std::ostream;
    00056 using std::endl;
    00057 using std::cerr;
    00058 using std::vector;
    00059 using std::flush;
    00060
    00062
    00063 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00064                         BFIGObjectiveFunction const * ocspObjectiveFunction,
    00065                         BaseModelVariableArray const & allVariables,
    00066                         BaseModelSentence const & constraintSet,
    00067                         bool use_dpll, double cutoffCost)
    00068 {
    00069         noExpand = false;
    00070
    00071         createBFIG(designVariables, ocspObjectiveFunction, allVariables, cutoffCost);
    00072
    00073         ISATTester * itTester = new ISATTester(allVariables, designVariables, constraintSet);
    00074         itTester->setDPLLFlag(use_dpll);
    00075         tester = itTester;
    00076
    00077         cerr << "*****Opsat 1" << endl; //xx
    00078 }
    00079
    00081
    00082 Opsat::Opsat(CCAVariables const & designVariables,
    00083         CCAModel const & model, bool use_dpll, double cutoffCost)
    00084 {
    00085         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00086         noExpand = false;
    00087
    00088         createBFIG(designVariables, model, cutoffCost);
    00089
    00090         //cerr << "Initializing ISAT Tester..." << endl;
    00091         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00092         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00093         itTester->setDPLLFlag(use_dpll);
    00094         tester = itTester;
    00095
    00096         cerr << "*****Opsat 2" << endl; //xx
    00097 }
    00098
    00100
    00101 Opsat::Opsat(CCAVariables const & designVariables,
    00102         CCAModel const & model, bool use_dpll)
    00103 {
    00104         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00105         noExpand = false;
    00106
    00107         createBFIG(designVariables, model);
    00108
    00109         //cerr << "Initializing ISAT Tester..." << endl;
    00110         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00111         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00112         itTester->setDPLLFlag(use_dpll);
    00113         tester = itTester;
    00114
    00115         cerr << "*****Opsat 3" << endl; //xx
    00116 }
    00117
    00119
    00120 Opsat::Opsat(CCAVariables const & designVariables,
    00121         CCAModel const & model, BaseModelSentence const & constraintSet,
    00122         bool use_dpll, double cutoffCost)
    00123 {
    00124         noExpand = false;
    00125         createBFIG(designVariables, model, cutoffCost);
    00126
    00127         //cerr << "Initializing ISAT Tester..." << endl;
    00128         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00129         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00130         itTester->setDPLLFlag(use_dpll);
    00131         tester = itTester;
    00132
    00133         cerr << "*****Opsat 4" << endl; //xx
    00134 }
    00135
    00137
    00138 Opsat::Opsat(CCAVariables const & designVariables,
    00139         CCAModel const & model, BaseModelSentence const & constraintSet,
    00140         bool use_dpll)
    00141 {
    00142         noExpand = false;
    00143         createBFIG(designVariables, model);
    00144
    00145         //cerr << "Initializing ISAT Tester..." << endl;
    00146         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00147         ISATTester * itTester = new ISATTester(variablesAll, designVariables, constraintSet);
    00148         itTester->setDPLLFlag(use_dpll);
    00149         tester = itTester;
    00150
    00151         cerr << "*****Opsat 5" << endl; //xx
    00152 }
    00153
    00155
    00156 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00157         IntegerArray const &valueMap,
    00158         vector<double> const & designVarProbs,
    00159         BaseModelVariableArray const & allVariables,
    00160         BaseModelSentence const & constraintSet,
    00161         bool use_dpll, double cutoffCost)
    00162 {
    00163         noExpand = false;
    00164
    00165         createBFIG(designVariables, allVariables, valueMap,
    00166                 designVarProbs, cutoffCost);
    00167
    00168         //cerr << "Initializing ISAT Tester..." << endl;
    00169         ISATTester * itTester = new ISATTester(allVariables, designVariables, constraintSet);
    00170         itTester->setDPLLFlag(use_dpll);
    00171         tester = itTester;
    00172
    00173         cerr << "*****Opsat 6" << endl; //xx
    00174 }
    00175
    00177
    00178 Opsat::Opsat(BaseModelVariableArray const & designVariables,
    00179         IntegerArray const &valueMap,
    00180         vector<double> const & designVarProbs,
    00181         BaseModelVariableArray const & allVariables,
    00182         BaseModelSentence const & constraintSet,
    00183         bool use_dpll)
    00184 {
    00185         noExpand = false;
    00186
    00187         createBFIG(designVariables, allVariables, valueMap,
    00188                 designVarProbs);
    00189
    00190         //cerr << "Initializing ISAT Tester..." << endl;
    00191         ZChaffTester * itTester = new ZChaffTester(allVariables, designVariables, constraintSet); //xx
    00192         //itTester->setDPLLFlag(true);
    00193         tester = itTester;
    00194
    00195         cerr << "*****Opsat 7" << endl; //xx
    00196 }
    00197
    00199
    00200 /*#
    00201 //Opsat::Opsat(list<Variable const *> designVariables,
    00202 //             list<Variable const *> stateVariables,
    00203 //             list<Constraint const *> baseConstraintSet,
    00204 //             list<Constraint const *> satConstraintSet,
    00205 //             list<Constraint const *> unsatConstraintSet,
    00206 //             bool use_dpll, bool use_cd)
    00207 //{
    00208 //      init(designVariables, stateVariables, baseConstraintSet,
    00209 //           satConstraintSet, unsatConstraintSet);
    00210 //      useDPLL(use_dpll);
    00211 //      useCD(use_cd);
    00212 //      debug = false;
    00213 //}
    00214 */
    00215
    00217
    00218 Opsat::Opsat(BaseModelVariableArray const & variableSet,
    00219         IntegerArray const &valueMap,
    00220         vector<double> const & designVarProbs,
    00221         BaseModelSentence const & constraintSet, double cutoffCost)
    00222 {
    00223         noExpand = false;
    00224
    00225         createBFIG(variableSet, variableSet, valueMap,
    00226                 designVarProbs, cutoffCost);
    00227
    00228         //cerr << "Initializing ISAT Tester..." << endl;
    00229         ISATTester * itTester = new ISATTester(variableSet, variableSet, constraintSet);
    00230         itTester->setDPLLFlag(true);
    00231         tester = itTester;
    00232
    00233         cerr << "*****Opsat 8" << endl; //xx
    00234 }
    00235
    00237
    00238 Opsat::Opsat(BaseModelVariableArray const & variableSet,
    00239         IntegerArray const &valueMap,
    00240         vector<double> const & designVarProbs,
    00241         BaseModelSentence const & constraintSet)
    00242 {
    00243         noExpand = false;
    00244
    00245         createBFIG(variableSet, variableSet, valueMap,
    00246                 designVarProbs);
    00247
    00248         //cerr << "Initializing ISAT Tester..." << endl;
    00249         ISATTester * itTester = new ISATTester(variableSet, variableSet, constraintSet);
    00250         itTester->setDPLLFlag(true);
    00251         tester = itTester;
    00252
    00253         cerr << "*****Opsat 9" << endl; //xx
    00254 }
    00255
    00257
    00258 Opsat::Opsat(AssignmentGeneratorInterface * myGenerator, BaseModelVariableArray const & searchVariables,
    00259         BaseModelVariableArray const & allVariables,
    00260         BaseModelSentence const & constraintSet, bool use_dpll)
    00261 {
    00262         debug = false;
    00263         noExpand = false;
    00264
    00265         generator = myGenerator;
    00266
    00267         //cerr << "Initializing ISAT Tester..." << endl;
    00268         ISATTester * itTester = new ISATTester(allVariables, searchVariables, constraintSet);
    00269         itTester->setDPLLFlag(use_dpll);
    00270         tester = itTester;
    00271
    00272         cerr << "*****Opsat 10" << endl; //xx
    00273 }
    00274
    00276
    00277 Opsat::~Opsat()
    00278 {
    00279 }
    00280
    00282
    00283 void
    00284 Opsat::skipExpanding(bool skip)
    00285 {
    00286       noExpand = skip;
    00287 }
    00288
    00290
    00291 void
    00292 Opsat::setTemporaryConstraint(BaseModelClause const * c)
    00293 {
    00294         assert(c);
    00295         tester->setTemporaryConstraint(c);
    00296 }
    00297
    00299
    00300 void
    00301 Opsat::addConstraint(BaseModelClause const * c)
    00302 {
    00303         assert(c);
    00304         tester->addConstraint(c);
    00306 }
    00307
    00309
    00310 void
    00311 Opsat::constrainByReachability()
    00312 {
    00313         //tester->constrainByReachability();
    00314 }
    00315
    00317
    00318 void
    00319 Opsat::constrainByNextState()
    00320 {
    00321         //tester->constrainByNextValue();
    00322 }
    00323
    00325
    00326 void
    00327 Opsat::clearTemporaryConstraint()
    00328 {
    00329         tester->clearTemporaryConstraint();
    00330 }
    00331
    00333
    00334 void Opsat::testTheory()
    00335 {
    00336         BaseModelAssignmentArray conflict(false);
    00337         cerr << "Theory is " << flush;
    00338         AssignmentTesterInterface::SolutionType consistent =
    00339                 tester->tryAssignment(NULL, 0, true, conflict);
    00340         switch(consistent){
    00341         case AssignmentTesterInterface::Valid:
    00342                 cerr << "Valid";
    00343                 break;
    00344         case AssignmentTesterInterface::Satisfiable:
    00345                 cerr << "Satisfiable";
    00346                 break;
    00347         case AssignmentTesterInterface::Unsatisfiable:
    00348                 cerr << "Unsatisfiable";
    00349                 break;
    00350         };
    00351         cerr << endl;
    00352 }
    00353
    00355
    00356 #ifndef EMBEDDED
    00357
    00358 ostream & Mers::Solvers::SAT::GATSAT::OpSAT::operator <<(ostream & out, Opsat const & other)
    00359 {
    00360         out << "Opsat:" << endl;
    00361         //other.generator->print(out);
    00362         //other.tester->print(out);
    00363         return out;
    00364 }
    00365
    00366 #endif
    00367
    00369
    00370 void
    00371 Opsat::createBFIG(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00372                 Mers::Generators::BFIG::BFIGObjectiveFunction const * ocspObjectiveFunction,
    00373                 Mers::Models::Base::BaseModelVariableArray const &allVariables,
    00374                 double cutoffCost)
    00375 {
    00376         CDBFIGFactory factory;
    00377         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00378                 ocspObjectiveFunction, allVariables, cutoffCost);
    00379         generator = agGen;
    00380 }
    00381
    00383
    00384 void Opsat::createBFIG(CCAVariables const & designVariables,
    00385         CCAModel const & model, double cutoffCost)
    00386 {
    00387         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00388         IntegerArray valueMap;
    00389         vector<double> probs;
    00390
    00391         int probIndex = 0;
    00392         unsigned int varIndex;
    00393         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00394                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00395                 // Assign a uniform probability.
    00396                 double prob = 1.0 / var.getDomain()->getLength();
    00397                 BaseModelDomain const &dom = *(var.getDomain());
    00398                 valueMap.pushBack(probIndex);
    00399                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00400                         probs.push_back(prob);
    00401                         probIndex++;
    00402                 }
    00403         }
    00404
    00405         createBFIG(designVariables, variablesAll, valueMap, probs, cutoffCost);
    00406 }
    00407
    00409
    00410 void Opsat::createBFIG(CCAVariables const & designVariables,
    00411         CCAModel const & model)
    00412 {
    00413         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00414         IntegerArray valueMap;
    00415         vector<double> probs;
    00416
    00417         int probIndex = 0;
    00418         unsigned int varIndex;
    00419         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00420                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00421                 // Assign a uniform probability.
    00422                 double prob = 1.0 / var.getDomain()->getLength();
    00423                 BaseModelDomain const &dom = *(var.getDomain());
    00424                 valueMap.pushBack(probIndex);
    00425                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00426                         probs.push_back(prob);
    00427                         probIndex++;
    00428                 }
    00429         }
    00430
    00431         createBFIG(designVariables, variablesAll, valueMap, probs);
    00432 }
    00433
    00435
    00436 void Opsat::createBFIG(BaseModelVariableArray const & designVariables,
    00437         BaseModelVariableArray const &allVariables,
    00438         IntegerArray const &valueMap, vector<double> const & probabilities,
    00439         double cutoffCost)
    00440 {
    00441         CDBFIGFactory factory;
    00442         //cerr << "Initializing BFIG Generator..." << endl;
    00443         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00444                 allVariables, valueMap, probabilities, cutoffCost);
    00445         generator = agGen;
    00446 }
    00447
    00449
    00450 void Opsat::createBFIG(BaseModelVariableArray const & designVariables,
    00451         BaseModelVariableArray const &allVariables,
    00452         IntegerArray const &valueMap, vector<double> const & probabilities)
    00453 {
    00454         CDBFIGFactory factory;
    00455         //cerr << "Initializing BFIG Generator..." << endl;
    00456         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00457                 allVariables, valueMap, probabilities);
    00458         generator = agGen;
    00459 }
    00460
    00462