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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/VsatBfig/VsatBfig.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 //
    00010 //# CHECKED MJP 08-07-2002
    00011
    00012 #ifdef _MSC_VER
    00013 #pragma warning( disable : 4786 )
    00014 #endif
    00015
    00016 #include "VsatBfig.h"
    00017
    00018 #include <cassert>
    00019
    00020 #include <Mers/Generators/AssignmentGeneratorInterface.h>
    00021
    00022 #include <Mers/Generators/BFIG/BFIGGenerator.h>
    00023 #include <Mers/Generators/BFIG/CDBFIG/CDBFIGFactory.h>
    00024 #include <Mers/Solvers/SAT/ValidSAT/ValidSAT.h>
    00025
    00026 #include <Mers/Models/CCA/CCAModel.h>
    00027
    00028 #include <Mers/Utils/Containers/IntegerArray.h>
    00029
    00031
    00032 using namespace Mers::Solvers::SAT::GATSAT::VsatBfig;
    00033 using Mers::Generators::AssignmentGeneratorInterface;
    00034 using Mers::Generators::BFIG::BFIGGenerator;
    00035 using Mers::Generators::BFIG::CDBFIG::CDBFIGFactory;
    00036 using Mers::Solvers::SAT::AssignmentTesterInterface;
    00037 using Mers::Solvers::SAT::ValidSAT::ValidSAT;
    00038 using Mers::Models::CCA::CCAVariables;
    00039 using Mers::Models::CCA::CCAModel;
    00040 using Mers::Models::Base::BaseModelVariableArray;
    00041 using Mers::Models::Base::BaseModelVariable;
    00042 using Mers::Models::Base::BaseModelDomain;
    00043 using Mers::Models::Base::BaseModelAssignmentArray;
    00044 using Mers::Models::Base::BaseModelSentence;
    00045 using Mers::Models::Base::BaseModelClause;
    00046 using Mers::Utils::Containers::IntegerArray;
    00047 using std::ostream;
    00048 using std::endl;
    00049 using std::cerr;
    00050 using std::vector;
    00051 using std::flush;
    00052
    00054
    00055 VsatBfig::VsatBfig(CCAVariables const & designVariables,
    00056         CCAModel const & model, double cutoffCost)
    00057 {
    00058         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00059         noExpand = false;
    00060
    00061         createBFIG(designVariables, model, cutoffCost);
    00062
    00063         //cerr << "Initializing ValidSAT Tester..." << endl;
    00064         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00065         tester = new Mers::Solvers::SAT::ValidSAT::ValidSAT(variablesAll, designVariables, constraintSet);
    00066 }
    00067
    00069
    00070 VsatBfig::VsatBfig(CCAVariables const & designVariables,
    00071         CCAModel const & model)
    00072 {
    00073         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00074         noExpand = false;
    00075
    00076         createBFIG(designVariables, model);
    00077
    00078         //cerr << "Initializing ValidSAT Tester..." << endl;
    00079         BaseModelSentence const &constraintSet = model.get_all_constraints();
    00080         tester = new Mers::Solvers::SAT::ValidSAT::ValidSAT(variablesAll, designVariables, constraintSet);
    00081 }
    00082
    00084
    00085 VsatBfig::VsatBfig(CCAVariables const & designVariables,
    00086         CCAModel const & model, BaseModelSentence const & constraintSet,
    00087         double cutoffCost)
    00088 {
    00089         noExpand = false;
    00090         createBFIG(designVariables, model, cutoffCost);
    00091
    00092         //cerr << "Initializing ValidSAT Tester..." << endl;
    00093         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00094         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00095                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(variablesAll, designVariables, constraintSet);
    00096         tester = itTester;
    00097 }
    00098
    00100
    00101 VsatBfig::VsatBfig(CCAVariables const & designVariables,
    00102         CCAModel const & model, BaseModelSentence const & constraintSet)
    00103 {
    00104         noExpand = false;
    00105         createBFIG(designVariables, model);
    00106
    00107         //cerr << "Initializing ValidSAT Tester..." << endl;
    00108         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00109         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00110                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(variablesAll, designVariables, constraintSet);
    00111         tester = itTester;
    00112 }
    00113
    00115
    00116 VsatBfig::VsatBfig(BaseModelVariableArray const & designVariables,
    00117         IntegerArray const &valueMap,
    00118         vector<double> const & designVarProbs,
    00119         BaseModelVariableArray const & allVariables,
    00120         BaseModelSentence const & constraintSet,
    00121         double cutoffCost)
    00122 {
    00123         noExpand = false;
    00124
    00125         createBFIG(designVariables, allVariables, valueMap,
    00126                 designVarProbs, cutoffCost);
    00127
    00128         //cerr << "Initializing ValidSAT Tester..." << endl;
    00129         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00130                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVariables, designVariables, constraintSet);
    00131         tester = itTester;
    00132 }
    00133
    00135
    00136 VsatBfig::VsatBfig(BaseModelVariableArray const & designVariables,
    00137         IntegerArray const &valueMap,
    00138         vector<double> const & designVarProbs,
    00139         BaseModelVariableArray const & allVariables,
    00140         BaseModelSentence const & constraintSet)
    00141 {
    00142         noExpand = false;
    00143
    00144         createBFIG(designVariables, allVariables, valueMap,
    00145                 designVarProbs);
    00146
    00147         //cerr << "Initializing ValidSAT Tester..." << endl;
    00148         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00149                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVariables, designVariables, constraintSet);
    00150         tester = itTester;
    00151 }
    00152
    00154
    00155 VsatBfig::VsatBfig(BaseModelVariableArray const & variableSet,
    00156         IntegerArray const &valueMap,
    00157         vector<double> const & designVarProbs,
    00158         BaseModelSentence const & constraintSet, double cutoffCost)
    00159 {
    00160         noExpand = false;
    00161
    00162         createBFIG(variableSet, variableSet, valueMap,
    00163                 designVarProbs, cutoffCost);
    00164
    00165         //cerr << "Initializing ValidSAT Tester..." << endl;
    00166         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00167                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(variableSet, variableSet, constraintSet);
    00168         tester = itTester;
    00169 }
    00170
    00172
    00173 VsatBfig::VsatBfig(BaseModelVariableArray const & variableSet,
    00174         IntegerArray const &valueMap,
    00175         vector<double> const & designVarProbs,
    00176         BaseModelSentence const & constraintSet)
    00177 {
    00178         noExpand = false;
    00179
    00180         createBFIG(variableSet, variableSet, valueMap,
    00181                 designVarProbs);
    00182
    00183         //cerr << "Initializing ValidSAT Tester..." << endl;
    00184         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00185                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(variableSet, variableSet, constraintSet);
    00186         tester = itTester;
    00187 }
    00188
    00190
    00191 VsatBfig::VsatBfig(AssignmentGeneratorInterface * myGenerator, BaseModelVariableArray const & searchVariables,
    00192         BaseModelVariableArray const & allVariables,
    00193         BaseModelSentence const & constraintSet)
    00194 {
    00195         debug = false;
    00196         noExpand = false;
    00197
    00198         generator = myGenerator;
    00199
    00200         //cerr << "Initializing ValidSAT Tester..." << endl;
    00201         Mers::Solvers::SAT::ValidSAT::ValidSAT * itTester =
    00202                 new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVariables, searchVariables, constraintSet);
    00203         tester = itTester;
    00204 }
    00205
    00207
    00208 VsatBfig::~VsatBfig()
    00209 {
    00210 }
    00211
    00213
    00214 void
    00215 VsatBfig::skipExpanding(bool skip)
    00216 {
    00217       noExpand = skip;
    00218 }
    00219
    00221
    00222 void
    00223 VsatBfig::setTemporaryConstraint(BaseModelClause const * c)
    00224 {
    00225         assert(c);
    00226         tester->setTemporaryConstraint(c);
    00227 }
    00228
    00230
    00231 void
    00232 VsatBfig::addConstraint(BaseModelClause const * c)
    00233 {
    00234         assert(c);
    00235         tester->addConstraint(c);
    00237 }
    00238
    00240
    00241 void
    00242 VsatBfig::constrainByReachability()
    00243 {
    00244         //tester->constrainByReachability();
    00245 }
    00246
    00248
    00249 void
    00250 VsatBfig::constrainByNextState()
    00251 {
    00252         //tester->constrainByNextValue();
    00253 }
    00254
    00256
    00257 void
    00258 VsatBfig::clearTemporaryConstraint()
    00259 {
    00260         tester->clearTemporaryConstraint();
    00261 }
    00262
    00264
    00265 void VsatBfig::testTheory()
    00266 {
    00267         BaseModelAssignmentArray conflict(false);
    00268         cerr << "Theory is " << flush;
    00269         AssignmentTesterInterface::SolutionType consistent =
    00270                 tester->tryAssignment(NULL, 0, true, conflict);
    00271         switch(consistent){
    00272         case AssignmentTesterInterface::Valid:
    00273                 cerr << "Valid";
    00274                 break;
    00275         case AssignmentTesterInterface::Satisfiable:
    00276                 cerr << "Satisfiable";
    00277                 break;
    00278         case AssignmentTesterInterface::Unsatisfiable:
    00279                 cerr << "Unsatisfiable";
    00280                 break;
    00281         };
    00282         cerr << endl;
    00283 }
    00284
    00286
    00287 #ifndef EMBEDDED
    00288
    00289 ostream & Mers::Solvers::SAT::GATSAT::VsatBfig::operator <<(ostream & out, VsatBfig const & other)
    00290 {
    00291         out << "VsatBfig:" << endl;
    00292         //other.generator->print(out);
    00293         //other.tester->print(out);
    00294         return out;
    00295 }
    00296
    00297 #endif
    00298
    00300
    00301 void VsatBfig::createBFIG(CCAVariables const & designVariables,
    00302         CCAModel const & model, double cutoffCost)
    00303 {
    00304         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00305         IntegerArray valueMap;
    00306         vector<double> probs;
    00307
    00308         int probIndex = 0;
    00309         unsigned int varIndex;
    00310         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00311                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00312                 // Assign a uniform probability.
    00313                 double prob = 1.0 / var.getDomain()->getLength();
    00314                 BaseModelDomain const &dom = *(var.getDomain());
    00315                 valueMap.pushBack(probIndex);
    00316                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00317                         probs.push_back(prob);
    00318                         probIndex++;
    00319                 }
    00320         }
    00321
    00322         createBFIG(designVariables, variablesAll, valueMap, probs, cutoffCost);
    00323 }
    00324
    00326
    00327 void VsatBfig::createBFIG(CCAVariables const & designVariables,
    00328         CCAModel const & model)
    00329 {
    00330         BaseModelVariableArray const &variablesAll = *(model.get_variables_p());
    00331         IntegerArray valueMap;
    00332         vector<double> probs;
    00333
    00334         int probIndex = 0;
    00335         unsigned int varIndex;
    00336         for(varIndex = 0; varIndex < designVariables.getLength(); varIndex++) {
    00337                 BaseModelVariable const &var = *(designVariables[varIndex]);
    00338                 // Assign a uniform probability.
    00339                 double prob = 1.0 / var.getDomain()->getLength();
    00340                 BaseModelDomain const &dom = *(var.getDomain());
    00341                 valueMap.pushBack(probIndex);
    00342                 for(unsigned int valIndex = 0; valIndex < dom.getLength(); valIndex++) {
    00343                         probs.push_back(prob);
    00344                         probIndex++;
    00345                 }
    00346         }
    00347
    00348         createBFIG(designVariables, variablesAll, valueMap, probs);
    00349 }
    00350
    00352
    00353 void VsatBfig::createBFIG(BaseModelVariableArray const & designVariables,
    00354         BaseModelVariableArray const &allVariables,
    00355         IntegerArray const &valueMap, vector<double> const & probabilities,
    00356         double cutoffCost)
    00357 {
    00358         CDBFIGFactory factory;
    00359         //cerr << "Initializing BFIG Generator..." << endl;
    00360         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00361                 allVariables, valueMap, probabilities, cutoffCost);
    00362         generator = agGen;
    00363 }
    00364
    00366
    00367 void VsatBfig::createBFIG(BaseModelVariableArray const & designVariables,
    00368         BaseModelVariableArray const &allVariables,
    00369         IntegerArray const &valueMap, vector<double> const & probabilities)
    00370 {
    00371         CDBFIGFactory factory;
    00372         //cerr << "Initializing BFIG Generator..." << endl;
    00373         BFIGGenerator * agGen = new BFIGGenerator(factory, designVariables,
    00374                 allVariables, valueMap, probabilities);
    00375         generator = agGen;
    00376 }
    00377
    00379