diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-02 12:39:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-02 12:39:23 +0000 |
commit | 90267f8729799f44c6fb33ace11b971a16e78dff (patch) | |
tree | 94a3bacbc8bba83e8002149232fb9804d2727ec1 /src/prop | |
parent | 1ea434616c48b92189e77b37b3e82dbbee0e0ccc (diff) |
* Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack
* Updated UF to handle the context dependent pre-registration
* Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 3 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 12 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 13 | ||||
-rw-r--r-- | src/prop/sat.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat.h | 11 |
5 files changed, 40 insertions, 3 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 629e44e3e..9b0c4847b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -98,7 +98,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { SatLiteral lit; if (!hasLiteral(node)) { // If no literal, well make one - lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral)); + lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; } else { @@ -411,6 +411,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { //Node atomic = handleNonAtomicNode(node); //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic); } + break; } } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 7ca117c2e..711379519 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -148,6 +148,11 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) setDecisionVar(v, dvar); + // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks + if (theoryAtom) { + variables_to_register.push(VarIntroInfo(v, decisionLevel())); + } + return v; } @@ -295,6 +300,13 @@ void Solver::cancelUntil(int level) { qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); + + // Register variables that have not been registered yet + int currentLevel = decisionLevel(); + for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) { + variables_to_register[i].level = currentLevel; + proxy->variableNotify(variables_to_register[i].var); + } } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 1141e53c4..4c6e98a2e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -80,12 +80,23 @@ protected: /** True if we are currently solving. */ bool minisat_busy; + // Information about registration of variables + struct VarIntroInfo { + Var var; + int level; + VarIntroInfo(Var var, int level) + : var(var), level(level) {} + }; + + /** Variables to re-register with theory solvers on backtracks */ + vec<VarIntroInfo> variables_to_register; + public: // Constructor/Destructor: // Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false); - CVC4_PUBLIC ~Solver(); + CVC4_PUBLIC virtual ~Solver(); // Problem specification: // diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 62558cac1..a7eced6f2 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -27,6 +27,10 @@ namespace CVC4 { namespace prop { +void SatSolver::variableNotify(SatVariable var) { + d_theoryEngine->preRegister(getNode(variableToLiteral(var))); +} + void SatSolver::theoryCheck(theory::Theory::Effort effort) { d_theoryEngine->check(effort); } diff --git a/src/prop/sat.h b/src/prop/sat.h index 2521f3ee7..39977a96b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -70,6 +70,10 @@ inline SatVariable literalToVariable(SatLiteral lit) { return Minisat::var(lit); } +inline SatLiteral variableToLiteral(SatVariable var) { + return Minisat::mkLit(var); +} + inline bool literalSign(SatLiteral lit) { return Minisat::sign(lit); } @@ -208,7 +212,7 @@ public: TheoryEngine* theoryEngine, context::Context* context); - ~SatSolver(); + virtual ~SatSolver(); bool solve(); @@ -242,6 +246,11 @@ public: void removeClausesAboveLevel(int level); + /** + * Notifies of a new variable at a decision level. + */ + void variableNotify(SatVariable var); + void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); |