From: Dejan Jovanović Date: Fri, 13 Aug 2010 17:27:12 +0000 (+0000) Subject: Adding the changes to the original copy X-Git-Tag: cvc5-1.0.0~8894 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca7639a67b6928fbb9aa2a38d4739a650189f67f;p=cvc5.git Adding the changes to the original copy --- diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README new file mode 100644 index 000000000..af71779d5 --- /dev/null +++ b/src/prop/minisat/CVC4-README @@ -0,0 +1,157 @@ +================ CHANGES TO THE ORIGINAL CODE ================================== + +The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and +the context. The context is obtained from the SmtEngine, and the proxy is an +intermediary class that has all-access to the SatSolver so as to simplify the +interface to (possible) other sat solvers. These two are passed to minisat at +construction time and some additional flags are set. We use the SimpSolver +solver with simplifications. + +To compare with original minisat code in SVN you can compare to revision 6 on +the trunk. + +The PropEngine then uses the following + +// Create the sat solver (this is the proxy, which will create minisat) +d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); +// Add some clauses +d_cnfStream->convertAndAssert(node); +// Check for satisfiabilty +bool result = d_satSolver->solve(); + +* Adding theory literals: + +The newVar method has been changed from + Var Solver::newVar(bool sign, bool dvar) +to + Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) +in order to mark the variables as theory literals. For that purpose there is a +new boolean array called "theory" that is true or false if the variables is for +a theory literal. + +* Backtracking/Pushing + +Backtracking in minisat is performed through the cancelUntil() method, which is +now modified to pop the context the appropriate number of times. + +Minisat pushes the scope in the newDecisionLevel() method where we appropriately +also push the CVC4 context. + +* Phase caching + +In order to implement phase-caching (RSAT paper) we +(1) flag minisat to use the user-provided polarities first by setting the +minisat::SimpSolver::polarity_user flag when initializing the solver (in sat.h) +(2) when a variable is set (in uncheckedEnqueue()) we remember the value in the +"polarity" table. + +* Asserting the theory literals + +In the uncheckedEnqueue() method, if the literal is a theory literal (looking +in the "theory" table), it is passed to the prop engine thorough the proxy. + +* Theory propagation (checking) + +The BCP propagation method was changed from propagate to propagateBool and +another method propagateTheory is defined to do the theory propagation. The +propagate method now looks like + +Clause* Solver::propagate() +{ + Clause* confl = NULL; + + while(qhead < trail.size()) { + confl = propagateBool(); + if (confl != NULL) break; + confl = propagateTheory(); + if (confl != NULL) break; + } + + return confl; +} + +The propagateBool method will perform the BCP on the newly assigned variables +in the trail, and if a conflict is found it will break. Otherwise, the theory +propagation is given a chance to check for satisfiability and maybe enqueue some +additional propagated literals. + +* Conflict resolution + +If a conflict is detected during theory propagation we can rely on the minisat +conflict resolution with a twist. Since a theory can return a conflict where +all literals are assigned at a level lower than the current level, we must +backtrack to the highest level of any literal in the conflict. This is done +already in the propagateTheory(). + +* Clause simplification + +Minisat performs some simplifications on the clause database: +(1) variable elimination +(2) subsumtion + +Subsumtion is complete even with theory reasoning, but eliminating theory +literals by resolution might be incomplete: + +(x = 0 \vee x = 1) \wedge (x != 1 \vee y = 1) \wedge x = y + ^^^^^ ^^^^^^ + v ~v + +would, after eliminating v, simplify to +(x = 0) wedge (y = 1) wedge (x = y) which is unsatisfiable + +while x = 1, y = 1 is a satisfying assignment for the above. + +Minisat does not perform variable elimination on the variables that are marked +as frozen (in the "frozen", SimSolver.h) table. We put all the theory literals +in the frozen table, which solves the incompleteness problem. + +================ NOTES ========================================================= + +* Accessing the internals of the SAT solver + +The non-public parts of the SAT solver are accessed via the static methods in +the SatSolver class. SatSolverProxy is declared as a friend of the +SatSolver and has all-privileges access to the internals -- use with care!!! + +* Clause Database and CNF + +The clause database consists of two parts: + + vec clauses; // List of problem clauses. + vec learnts; // List of learnt clauses. + +Clauses is the original problem clauses, and learnts are the clauses learned +during the search. I have disabled removal of satisfied problem clauses by +setting the remove_satisfied flag to false. + +The learnt clauses get removed every once in a while by removing the half of +clauses with the low activity (reduceDB()) + +Since the clause database backtracks with the SMT solver, the CNF cache should +be context dependent and everything will be in sync. + +* Adding a Clause + +The only method in the interface that allows addition of clauses in MiniSAT is + + bool Solver::addClause(vec& ps), + +but it only adds the problem clauses. + +In order to add the clauses to the removable database the interface is now + + bool Solver::addClause(vec& ps, bool removable). + +Clauses added with removable=true might get removed by the SAT solver when +compacting the database. + +The question is whether to add the propagation/conflict lemmas as removable or +not? + +* Literal Activities + +We do not backtrack literal activities. This does not semantically change the +equivalence of the context, but does change solve times if the same problem is +run several times. + +* Do we need to assign literals that only appear in satisfied clauses? diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile new file mode 100644 index 000000000..e8b442ac1 --- /dev/null +++ b/src/prop/minisat/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/prop/minisat + +include $(topdir)/Makefile.subdir diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am new file mode 100644 index 000000000..56f61adad --- /dev/null +++ b/src/prop/minisat/Makefile.am @@ -0,0 +1,29 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG + +noinst_LTLIBRARIES = libminisat.la +libminisat_la_SOURCES = \ + core/Solver.C \ + core/Solver.h \ + core/SolverTypes.h \ + simp/SimpSolver.C \ + simp/SimpSolver.h \ + mtl/Alg.h \ + mtl/BasicHeap.h \ + mtl/BoxedVec.h \ + mtl/Heap.h \ + mtl/Map.h \ + mtl/Queue.h \ + mtl/Sort.h \ + mtl/Vec.h + +EXTRA_DIST = \ + core/Main.C \ + core/Makefile \ + simp/Main.C \ + simp/Makefile \ + README \ + LICENSE \ + mtl/template.mk diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 404f4da5e..1667af20d 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -19,17 +19,46 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Solver.h" #include "Sort.h" +#include "prop/sat.h" #include - //================================================================================================= // Constructor/Destructor: +namespace CVC4 { +namespace prop { +namespace minisat { + +Clause* Solver::lazy_reason = reinterpret_cast(1); + +Clause* Solver::getReason(Lit l) +{ + if (reason[var(l)] != lazy_reason) return reason[var(l)]; + // Get the explanation from the theory + SatClause explanation; + if (value(l) == l_True) { + proxy->explainPropagation(l, explanation); + assert(explanation[0] == l); + } else { + proxy->explainPropagation(~l, explanation); + assert(explanation[0] == ~l); + } + Clause* real_reason = Clause_new(explanation, true); + reason[var(l)] = real_reason; + // Add it to the database + learnts.push(real_reason); + attachClause(*real_reason); + return real_reason; +} + +Solver::Solver(SatSolver* proxy, context::Context* context) : -Solver::Solver() : + // SMT stuff + proxy(proxy) + , context(context) // Parameters: (formerly in 'SearchParams') - var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) + , var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) // More parameters: @@ -70,7 +99,7 @@ Solver::~Solver() // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). // -Var Solver::newVar(bool sign, bool dvar) +Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) { int v = nVars(); watches .push(); // (list for positive literal) @@ -81,6 +110,8 @@ Var Solver::newVar(bool sign, bool dvar) activity .push(0); seen .push(0); + theory .push(theoryAtom); + polarity .push((char)sign); decision_var.push((char)dvar); @@ -89,7 +120,7 @@ Var Solver::newVar(bool sign, bool dvar) } -bool Solver::addClause(vec& ps) +bool Solver::addClause(vec& ps, ClauseType type) { assert(decisionLevel() == 0); @@ -110,16 +141,19 @@ bool Solver::addClause(vec& ps) if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ + assert(type != CLAUSE_LEMMA); assert(value(ps[0]) == l_Undef); uncheckedEnqueue(ps[0]); - return ok = (propagate() == NULL); + return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL); }else{ Clause* c = Clause_new(ps, false); clauses.push(c); + if (type == CLAUSE_LEMMA) lemmas.push(c); attachClause(*c); } return true; + } @@ -132,6 +166,7 @@ void Solver::attachClause(Clause& c) { void Solver::detachClause(Clause& c) { + Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); assert(find(watches[toInt(~c[0])], &c)); assert(find(watches[toInt(~c[1])], &c)); @@ -142,8 +177,10 @@ void Solver::detachClause(Clause& c) { void Solver::removeClause(Clause& c) { + Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl; detachClause(c); - free(&c); } + free(&c); +} bool Solver::satisfied(const Clause& c) const { @@ -157,14 +194,26 @@ bool Solver::satisfied(const Clause& c) const { // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + // Pop the SMT context + for (int l = trail_lim.size() - level; l > 0; --l) + context->pop(); + // Now the minisat stuff + for (int c = trail.size()-1; c >= trail_lim[level]; c--) { Var x = var(trail[c]); assigns[x] = toInt(l_Undef); - insertVarOrder(x); } + insertVarOrder(x); + } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - } } + // We can erase the lemmas now + for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) { + // TODO: can_erase[lemma[c]] = true; + } + lemmas.shrink(lemmas.size() - lemmas_lim[level]); + lemmas_lim.shrink(lemmas_lim.size() - level); + } +} //================================================================================================= @@ -255,7 +304,7 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; - confl = reason[var(p)]; + confl = getReason(p); seen[var(p)] = 0; pathC--; @@ -272,12 +321,12 @@ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) - if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level)) + if (getReason(out_learnt[i]) == NULL || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; }else{ out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++){ - Clause& c = *reason[var(out_learnt[i])]; + Clause& c = *getReason(out_learnt[i]); for (int k = 1; k < c.size(); k++) if (!seen[var(c[k])] && level[var(c[k])] > 0){ out_learnt[j++] = out_learnt[i]; @@ -315,13 +364,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ - assert(reason[var(analyze_stack.last())] != NULL); + assert(getReason(analyze_stack.last()) != NULL); Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); for (int i = 1; i < c.size(); i++){ Lit p = c[i]; if (!seen[var(p)] && level[var(p)] > 0){ - if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ + if (getReason(p) != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ seen[var(p)] = 1; analyze_stack.push(p); analyze_toclear.push(p); @@ -381,16 +430,110 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) void Solver::uncheckedEnqueue(Lit p, Clause* from) { assert(value(p) == l_Undef); - assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient - level [var(p)] = decisionLevel(); - reason [var(p)] = from; + assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost efficient + level [var(p)] = decisionLevel(); + reason [var(p)] = from; + // Added for phase-caching + polarity [var(p)] = sign(p); trail.push(p); + + if (theory[var(p)] && from != lazy_reason) { + // Enqueue to the theory + proxy->enqueueTheoryLiteral(p); + } +} + + +Clause* Solver::propagate(TheoryCheckType type) +{ + Clause* confl = NULL; + + // If this is the final check, no need for Boolean propagation and + // theory propagation + if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + return theoryCheck(theory::Theory::FULL_EFFORT); + } + + // The effort we will be using to theory check + theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? + theory::Theory::QUICK_CHECK : theory::Theory::STANDARD; + + // Keep running until we have checked everything, we + // have no conflict and no new literals have been asserted + bool new_assertions; + do { + new_assertions = false; + while(qhead < trail.size()) { + confl = propagateBool(); + if (confl != NULL) break; + confl = theoryCheck(effort); + if (confl != NULL) break; + } + + if (confl == NULL && type == CHECK_WITH_PROPAGATION_STANDARD) { + new_assertions = propagateTheory(); + if (!new_assertions) break; + } + } while (new_assertions); + + return confl; } +bool Solver::propagateTheory() { + std::vector propagatedLiterals; + proxy->theoryPropagate(propagatedLiterals); + const unsigned i_end = propagatedLiterals.size(); + for (unsigned i = 0; i < i_end; ++ i) { + uncheckedEnqueue(propagatedLiterals[i], lazy_reason); + } + proxy->clearPropagatedLiterals(); + return propagatedLiterals.size() > 0; +} /*_________________________________________________________________________________________________ | -| propagate : [void] -> [Clause*] +| theoryCheck: [void] -> [Clause*] +| +| Description: +| Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting +| clause is returned, otherwise NULL. +| +| Note: the propagation queue might be NOT empty +|________________________________________________________________________________________________@*/ +Clause* Solver::theoryCheck(theory::Theory::Effort effort) +{ + Clause* c = NULL; + SatClause clause; + proxy->theoryCheck(effort, clause); + int clause_size = clause.size(); + Assert(clause_size != 1, "Can't handle unit clause explanations"); + if(clause_size > 0) { + // Find the max level of the conflict + int max_level = 0; + for (int i = 0; i < clause_size; ++i) { + int current_level = level[var(clause[i])]; + Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason[var(clause[i])] << " at level " << current_level << std::endl; + Assert(toLbool(assigns[var(clause[i])]) != l_Undef, "Got an unassigned literal in conflict!"); + if (current_level > max_level) max_level = current_level; + } + // If smaller than the decision level then pop back so we can analyse + Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl; + Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!"); + if (max_level < decisionLevel()) { + Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl; + cancelUntil(max_level); + } + // Create the new clause and attach all the information + c = Clause_new(clause, true); + learnts.push(c); + attachClause(*c); + } + return c; +} + +/*_________________________________________________________________________________________________ +| +| propagateBool : [void] -> [Clause*] | | Description: | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, @@ -399,7 +542,7 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ -Clause* Solver::propagate() +Clause* Solver::propagateBool() { Clause* confl = NULL; int num_props = 0; @@ -509,7 +652,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) + if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -554,9 +697,9 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) starts++; bool first = true; - + TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; for (;;){ - Clause* confl = propagate(); + Clause* confl = propagate(check_type); if (confl != NULL){ // CONFLICT conflicts++; conflictC++; @@ -582,9 +725,16 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) varDecayActivity(); claDecayActivity(); + // We have a conflict so, we are going back to standard checks + check_type = CHECK_WITH_PROPAGATION_STANDARD; + }else{ // NO CONFLICT + // If this was a final check, we are satisfiable + if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) + return l_True; + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); @@ -620,9 +770,11 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) decisions++; next = pickBranchLit(polarity_mode, random_var_freq); - if (next == lit_Undef) - // Model found: - return l_True; + if (next == lit_Undef) { + // We need to do a full theory check to confirm + check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; + continue; + } } // Increase decision level and enqueue 'next' @@ -722,7 +874,8 @@ void Solver::verifyModel() assert(!failed); - reportf("Verified %d original clauses.\n", clauses.size()); + if(verbosity >= 1) + reportf("Verified %d original clauses.\n", clauses.size()); } @@ -739,3 +892,8 @@ void Solver::checkLiteralCount() assert((int)clauses_literals == cnt); } } + +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 0137b6ff3..2e44803e9 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,34 +17,68 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Solver_h -#define Solver_h +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__MINISAT__SOLVER_H +#define __CVC4__PROP__MINISAT__SOLVER_H + +#include "context/context.h" +#include "theory/theory.h" #include +#include -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" +#include "../mtl/Vec.h" +#include "../mtl/Heap.h" +#include "../mtl/Alg.h" #include "SolverTypes.h" - //================================================================================================= // Solver -- the main class: +namespace CVC4 { +namespace prop { + +class SatSolver; + +namespace minisat { class Solver { + + /** The only CVC4 entry point to the private solver data */ + friend class CVC4::prop::SatSolver; + +protected: + + /** The pointer to the proxy that provides interfaces to the SMT engine */ + SatSolver* proxy; + + /** The context from the SMT solver */ + context::Context* context; + public: // Constructor/Destructor: // - Solver(); - ~Solver(); + Solver(SatSolver* proxy, context::Context* context); + CVC4_PUBLIC ~Solver(); // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. - bool addClause (vec& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. + + // Types of clauses + enum ClauseType { + // Clauses defined by the problem + CLAUSE_PROBLEM, + // Lemma clauses added by the theories + CLAUSE_LEMMA, + // Conflict clauses + CLAUSE_CONFLICT + }; + + bool addClause (vec& ps, ClauseType type); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: // @@ -54,7 +88,7 @@ public: bool okay () const; // FALSE means solver is in a conflicting state // Variable mode: - // + // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should 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. @@ -122,12 +156,20 @@ protected: vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments (lbool:s stored as char:s). vec polarity; // The preferred polarity of each variable. + vec theory; // Is the variable representing a theory atom vec decision_var; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. - vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec lemmas; // List of lemmas we added (context dependent) + vec lemmas_lim; // Separator indices for different decision levels in 'lemmas'. + static Clause* lazy_reason; // The mark when we need to ask the theory engine for a reason + vec reason; // 'reason[var]' is the clause that implied the variables current value, lazy_reason if theory propagated, or 'NULL' if none. + + Clause* getReason(Lit l); // Returns the reason, or asks the theory for an explanation + vec level; // 'level[var]' contains the level at which the assignment was made. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int lhead; // Head of the lemma stack (for backtracking) int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. vec assumptions; // Current set of assumptions provided to solve by the user. @@ -144,6 +186,15 @@ protected: vec analyze_toclear; vec add_tmp; + enum TheoryCheckType { + // Quick check, but don't perform theory propagation + CHECK_WITHOUTH_PROPAGATION_QUICK, + // Check and perform theory propagation + CHECK_WITH_PROPAGATION_STANDARD, + // The SAT problem is satisfiable, perform a full theory check + CHECK_WITHOUTH_PROPAGATION_FINAL + }; + // Main internal methods: // void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. @@ -151,7 +202,10 @@ protected: void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. - Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause. + Clause* propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause. + Clause* propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. + bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted. + Clause* theoryCheck (theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? @@ -177,7 +231,7 @@ protected: // Misc: // - int decisionLevel () const; // Gives the current decisionlevel. + int decisionLevel () const; // Gives the current decision level. uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... @@ -203,11 +257,9 @@ protected: return (int)(drand(seed) * size); } }; - //================================================================================================= // Implementation of inline methods: - inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); } @@ -233,7 +285,7 @@ inline void Solver::claBumpActivity (Clause& c) { inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.size()); context->push(); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); } @@ -256,6 +308,7 @@ inline bool Solver::okay () const { return ok; } #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) ) +//#define reportf(format, args...) do {} while(0) static inline void logLit(FILE* f, Lit l) { @@ -297,6 +350,9 @@ inline void Solver::printClause(const C& c) } } +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ //================================================================================================= -#endif +#endif /* __CVC4__PROP__MINISAT__SOLVER_H */ diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 47e302390..fd6a78ab0 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -17,13 +17,18 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" -#ifndef SolverTypes_h -#define SolverTypes_h +#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H +#define __CVC4__PROP__MINISAT__SOLVERTYPES_H #include #include +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -194,4 +199,8 @@ inline void Clause::strengthen(Lit p) calcAbstraction(); } -#endif +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */ diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 240962dfc..e636f2b87 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -17,8 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Alg_h -#define Alg_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Alg_h +#define CVC4_MiniSat_Alg_h + +#include + +namespace CVC4 { +namespace prop { +namespace minisat { //================================================================================================= // Useful functions on vectors @@ -54,4 +62,8 @@ static inline bool find(V& ts, const T& t) return j < ts.size(); } -#endif +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_Alg_h */ diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index 556d98f84..cb6a7cbd8 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef BasicHeap_h -#define BasicHeap_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_BasicHeap_h +#define CVC4_MiniSat_BasicHeap_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -95,4 +101,9 @@ class BasicHeap { //================================================================================================= -#endif + +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_BasicHeap_h */ diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index bddf41008..7cf5ba14f 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef BoxedVec_h -#define BoxedVec_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_BoxedVec_h +#define CVC4_MiniSat_BoxedVec_h #include #include #include +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Automatically resizable arrays // @@ -50,7 +56,7 @@ class bvec { x->cap = size; return x; } - + }; Vec_t* ref; @@ -76,16 +82,16 @@ class bvec { altvec (altvec& other) { assert(0); } public: - void clear (bool dealloc = false) { + void clear (bool dealloc = false) { if (ref != NULL){ - for (int i = 0; i < ref->sz; i++) + for (int i = 0; i < ref->sz; i++) (*ref).data[i].~T(); - if (dealloc) { - free(ref); ref = NULL; - }else + if (dealloc) { + free(ref); ref = NULL; + }else ref->sz = 0; - } + } } // Constructors: @@ -107,11 +113,11 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - //new (&ref->data[size]) T(elem); - ref->data[size] = elem; - ref->sz = size+1; + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; } void push () { @@ -119,10 +125,10 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - new (&ref->data[size]) T(); - ref->sz = size+1; + new (&ref->data[size]) T(); + ref->sz = size+1; } void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } @@ -143,5 +149,8 @@ public: }; +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif +#endif /* CVC4_MiniSat_BoxedVec_h */ diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index b07ccd152..20d379b1d 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -17,10 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Heap_h -#define Heap_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Heap_h +#define CVC4_MiniSat_Heap_h #include "Vec.h" +#include + +namespace CVC4 { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -92,7 +99,7 @@ class Heap { indices[n] = heap.size(); heap.push(n); - percolateUp(indices[n]); + percolateUp(indices[n]); } @@ -104,19 +111,19 @@ class Heap { indices[x] = -1; heap.pop(); if (heap.size() > 1) percolateDown(0); - return x; + return x; } - void clear(bool dealloc = false) - { + void clear(bool dealloc = false) + { for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1; #ifdef NDEBUG for (int i = 0; i < indices.size(); i++) assert(indices[i] == -1); #endif - heap.clear(dealloc); + heap.clear(dealloc); } @@ -164,6 +171,9 @@ class Heap { }; +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ //================================================================================================= -#endif +#endif /* CVC4_MiniSat_Heap_h */ diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index b6d76a31c..715b84da4 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Map_h -#define Map_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Map_h +#define CVC4_MiniSat_Map_h #include #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Default hash/equals functions // @@ -80,7 +86,7 @@ class Map { cap = newsize; } - + public: Map () : table(NULL), cap(0), size(0) {} @@ -94,7 +100,7 @@ class Map { for (int i = 0; i < ps.size(); i++) if (equals(ps[i].key, k)){ d = ps[i].data; - return true; } + return true; } return false; } @@ -115,4 +121,8 @@ class Map { } }; -#endif +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_Map_h */ diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index 2cc110ce9..291a1f2e3 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Queue_h -#define Queue_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Queue_h +#define CVC4_MiniSat_Queue_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= @@ -79,4 +85,9 @@ public: //}; //================================================================================================= -#endif + +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_Queue_h */ diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index 1f301f5c2..19e89803b 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -17,11 +17,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Sort_h -#define Sort_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Sort_h +#define CVC4_MiniSat_Sort_h #include "Vec.h" +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Some sorting algorithms for vec's @@ -90,4 +96,9 @@ template void sort(vec& v) { //================================================================================================= -#endif + +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* CVC4_MiniSat_Sort_h */ diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index e780aa167..364991aa9 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -17,13 +17,19 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef Vec_h -#define Vec_h +#include "cvc4_private.h" + +#ifndef CVC4_MiniSat_Vec_h +#define CVC4_MiniSat_Vec_h #include #include #include +namespace CVC4 { +namespace prop { +namespace minisat { + //================================================================================================= // Automatically resizable arrays // @@ -129,5 +135,8 @@ void vec::clear(bool dealloc) { sz = 0; if (dealloc) free(data), data = NULL, cap = 0; } } +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif +#endif /* CVC4_MiniSat_Vec_h */ diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 22121c31e..00f93402f 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -24,9 +24,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //================================================================================================= // Constructor/Destructor: +namespace CVC4 { +namespace prop { +namespace minisat { -SimpSolver::SimpSolver() : - grow (0) +SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) : + Solver(proxy, context) + , grow (0) , asymm_mode (false) , redundancy_check (false) , merges (0) @@ -54,14 +58,14 @@ SimpSolver::~SimpSolver() } -Var SimpSolver::newVar(bool sign, bool dvar) { - Var v = Solver::newVar(sign, dvar); +Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { + Var v = Solver::newVar(sign, dvar,theoryAtom); if (use_simplification){ n_occ .push(0); n_occ .push(0); occurs .push(); - frozen .push((char)false); + frozen .push((char)theoryAtom); touched .push(0); elim_heap.insert(v); elimtable.push(); @@ -114,7 +118,7 @@ bool SimpSolver::solve(const vec& assumps, bool do_simp, bool turn_off_simp -bool SimpSolver::addClause(vec& ps) +bool SimpSolver::addClause(vec& ps, ClauseType type) { for (int i = 0; i < ps.size(); i++) if (isEliminated(var(ps[i]))) @@ -125,7 +129,7 @@ bool SimpSolver::addClause(vec& ps) if (redundancy_check && implied(ps)) return true; - if (!Solver::addClause(ps)) + if (!Solver::addClause(ps, type)) return false; if (use_simplification && clauses.size() == nclauses + 1){ @@ -152,6 +156,7 @@ bool SimpSolver::addClause(vec& ps) void SimpSolver::removeClause(Clause& c) { + Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl; assert(!c.learnt()); if (use_simplification) @@ -207,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true; } @@ -224,11 +229,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& ou for (int i = 0; i < qs.size(); i++){ if (var(qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) + if (var(ps[j]) == var(qs[i])) { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -256,11 +262,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v) for (int i = 0; i < qs.size(); i++){ if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) + if (var(__ps[j]) == var(__qs[i])) { if (__ps[j] == ~__qs[i]) return false; else goto next; + } } next:; } @@ -305,7 +312,7 @@ bool SimpSolver::implied(const vec& c) uncheckedEnqueue(~c[i]); } - bool result = propagate() != NULL; + bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL; cancelUntil(0); return result; } @@ -387,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c) else l = c[i]; - if (propagate() != NULL){ + if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){ cancelUntil(0); asymm_lits++; if (!strengthenClause(c, l)) @@ -478,7 +485,7 @@ bool SimpSolver::eliminateVar(Var v, bool fail) vec resolvent; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) - if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent)) + if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent, CLAUSE_CONFLICT)) return false; // DEBUG: For checking that a clause set is saturated with respect to variable elimination. @@ -520,7 +527,7 @@ void SimpSolver::remember(Var v) clause.push(c[j]); remembered_clauses++; - check(addClause(clause)); + check(addClause(clause, CLAUSE_PROBLEM)); free(&c); } @@ -698,3 +705,7 @@ void SimpSolver::toDimacs(const char* file) }else fprintf(stderr, "could not open file %s\n", file); } + +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index f1bf88240..3da574f6c 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -17,26 +17,35 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef SimpSolver_h -#define SimpSolver_h +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H +#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H #include +#include + +#include "../mtl/Queue.h" +#include "../core/Solver.h" -#include "Queue.h" -#include "Solver.h" +namespace CVC4 { +namespace prop { +class SatSolver; + +namespace minisat { class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(); - ~SimpSolver(); + SimpSolver(SatSolver* proxy, context::Context* context); + CVC4_PUBLIC ~SimpSolver(); // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); - bool addClause (vec& ps); + Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); + bool addClause (vec& ps, ClauseType type); // Variable mode: // @@ -157,5 +166,9 @@ inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size( inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } } inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp) { vec tmp; return solve(tmp, do_simp, turn_off_simp); } +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + //================================================================================================= -#endif +#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */