diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
commit | dc4b8296ded0a2288fbfeb71b9ded9217bad6b86 (patch) | |
tree | 7bb1a9d305c46464e0470486e406cdffa9558644 /src/prop/prop_engine.cpp | |
parent | fb7d93e00e70b36d12c1d5deec914426c982b3cf (diff) |
beautification of the prop engine
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 78 |
1 files changed, 36 insertions, 42 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ad38c2a1f..5889ba504 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -17,9 +17,6 @@ #include "theory/theory_engine.h" #include "util/decision_engine.h" -#include "prop/minisat/mtl/Vec.h" -#include "prop/minisat/simp/SimpSolver.h" -#include "prop/minisat/core/SolverTypes.h" #include "util/Assert.h" #include "util/output.h" #include "util/options.h" @@ -28,44 +25,42 @@ #include <utility> #include <map> -using namespace CVC4::prop::minisat; using namespace std; namespace CVC4 { +namespace prop { -PropEngine::PropEngine(const Options* opts, - DecisionEngine& de, - TheoryEngine& te) : +PropEngine::PropEngine(const Options* opts, DecisionEngine* de, + TheoryEngine* te) : d_opts(opts), - d_de(de), - d_te(te), - d_restartMayBeNeeded(false){ - d_sat = new Solver(); + d_de(de), + d_te(te), + d_restartMayBeNeeded(false) { + d_sat = new SatSolver(); d_cnfStream = new CVC4::prop::TseitinCnfStream(this); } -PropEngine::~PropEngine(){ +PropEngine::~PropEngine() { delete d_cnfStream; delete d_sat; } - -void PropEngine::assertClause(vec<Lit> & c){ +void PropEngine::assertClause(SatClause& clause) { /*we can also here add a context dependent queue of assertions *for restarting the sat solver */ //TODO assert that each lit has been mapped to an atom or requested - d_sat->addClause(c); + d_sat->addClause(clause); } -Var PropEngine::registerAtom(const Node & n){ - Var v = requestFreshVar(); - d_atom2var.insert(make_pair(n,v)); - d_var2atom.insert(make_pair(v,n)); +SatVariable PropEngine::registerAtom(const Node & n) { + SatVariable v = requestFreshVar(); + d_atom2var.insert(make_pair(n, v)); + d_var2atom.insert(make_pair(v, n)); return v; } -Var PropEngine::requestFreshVar(){ +SatVariable PropEngine::requestFreshVar() { return d_sat->newVar(); } @@ -79,20 +74,19 @@ void PropEngine::assertFormula(const Node& node) { d_assertionList.push_back(node); } -void PropEngine::restart(){ +void PropEngine::restart() { delete d_sat; - d_sat = new Solver(); + d_sat = new SatSolver(); d_cnfStream->flushCache(); d_atom2var.clear(); d_var2atom.clear(); - for(vector<Node>::iterator iter = d_assertionList.begin(); - iter != d_assertionList.end(); ++iter){ + for(vector<Node>::iterator iter = d_assertionList.begin(); iter + != d_assertionList.end(); ++iter) { d_cnfStream->convertAndAssert(*iter); } } - Result PropEngine::solve() { if(d_restartMayBeNeeded) restart(); @@ -100,7 +94,7 @@ Result PropEngine::solve() { d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1; bool result = d_sat->solve(); - if(!result){ + if(!result) { d_restartMayBeNeeded = true; } @@ -109,22 +103,22 @@ Result PropEngine::solve() { return Result(result ? Result::SAT : Result::UNSAT); } +void PropEngine::assertLit(SatLiteral lit) { + SatVariable var = literalToVariable(lit); + if(isVarMapped(var)) { + Node atom = lookupVar(var); + //Theory* t = ...; + //t must be the corresponding theory for the atom + + //Literal l(atom, sign(l)); + //t->assertLiteral(l ); + } +} - void PropEngine::assertLit(Lit l){ - Var v = var(l); - if(isVarMapped(v)){ - Node atom = lookupVar(v); - //Theory* t = ...; - //t must be the corresponding theory for the atom - - //Literal l(atom, sign(l)); - //t->assertLiteral(l ); - } - } - - void PropEngine::signalBooleanPropHasEnded(){} - //TODO decisionEngine should be told - //TODO theoryEngine to call lightweight theory propogation - +void PropEngine::signalBooleanPropHasEnded() { +} +//TODO decisionEngine should be told +//TODO theoryEngine to call lightweight theory propogation +}/* prop namespace */ }/* CVC4 namespace */ |