--- /dev/null
+================ 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<Clause*> clauses; // List of problem clauses.
+ vec<Clause*> 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<Lit>& 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<Lit>& 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?
--- /dev/null
+topdir = ../../..
+srcdir = src/prop/minisat
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
#include "Solver.h"
#include "Sort.h"
+#include "prop/sat.h"
#include <cmath>
-
//=================================================================================================
// Constructor/Destructor:
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
+Clause* Solver::lazy_reason = reinterpret_cast<Clause*>(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:
// 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)
activity .push(0);
seen .push(0);
+ theory .push(theoryAtom);
+
polarity .push((char)sign);
decision_var.push((char)dvar);
}
-bool Solver::addClause(vec<Lit>& ps)
+bool Solver::addClause(vec<Lit>& ps, ClauseType type)
{
assert(decisionLevel() == 0);
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;
+
}
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));
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 {
//
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);
+ }
+}
//=================================================================================================
// 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--;
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];
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);
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<Lit> 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,
| 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;
{
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))
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++;
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();
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'
assert(!failed);
- reportf("Verified %d original clauses.\n", clauses.size());
+ if(verbosity >= 1)
+ reportf("Verified %d original clauses.\n", clauses.size());
}
assert((int)clauses_literals == cnt);
}
}
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
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 <cstdio>
+#include <cassert>
-#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<Lit>& 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<Lit>& ps, ClauseType type); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
// Solving:
//
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.
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<char> assigns; // The current assignments (lbool:s stored as char:s).
vec<char> polarity; // The preferred polarity of each variable.
+ vec<bool> theory; // Is the variable representing a theory atom
vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
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<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+ vec<Clause*> lemmas; // List of lemmas we added (context dependent)
+ vec<int> 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<Clause*> 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<int> 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<Lit> assumptions; // Current set of assumptions provided to solve by the user.
vec<Lit> analyze_toclear;
vec<Lit> 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.
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<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
// 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 ...
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); }
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); }
#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)
{
}
}
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
//=================================================================================================
-#endif
+#endif /* __CVC4__PROP__MINISAT__SOLVER_H */
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 <cassert>
#include <stdint.h>
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
calcAbstraction();
}
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */
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 <cassert>
+
+namespace CVC4 {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Useful functions on vectors
return j < ts.size();
}
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Alg_h */
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.
//=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_BasicHeap_h */
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 <cstdlib>
#include <cassert>
#include <new>
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
//=================================================================================================
// Automatically resizable arrays
//
x->cap = size;
return x;
}
-
+
};
Vec_t* ref;
altvec (altvec<T>& 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:
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 () {
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(); }
};
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
-#endif
+#endif /* CVC4_MiniSat_BoxedVec_h */
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 <cassert>
+
+namespace CVC4 {
+namespace prop {
+namespace minisat {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
indices[n] = heap.size();
heap.push(n);
- percolateUp(indices[n]);
+ percolateUp(indices[n]);
}
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);
}
};
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
//=================================================================================================
-#endif
+#endif /* CVC4_MiniSat_Heap_h */
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 <stdint.h>
#include "Vec.h"
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
//=================================================================================================
// Default hash/equals functions
//
cap = newsize;
}
-
+
public:
Map () : table(NULL), cap(0), size(0) {}
for (int i = 0; i < ps.size(); i++)
if (equals(ps[i].key, k)){
d = ps[i].data;
- return true; }
+ return true; }
return false;
}
}
};
-#endif
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Map_h */
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 {
+
//=================================================================================================
//};
//=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Queue_h */
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
//=================================================================================================
-#endif
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#endif /* CVC4_MiniSat_Sort_h */
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 <cstdlib>
#include <cassert>
#include <new>
+namespace CVC4 {
+namespace prop {
+namespace minisat {
+
//=================================================================================================
// Automatically resizable arrays
//
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 */
//=================================================================================================
// 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)
}
-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();
-bool SimpSolver::addClause(vec<Lit>& ps)
+bool SimpSolver::addClause(vec<Lit>& ps, ClauseType type)
{
for (int i = 0; i < ps.size(); i++)
if (isEliminated(var(ps[i])))
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){
void SimpSolver::removeClause(Clause& c)
{
+ Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
assert(!c.learnt());
if (use_simplification)
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;
}
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:;
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:;
}
uncheckedEnqueue(~c[i]);
}
- bool result = propagate() != NULL;
+ bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL;
cancelUntil(0);
return result;
}
else
l = c[i];
- if (propagate() != NULL){
+ if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){
cancelUntil(0);
asymm_lits++;
if (!strengthenClause(c, l))
vec<Lit> 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.
clause.push(c[j]);
remembered_clauses++;
- check(addClause(clause));
+ check(addClause(clause, CLAUSE_PROBLEM));
free(&c);
}
}else
fprintf(stderr, "could not open file %s\n", file);
}
+
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
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 <cstdio>
+#include <cassert>
+
+#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<Lit>& ps);
+ Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false);
+ bool addClause (vec<Lit>& ps, ClauseType type);
// Variable mode:
//
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<Lit> 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 */
projects / cvc5.git / commitdiff