diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 45 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 32 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 16 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 18 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 31 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 6 |
7 files changed, 139 insertions, 15 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index a260a8ca1..697ab4853 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -351,7 +351,7 @@ void Solver::cancelUntil(int level) { if(intro_level(x) != -1) {// might be unregistered assigns [x] = l_Undef; vardata[x].trail_index = -1; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) polarity[x] = sign(trail[c]); insertVarOrder(x); } @@ -359,6 +359,7 @@ void Solver::cancelUntil(int level) { qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); + flipped.shrink(flipped.size() - level); // Register variables that have not been registered yet int currentLevel = decisionLevel(); @@ -442,7 +443,7 @@ Lit Solver::pickBranchLit() return mkLit(next, (dec_pol == l_True) ); } // If it can't use internal heuristic to do that - return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); + return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] & 0x1)); } } @@ -1461,7 +1462,7 @@ void Solver::pop() Debug("minisat") << "== unassigning " << l << std::endl; Var x = var(l); assigns [x] = l_Undef; - if (phase_saving >= 1) + if (phase_saving >= 1 && (polarity[x] & 0x2) == 0) polarity[x] = sign(l); insertVarOrder(x); trail_user.pop(); @@ -1489,8 +1490,46 @@ void Solver::renewVar(Lit lit, int level) { Var v = var(lit); vardata[v].intro_level = (level == -1 ? getAssertionLevel() : level); setDecisionVar(v, true); + // explicitly not resetting polarity phase-locking here } +bool Solver::flipDecision() { + Debug("flipdec") << "FLIP: decision level is " << decisionLevel() << std::endl; + if(decisionLevel() == 0) { + Debug("flipdec") << "FLIP: no decisions, returning false" << std::endl; + return false; + } + + // find the level to cancel until + int level = trail_lim.size() - 1; + Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 1 : 0) << " flipped?" << flipped[level] << std::endl; + while(level > 0 && (flipped[level] || /* phase-locked */ (polarity[var(trail[trail_lim[level]])] & 0x2) != 0)) { + --level; + Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 2 : 0) << " flipped?" << flipped[level] << std::endl; + } + if(level < 0) { + Lit l = trail[trail_lim[0]]; + Debug("flipdec") << "FLIP: canceling everything, flipping root decision " << l << std::endl; + cancelUntil(0); + newDecisionLevel(); + Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl; + uncheckedEnqueue(~l); + flipped[0] = true; + Debug("flipdec") << "FLIP: returning false" << std::endl; + return false; + } + Lit l = trail[trail_lim[level]]; + Debug("flipdec") << "FLIP: canceling to level " << level << ", flipping decision " << l << std::endl; + cancelUntil(level); + newDecisionLevel(); + Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl; + uncheckedEnqueue(~l); + flipped[level] = true; + Debug("flipdec") << "FLIP: returning true" << std::endl; + return true; +} + + CRef Solver::updateLemmas() { Debug("minisat::lemmas") << "Solver::updateLemmas()" << std::endl; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index e677d7220..fdc9a98b7 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -54,7 +54,7 @@ class Solver { /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::TheoryProxy; - friend class CVC4::SatProof; + friend class CVC4::SatProof; protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ @@ -64,7 +64,7 @@ protected: CVC4::context::Context* context; /** The current assertion level (user) */ - int assertionLevel; + int assertionLevel; /** Variable representing true */ Var varTrue; @@ -77,7 +77,7 @@ public: int getAssertionLevel() const { return assertionLevel; } protected: /** Do we allow incremental solving */ - bool enable_incremental; + bool enable_incremental; /** Literals propagated by lemmas */ vec< vec<Lit> > lemmas; @@ -89,7 +89,7 @@ protected: bool recheck; /** Shrink 'cs' to contain only clauses below given level */ - void removeClausesAboveLevel(vec<CRef>& cs, int level); + void removeClausesAboveLevel(vec<CRef>& cs, int level); /** True if we are currently solving. */ bool minisat_busy; @@ -182,11 +182,13 @@ public: void toDimacs (const char* file, Lit p); void toDimacs (const char* file, Lit p, Lit q); void toDimacs (const char* file, Lit p, Lit q, Lit r); - + // Variable mode: - // + // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. + void freezePolarity (Var v, bool b); // Declare which polarity the decision heuristic MUST ALWAYS use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. + bool flipDecision (); // Backtrack and flip most recent decision // Read state: // @@ -199,6 +201,7 @@ public: int nLearnts () const; // The current number of learnt clauses. int nVars () const; // The current number of variables. int nFreeVars () const; + bool isDecision (Var x) const; // is the given var a decision? // Debugging SMT explanations // @@ -290,8 +293,9 @@ protected: OccLists<Lit, vec<Watcher>, WatcherDeleted> watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec<lbool> assigns; // The current assignments. - vec<char> polarity; // The preferred polarity of each variable. + vec<char> polarity; // The preferred polarity of each variable (bit 0) and whether it's locked (bit 1). vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic. + vec<int> flipped; // Which trail_lim decisions have been flipped in this context. vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. vec<Lit> trail_user; // Stack of assignments to UNdo on user pop. @@ -423,6 +427,8 @@ inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; } +inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; } + inline int Solver::level (Var x) const { return vardata[x].level; } inline int Solver::intro_level(Var x) const { return vardata[x].intro_level; } @@ -466,7 +472,7 @@ inline bool Solver::addClause (Lit p, bool removable) inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } @@ -481,14 +487,16 @@ inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } inline bool Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } -inline void Solver::setDecisionVar(Var v, bool b) -{ - if ( b && !decision[v]) dec_vars++; - else if (!b && decision[v]) dec_vars--; +inline void Solver::freezePolarity(Var v, bool b) { polarity[v] = int(b) | 0x2; } +inline void Solver::setDecisionVar(Var v, bool b) +{ + if ( b && !decision[v] ) dec_vars++; + else if (!b && decision[v] ) dec_vars--; decision[v] = b; insertVarOrder(v); } + inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; } inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; } inline void Solver::interrupt(){ asynch_interrupt = true; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 6b02153c7..6fa698bd0 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -178,6 +178,22 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const return true; } +void MinisatSatSolver::requirePhase(SatLiteral lit) { + Assert(!d_minisat->rnd_pol); + Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl; + SatVariable v = lit.getSatVariable(); + d_minisat->freezePolarity(v, lit.isNegated()); +} + +bool MinisatSatSolver::flipDecision() { + Debug("minisat") << "flipDecision()" << std::endl; + return d_minisat->flipDecision(); +} + +bool MinisatSatSolver::isDecision(SatVariable decn) const { + return d_minisat->isDecision( decn ); +} + /** Incremental interface */ unsigned MinisatSatSolver::getAssertionLevel() const { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 9171bf232..f87e4ae53 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -84,6 +84,12 @@ public: void renewVar(SatLiteral lit, int level = -1); + void requirePhase(SatLiteral lit); + + bool flipDecision(); + + bool isDecision(SatVariable decn) const; + class Statistics { private: ReferenceStat<uint64_t> d_statStarts, d_statDecisions; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 702a530cf..f3904549f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -126,6 +126,24 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { d_cnfStream->convertAndAssert(node, removable, negated); } +void PropEngine::requirePhase(TNode n, bool phase) { + Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; + + Assert(n.getType().isBoolean()); + SatLiteral lit = d_cnfStream->getLiteral(n); + d_satSolver->requirePhase(phase ? lit : ~lit); +} + +bool PropEngine::flipDecision() { + Debug("prop") << "flipDecision()" << endl; + return d_satSolver->flipDecision(); +} + +bool PropEngine::isDecision(Node lit) const { + Assert(isTranslatedSatLiteral(lit)); + return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); +} + void PropEngine::printSatisfyingAssignment(){ const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache(); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 603cdb0e6..dcfc5a9df 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -194,6 +194,37 @@ public: void assertLemma(TNode node, bool negated, bool removable); /** + * If ever n is decided upon, it must be in the given phase. This + * occurs *globally*, i.e., even if the literal is untranslated by + * user pop and retranslated, it keeps this phase. The associated + * variable will _always_ be phase-locked. + * + * @param n the node in question; must have an associated SAT literal + * @param phase the phase to use + */ + void requirePhase(TNode n, bool phase); + + /** + * Backtracks to and flips the most recent unflipped decision, and + * returns TRUE. If the decision stack is nonempty but all + * decisions have been flipped already, the state is backtracked to + * the root decision, which is re-flipped to the original phase (and + * FALSE is returned). If the decision stack is empty, the state is + * unchanged and FALSE is returned. + * + * @return true if a decision was flipped as requested; false if the + * root decision was reflipped, or if no decisions are on the stack. + */ + bool flipDecision(); + + /** + * Return whether the given literal is a SAT decision. Either phase + * is permitted; that is, if "lit" is a SAT decision, this function + * returns true for both lit and the negation of lit. + */ + bool isDecision(Node lit) const; + + /** * Checks the current context for satisfiability. * * @param millis the time limit for this call in milliseconds diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 2865f2cb5..79e54cac2 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -123,6 +123,12 @@ public: virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; + virtual void requirePhase(SatLiteral lit) = 0; + + virtual bool flipDecision() = 0; + + virtual bool isDecision(SatVariable decn) const = 0; + }; }/* prop namespace */ |