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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/CompileSAT/CompileSAT.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
    00011 #ifdef _MSC_VER
    00012 #pragma warning( disable : 4786 )
    00013 #endif
    00014
    00015 #include "CompileSAT.h"
    00016
    00017 #include <cassert>
    00018 #include <Mers/Generators/IDSetGenerator/IDSetGenerator.h>
    00019 #include <Mers/Solvers/SAT/ValidSAT/ValidSAT.h>
    00020
    00022
    00023 using namespace Mers::Solvers::SAT::GATSAT::CompileSAT;
    00024 using Mers::Solvers::SAT::GATSAT::GATSAT;
    00025 using Mers::Solvers::SAT::AssignmentTesterInterface;
    00026 using Mers::Solvers::SAT::ValidSAT::ValidSAT;
    00027 using Mers::Generators::AssignmentGeneratorInterface;
    00028 using Mers::Generators::IDSetGenerator::IDSetGenerator;
    00029 using Mers::Models::Base::BaseModelVariableArray;
    00030 using Mers::Models::Base::BaseModelVariableArrayArray;
    00031 using Mers::Models::Base::BaseModelSentence;
    00032 using Mers::Models::Base::BaseModelClause;
    00033 using std::cout;
    00034 using std::endl;
    00035 using std::ostream;
    00036
    00038
    00039 CompileSAT::CompileSAT(BaseModelVariableArrayArray const & searchGroups,
    00040         BaseModelVariableArray const & decisionVariables,
    00041         BaseModelVariableArray const & allVariables,
    00042         BaseModelSentence const & constraintSet, bool testForValid)
    00043         : decisionVars(false), allVars(false),
    00044         constraints(BaseModelSentence::CNF, true), searchSet(true)
    00045 {
    00046         searchSet = searchGroups;
    00047         decisionVars = decisionVariables;
    00048
    00049         allVars = allVariables;
    00050         constraints = constraintSet;
    00051
    00052         generator = new IDSetGenerator(searchSet);
    00053
    00054         tester = new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVars, decisionVars, constraints, testForValid);
    00055 }
    00056
    00058
    00059 CompileSAT::CompileSAT(BaseModelVariableArray const & decisionVariables,
    00060         BaseModelVariableArray const & allVariables,
    00061         BaseModelSentence const & constraintSet, bool testForValid)
    00062         : decisionVars(false), allVars(false),
    00063         constraints(BaseModelSentence::CNF, true), searchSet(true)
    00064 {
    00065         decisionVars = decisionVariables;
    00066         allVars = allVariables;
    00067         constraints = constraintSet;
    00068
    00069         BaseModelVariableArray * searchVect =
    00070                 new BaseModelVariableArray(decisionVars);
    00071         searchSet.pushBack(searchVect);
    00072         generator = new IDSetGenerator(searchSet);
    00073
    00074         tester = new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVars, decisionVars, constraints, testForValid);
    00075 }
    00076
    00078
    00079 CompileSAT::CompileSAT(BaseModelVariableArray const & allVariables,
    00080         BaseModelSentence const & constraintSet, bool testForValid)
    00081         : decisionVars(false), allVars(false),
    00082         constraints(BaseModelSentence::CNF, true), searchSet(true)
    00083 {
    00084         decisionVars = allVariables;
    00085         allVars = allVariables;
    00086         constraints = constraintSet;
    00087
    00088         BaseModelVariableArray * searchVect =
    00089                 new BaseModelVariableArray(decisionVars);
    00090         searchSet.pushBack(searchVect);
    00091         generator = new IDSetGenerator(searchSet);
    00092
    00093         tester = new Mers::Solvers::SAT::ValidSAT::ValidSAT(allVars, decisionVars, constraints, testForValid);
    00094 }
    00095
    00097
    00098 CompileSAT::CompileSAT(AssignmentGeneratorInterface * myGenerator,
    00099         AssignmentTesterInterface * myTester)
    00100         : GATSAT(myGenerator, myTester), decisionVars(false), allVars(false),
    00101         constraints(BaseModelSentence::CNF, true), searchSet(true)
    00102 {
    00103 }
    00104
    00106
    00107 CompileSAT::~CompileSAT()
    00108 {
    00109 }
    00110
    00112
    00113 void CompileSAT::addTemporaryConstraint(BaseModelClause const * c)
    00114 {
    00115         tester->addTemporaryConstraint(c);
    00116 }
    00117
    00119
    00120 void CompileSAT::setTemporaryConstraint(BaseModelClause const * c)
    00121 {
    00122         tester->setTemporaryConstraint(c);
    00123 }
    00124
    00126
    00127 void CompileSAT::clearTemporaryConstraint()
    00128 {
    00129         tester->clearTemporaryConstraint();
    00130 }
    00131
    00133
    00134 #ifndef EMBEDDED
    00135
    00136 ostream& Mers::Solvers::SAT::GATSAT::CompileSAT::operator<<(ostream& os,
    00137         CompileSAT const & op)
    00138 {
    00139         // not complete, for now:
    00140         (void)op;
    00141         os << "CompileSAT: Generate and Test SAT Engine for Compilation" << endl;
    00142         return os;
    00143 }
    00144
    00145 #endif
    00146