From dc4b8296ded0a2288fbfeb71b9ded9217bad6b86 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 4 Feb 2010 23:50:23 +0000 Subject: [PATCH] beautification of the prop engine --- src/expr/node.cpp | 17 ++++ src/expr/node.h | 1 + src/prop/cnf_stream.cpp | 195 ++++++++++++++------------------------- src/prop/cnf_stream.h | 73 ++++++++------- src/prop/prop_engine.cpp | 78 ++++++++-------- src/prop/prop_engine.h | 92 +++++++++--------- src/prop/sat.h | 50 ++++++++++ src/smt/smt_engine.cpp | 23 +++-- src/smt/smt_engine.h | 15 +-- 9 files changed, 275 insertions(+), 269 deletions(-) diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 72ad61e95..6f1c525ca 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -37,6 +37,23 @@ bool Node::isNull() const { return d_ev == &NodeValue::s_null; } +////FIXME: This function is a major hack! Should be changed ASAP +////TODO: Should use positive definition, i.e. what kinds are atomic. +bool Node::isAtomic() const { + switch(getKind()) { + case NOT: + case XOR: + case ITE: + case IFF: + case IMPLIES: + case OR: + case AND: + return false; + default: + return true; + } +} + Node::Node() : d_ev(&NodeValue::s_null) { // No refcount needed diff --git a/src/expr/node.h b/src/expr/node.h index 63bacaa52..3b0cb8abb 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -153,6 +153,7 @@ public: inline void toStream(std::ostream&) const; bool isNull() const; + bool isAtomic() const; /** * Very basic pretty printer for Node. diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e333543b4..b4a0a297e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -22,36 +22,11 @@ #include -using namespace CVC4::prop::minisat; using namespace std; namespace CVC4 { namespace prop { -bool atomic(const Node & n); - - -static void printVar(ostream & out, Var v){ - out << v; -} - -static void printLit(ostream & out, Lit l) { - const char * s = (sign(l))?"~":" "; - out << s << var(l); -} - - -static void printClause(ostream & out, vec & c) { - out << "clause:"; - for(int i=0;i & c) { - Debug("cnf") << "Inserting into stream "; - printClause(Debug("cnf"),c); - +void CnfStream::insertClauseIntoStream(SatClause& c) { + Debug("cnf") << "Inserting into stream " << c << endl; d_propEngine->assertClause(c); } -void CnfStream::insertClauseIntoStream(minisat::Lit a) { - vec clause(1); +void CnfStream::insertClauseIntoStream(SatLiteral a) { + SatClause clause(1); clause[0] = a; insertClauseIntoStream(clause); } -void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b) { - vec clause(2); +void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b) { + SatClause clause(2); clause[0] = a; clause[1] = b; insertClauseIntoStream(clause); } -void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b, - minisat::Lit c) { - vec clause(3); +void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c) { + SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; insertClauseIntoStream(clause); } -bool CnfStream::isCached(const Node & n) const { +bool CnfStream::isCached(const Node& n) const { return d_translationCache.find(n) != d_translationCache.end(); } -Lit CnfStream::lookupInCache(const Node & n) const { +SatLiteral CnfStream::lookupInCache(const Node& n) const { Assert(isCached(n), - "Node is not in cnf translation cache"); + "Node is not in cnf translation cache"); return d_translationCache.find(n)->second; } @@ -104,28 +74,24 @@ void CnfStream::flushCache() { d_translationCache.clear(); } -void CnfStream::cacheTranslation(const Node & node, Lit lit) { - Debug("cnf") << "cacheing translation "<< node << " to "; - printLit(Debug("cnf"),lit); - Debug("cnf") << endl; - +void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) { + Debug("cnf") << "caching translation " << node << " to " << lit << endl; d_translationCache.insert(make_pair(node, lit)); } -Lit CnfStream::aquireAndRegister(const Node & node, bool atom) { - Var v = atom ? - d_propEngine->registerAtom(node) - : d_propEngine->requestFreshVar(); - Lit l(v); - cacheTranslation(node, l); - return l; +SatLiteral CnfStream::aquireAndRegister(const Node& node, bool atom) { + SatVariable var = atom ? d_propEngine->registerAtom(node) + : d_propEngine->requestFreshVar(); + SatLiteral lit(var); + cacheTranslation(node, lit); + return lit; } -bool CnfStream::isAtomMapped(const Node & n) const{ +bool CnfStream::isAtomMapped(const Node& n) const { return d_propEngine->isAtomMapped(n); } - -Var CnfStream::lookupAtom(const Node & n) const{ + +SatVariable CnfStream::lookupAtom(const Node& n) const { return d_propEngine->lookupAtom(n); } @@ -135,12 +101,12 @@ Var CnfStream::lookupAtom(const Node & n) const{ /***********************************************/ /***********************************************/ -Lit TseitinCnfStream::handleAtom(const Node & n) { - Assert(atomic(n), "handleAtom(n) expects n to be an atom"); +SatLiteral TseitinCnfStream::handleAtom(const Node& n) { + Assert(n.isAtomic(), "handleAtom(n) expects n to be an atom"); Debug("cnf") << "handling atom" << endl; - Lit l = aquireAndRegister(n, true); + SatLiteral l = aquireAndRegister(n, true); switch(n.getKind()) { /* TRUE and FALSE are handled specially. */ case TRUE: insertClauseIntoStream(l); @@ -154,13 +120,13 @@ Lit TseitinCnfStream::handleAtom(const Node & n) { return l; } -Lit TseitinCnfStream::handleXor(const Node & n) { +SatLiteral TseitinCnfStream::handleXor(const Node& n) { // n: a XOR b - Lit a = recTransform(n[0]); - Lit b = recTransform(n[1]); + SatLiteral a = recTransform(n[0]); + SatLiteral b = recTransform(n[1]); - Lit l = aquireAndRegister(n); + SatLiteral l = aquireAndRegister(n); insertClauseIntoStream(a, b, ~l); insertClauseIntoStream(a, ~b, l); @@ -174,27 +140,27 @@ Lit TseitinCnfStream::handleXor(const Node & n) { size of the number of children of n. */ void TseitinCnfStream::mapRecTransformOverChildren(const Node& n, - vec & target) { - Assert(target.size() == n.getNumChildren(), - "Size of the children must be the same the constructed clause"); + SatClause& target) { + Assert((unsigned)target.size() == n.getNumChildren(), + "Size of the children must be the same the constructed clause"); int i = 0; Node::iterator subExprIter = n.begin(); while(subExprIter != n.end()) { - Lit equivalentLit = recTransform(*subExprIter); + SatLiteral equivalentLit = recTransform(*subExprIter); target[i] = equivalentLit; ++subExprIter; ++i; } } -Lit TseitinCnfStream::handleOr(const Node& n) { +SatLiteral TseitinCnfStream::handleOr(const Node& n) { //child_literals - vec lits(n.getNumChildren()); + SatClause lits(n.getNumChildren()); mapRecTransformOverChildren(n, lits); - Lit e = aquireAndRegister(n); + SatLiteral e = aquireAndRegister(n); /* e <-> (a1 | a2 | a3 | ...) *: e -> (a1 | a2 | a3 | ...) @@ -207,11 +173,10 @@ Lit TseitinCnfStream::handleOr(const Node& n) { * : (e | ~a1) & (e |~a2) & (e & ~a3) & ... */ - vec c(1 + lits.size()); - + SatClause c(1 + lits.size()); for(int index = 0; index < lits.size(); ++index) { - Lit a = lits[index]; + SatLiteral a = lits[index]; c[index] = a; insertClauseIntoStream(e, ~a); } @@ -224,15 +189,15 @@ Lit TseitinCnfStream::handleOr(const Node& n) { /* TODO: this only supports 2-ary <=> nodes atm. * Should this be changed? */ -Lit TseitinCnfStream::handleIff(const Node& n) { - Assert(n.getKind() == IFF); +SatLiteral TseitinCnfStream::handleIff(const Node& n) { + Assert(n.getKind() == IFF); Assert(n.getNumChildren() == 2); // n: a <=> b; - Lit a = recTransform(n[0]); - Lit b = recTransform(n[1]); + SatLiteral a = recTransform(n[0]); + SatLiteral b = recTransform(n[1]); - Lit l = aquireAndRegister(n); + SatLiteral l = aquireAndRegister(n); /* l <-> (a<->b) * : l -> ((a-> b) & (b->a)) @@ -254,16 +219,16 @@ Lit TseitinCnfStream::handleIff(const Node& n) { return l; } -Lit TseitinCnfStream::handleAnd(const Node& n) { - Assert(n.getKind() == AND); +SatLiteral TseitinCnfStream::handleAnd(const Node& n) { + Assert(n.getKind() == AND); Assert(n.getNumChildren() >= 1); //TODO: we know the exact size of the this. //Dynamically allocated array would have less overhead no? - vec lits(n.getNumChildren()); + SatClause lits(n.getNumChildren()); mapRecTransformOverChildren(n, lits); - Lit e = aquireAndRegister(n); + SatLiteral e = aquireAndRegister(n); /* e <-> (a1 & a2 & a3 & ...) * : e -> (a1 & a2 & a3 & ...) @@ -276,9 +241,9 @@ Lit TseitinCnfStream::handleAnd(const Node& n) { * : e | ~a1 | ~a2 | ~a3 | ... */ - vec c(lits.size()+1); + SatClause c(lits.size() + 1); for(int index = 0; index < lits.size(); ++index) { - Lit a = lits[index]; + SatLiteral a = lits[index]; c[index] = (~a); insertClauseIntoStream(~e, a); } @@ -289,15 +254,15 @@ Lit TseitinCnfStream::handleAnd(const Node& n) { return e; } -Lit TseitinCnfStream::handleImplies(const Node & n) { +SatLiteral TseitinCnfStream::handleImplies(const Node& n) { Assert(n.getKind() == IMPLIES); Assert(n.getNumChildren() == 2); // n: a => b; - Lit a = recTransform(n[0]); - Lit b = recTransform(n[1]); + SatLiteral a = recTransform(n[0]); + SatLiteral b = recTransform(n[1]); - Lit l = aquireAndRegister(n); + SatLiteral l = aquireAndRegister(n); /* l <-> (a->b) * (l -> (a->b)) & (l <- (a->b)) @@ -319,31 +284,29 @@ Lit TseitinCnfStream::handleImplies(const Node & n) { return l; } -Lit TseitinCnfStream::handleNot(const Node & n) { +SatLiteral TseitinCnfStream::handleNot(const Node& n) { Assert(n.getKind() == NOT); Assert(n.getNumChildren() == 1); // n : NOT m Node m = n[0]; - Lit equivM = recTransform(m); + SatLiteral equivM = recTransform(m); - Lit equivN = ~equivM; + SatLiteral equivN = ~equivM; cacheTranslation(n, equivN); return equivN; } -//FIXME: This function is a major hack! Should be changed ASAP -//Assumes binary no else if branchs, and that ITEs -Lit TseitinCnfStream::handleIte(const Node & n) { +SatLiteral TseitinCnfStream::handleIte(const Node& n) { Assert(n.getKind() == ITE); Assert(n.getNumChildren() == 3); // n : IF c THEN t ELSE f ENDIF; - Lit c = recTransform(n[0]); - Lit t = recTransform(n[1]); - Lit f = recTransform(n[2]); + SatLiteral c = recTransform(n[0]); + SatLiteral t = recTransform(n[1]); + SatLiteral f = recTransform(n[2]); // d <-> IF c THEN tB ELSE fb // : d -> (c & tB) | (~c & fB) @@ -361,7 +324,7 @@ Lit TseitinCnfStream::handleIte(const Node & n) { // : ((~c | ~t)& ( c |~fb)) | d // : (~c | ~ t | d) & (c | ~f | d) - Lit d = aquireAndRegister(n); + SatLiteral d = aquireAndRegister(n); insertClauseIntoStream(~d, ~c, t); insertClauseIntoStream(~d, c, f); @@ -372,45 +335,27 @@ Lit TseitinCnfStream::handleIte(const Node & n) { return d; } -//FIXME: This function is a major hack! Should be changed ASAP -//TODO: Should be moved. Not sure where... -//TODO: Should use positive definition, i.e. what kinds are atomic. -bool atomic(const Node & n) { - switch(n.getKind()) { - case NOT: - case XOR: - case ITE: - case IFF: - case IMPLIES: - case OR: - case AND: - return false; - default: - return true; - } -} - -//TODO: The following code assumes everthing is either +//TODO: The following code assumes everything is either // an atom or is a logical connective. This ignores quantifiers and lambdas. -Lit TseitinCnfStream::recTransform(const Node & n) { +SatLiteral TseitinCnfStream::recTransform(const Node& n) { if(isCached(n)) { return lookupInCache(n); } - if(atomic(n)) { - - /* Unforunately we need to potentially allow + if(n.isAtomic()) { + + /* Unfortunately we need to potentially allow * for n to be to the Atom <-> Var map but not the * translation cache. * This is because the translation cache can be flushed. * It is really not clear where this check should go, but * it needs to be done. */ - if(isAtomMapped(n)){ + if(isAtomMapped(n)) { /* Puts the atom in the translation cache after looking it up. * Avoids doing 2 map lookups for this atom in the future. */ - Lit l(lookupAtom(n)); + SatLiteral l(lookupAtom(n)); cacheTranslation(n, l); return l; } @@ -438,8 +383,8 @@ Lit TseitinCnfStream::recTransform(const Node & n) { } } -void TseitinCnfStream::convertAndAssert(const Node & n) { - Lit e = recTransform(n); +void TseitinCnfStream::convertAndAssert(const Node& n) { + SatLiteral e = recTransform(n); insertClauseIntoStream(e); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 97f1ee801..0cc8cb425 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -23,19 +23,15 @@ #define __CVC4__CNF_STREAM_H #include "expr/node.h" -#include "prop/minisat/simp/SimpSolver.h" -#include "prop/minisat/core/SolverTypes.h" -#include "prop/prop_engine.h" +#include "prop/sat.h" #include -namespace CVC4 { -class PropEngine; -} - namespace CVC4 { namespace prop { +class PropEngine; + /** * Comments for the behavior of the whole class... * @author Tim King @@ -58,44 +54,46 @@ private: * for correctness. This can be flushed when memory is under pressure. * TODO: Use attributes when they arrive */ - std::map d_translationCache; + std::map d_translationCache; protected: - bool isAtomMapped(const Node & n) const; - minisat::Var lookupAtom(const Node & n) const; + + bool isAtomMapped(const Node& n) const; + + SatVariable lookupAtom(const Node& node) const; /** * Uniform interface for sending a clause back to d_propEngine. * May want to have internal data-structures later on */ - void insertClauseIntoStream(minisat::vec & c); - void insertClauseIntoStream(minisat::Lit a); - void insertClauseIntoStream(minisat::Lit a, minisat::Lit b); - void insertClauseIntoStream(minisat::Lit a, minisat::Lit b, minisat::Lit c); + void insertClauseIntoStream(SatClause& clause); + void insertClauseIntoStream(SatLiteral a); + void insertClauseIntoStream(SatLiteral a, SatLiteral b); + void insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c); //utilities for the translation cache; - bool isCached(const Node & n) const; + bool isCached(const Node& node) const; /** * Method comments... * @param n * @return returns ... */ - minisat::Lit lookupInCache(const Node & n) const; - + SatLiteral lookupInCache(const Node& n) const; //negotiates the mapping of atoms to literals with PropEngine - void cacheTranslation(const Node & node, minisat::Lit lit); - minisat::Lit aquireAndRegister(const Node & n, bool atom = false); + void cacheTranslation(const Node& node, SatLiteral lit); + + SatLiteral aquireAndRegister(const Node& node, bool atom = false); public: + /** * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses * and sends them to the given PropEngine. - * @param pe + * @param propEngine */ - CnfStream(CVC4::PropEngine *pe); - + CnfStream(PropEngine* propEngine); /** * Empties the internal translation cache. @@ -104,9 +102,9 @@ public: /** * Converts and asserts a formula. - * @param n node to convert and assert + * @param node node to convert and assert */ - virtual void convertAndAssert(const Node & n) = 0; + virtual void convertAndAssert(const Node& node) = 0; }; /* class CnfStream */ @@ -123,8 +121,10 @@ public: class TseitinCnfStream : public CnfStream { public: - void convertAndAssert(const Node & n); - TseitinCnfStream(CVC4::PropEngine *pe); + + void convertAndAssert(const Node& node); + + TseitinCnfStream(PropEngine* propEngine); private: @@ -139,15 +139,15 @@ private: * * handleX( n ) can assume that n is not in d_translationCache */ - minisat::Lit handleAtom(const Node & n); - minisat::Lit handleNot(const Node & n); - minisat::Lit handleXor(const Node & n); - minisat::Lit handleImplies(const Node & n); - minisat::Lit handleIff(const Node & n); - minisat::Lit handleIte(const Node & n); + SatLiteral handleAtom(const Node& node); + SatLiteral handleNot(const Node& node); + SatLiteral handleXor(const Node& node); + SatLiteral handleImplies(const Node& node); + SatLiteral handleIff(const Node& node); + SatLiteral handleIte(const Node& node); - minisat::Lit handleAnd(const Node& n); - minisat::Lit handleOr(const Node& n); + SatLiteral handleAnd(const Node& node); + SatLiteral handleOr(const Node& node); /** * Maps recTransform over the children of a node. This is very useful for @@ -159,11 +159,10 @@ private: * @param n ... * @param target ... */ - void mapRecTransformOverChildren(const Node& n, - minisat::vec & target); + void mapRecTransformOverChildren(const Node& node, SatClause& target); //Recursively dispatches the various Kinds to the appropriate handler. - minisat::Lit recTransform(const Node & n); + SatLiteral recTransform(const Node& node); }; /* class TseitinCnfStream */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ad38c2a1f..5889ba504 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -17,9 +17,6 @@ #include "theory/theory_engine.h" #include "util/decision_engine.h" -#include "prop/minisat/mtl/Vec.h" -#include "prop/minisat/simp/SimpSolver.h" -#include "prop/minisat/core/SolverTypes.h" #include "util/Assert.h" #include "util/output.h" #include "util/options.h" @@ -28,44 +25,42 @@ #include #include -using namespace CVC4::prop::minisat; using namespace std; namespace CVC4 { +namespace prop { -PropEngine::PropEngine(const Options* opts, - DecisionEngine& de, - TheoryEngine& te) : +PropEngine::PropEngine(const Options* opts, DecisionEngine* de, + TheoryEngine* te) : d_opts(opts), - d_de(de), - d_te(te), - d_restartMayBeNeeded(false){ - d_sat = new Solver(); + d_de(de), + d_te(te), + d_restartMayBeNeeded(false) { + d_sat = new SatSolver(); d_cnfStream = new CVC4::prop::TseitinCnfStream(this); } -PropEngine::~PropEngine(){ +PropEngine::~PropEngine() { delete d_cnfStream; delete d_sat; } - -void PropEngine::assertClause(vec & c){ +void PropEngine::assertClause(SatClause& clause) { /*we can also here add a context dependent queue of assertions *for restarting the sat solver */ //TODO assert that each lit has been mapped to an atom or requested - d_sat->addClause(c); + d_sat->addClause(clause); } -Var PropEngine::registerAtom(const Node & n){ - Var v = requestFreshVar(); - d_atom2var.insert(make_pair(n,v)); - d_var2atom.insert(make_pair(v,n)); +SatVariable PropEngine::registerAtom(const Node & n) { + SatVariable v = requestFreshVar(); + d_atom2var.insert(make_pair(n, v)); + d_var2atom.insert(make_pair(v, n)); return v; } -Var PropEngine::requestFreshVar(){ +SatVariable PropEngine::requestFreshVar() { return d_sat->newVar(); } @@ -79,20 +74,19 @@ void PropEngine::assertFormula(const Node& node) { d_assertionList.push_back(node); } -void PropEngine::restart(){ +void PropEngine::restart() { delete d_sat; - d_sat = new Solver(); + d_sat = new SatSolver(); d_cnfStream->flushCache(); d_atom2var.clear(); d_var2atom.clear(); - for(vector::iterator iter = d_assertionList.begin(); - iter != d_assertionList.end(); ++iter){ + for(vector::iterator iter = d_assertionList.begin(); iter + != d_assertionList.end(); ++iter) { d_cnfStream->convertAndAssert(*iter); } } - Result PropEngine::solve() { if(d_restartMayBeNeeded) restart(); @@ -100,7 +94,7 @@ Result PropEngine::solve() { d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1; bool result = d_sat->solve(); - if(!result){ + if(!result) { d_restartMayBeNeeded = true; } @@ -109,22 +103,22 @@ Result PropEngine::solve() { return Result(result ? Result::SAT : Result::UNSAT); } +void PropEngine::assertLit(SatLiteral lit) { + SatVariable var = literalToVariable(lit); + if(isVarMapped(var)) { + Node atom = lookupVar(var); + //Theory* t = ...; + //t must be the corresponding theory for the atom + + //Literal l(atom, sign(l)); + //t->assertLiteral(l ); + } +} - void PropEngine::assertLit(Lit l){ - Var v = var(l); - if(isVarMapped(v)){ - Node atom = lookupVar(v); - //Theory* t = ...; - //t must be the corresponding theory for the atom - - //Literal l(atom, sign(l)); - //t->assertLiteral(l ); - } - } - - void PropEngine::signalBooleanPropHasEnded(){} - //TODO decisionEngine should be told - //TODO theoryEngine to call lightweight theory propogation - +void PropEngine::signalBooleanPropHasEnded() { +} +//TODO decisionEngine should be told +//TODO theoryEngine to call lightweight theory propogation +}/* prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index afeee3a41..d60771e95 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -21,76 +21,72 @@ #include "expr/node.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" -#include "prop/minisat/simp/SimpSolver.h" -#include "prop/minisat/core/SolverTypes.h" +#include "sat.h" #include "util/result.h" +#include "util/options.h" #include -#include "prop/cnf_stream.h" namespace CVC4 { - namespace prop { - class CnfStream; - } +namespace prop { - class Options; -} - -namespace CVC4 { +class CnfStream; // In terms of abstraction, this is below (and provides services to) // Prover and above (and requires the services of) a specific // propositional solver, DPLL or otherwise. class PropEngine { + + friend class CnfStream; + + /** The global options */ const Options *d_opts; - DecisionEngine &d_de; - TheoryEngine &d_te; + /** The decision engine we will be using */ + DecisionEngine *d_de; + /** The theory engine we will be using */ + TheoryEngine *d_te; - friend class CVC4::prop::CnfStream; - /** * The SAT solver. */ - CVC4::prop::minisat::Solver* d_sat; - - std::map d_atom2var; - std::map d_var2atom; + SatSolver* d_sat; + std::map d_atom2var; + std::map d_var2atom; /** * Requests a fresh variable from d_sat, v. * Adds mapping of n -> v to d_node2var, and * a mapping of v -> n to d_var2node. */ - CVC4::prop::minisat::Var registerAtom(const Node & n); + SatVariable registerAtom(const Node& node); /** * Requests a fresh variable from d_sat. */ - CVC4::prop::minisat::Var requestFreshVar(); - + SatVariable requestFreshVar(); /** * Returns true iff this Node is in the atom to variable mapping. * @param n the Node to lookup * @return true iff this Node is in the atom to variable mapping. */ - bool isAtomMapped(const Node & n) const; + bool isAtomMapped(const Node& node) const; /** * Returns the variable mapped by the atom Node. * @param n the atom to do the lookup by * @return the corresponding variable */ - CVC4::prop::minisat::Var lookupAtom(const Node & n) const; + SatVariable lookupAtom(const Node& node) const; /** * Flags whether the solver may need to have its state reset before * solving occurs */ bool d_restartMayBeNeeded; - + /** * Cleans existing state in the PropEngine and reinitializes the state. */ @@ -101,47 +97,44 @@ class PropEngine { */ std::vector d_assertionList; - /** - * Returns true iff the minisat var has been mapped to an atom. - * @param v variable to check if it is mapped + * Returns true iff the variable from the sat solver has been mapped to + * an atom. + * @param var variable to check if it is mapped * @return returns true iff the minisat var has been mapped. */ - bool isVarMapped(CVC4::prop::minisat::Var v) const; + bool isVarMapped(SatVariable var) const; /** * Returns the atom mapped by the variable v. - * @param v the variable to do the lookup by + * @param var the variable to do the lookup by * @return an atom */ - Node lookupVar(CVC4::prop::minisat::Var v) const; - - + Node lookupVar(SatVariable var) const; /** - * Asserts an internally constructed clause. - * Each literal is assumed to be in the 1:1 mapping contained in d_node2lit & d_lit2node. - * @param c the clause to be asserted. + * Asserts an internally constructed clause. Each literal is assumed to be in + * the 1-1 mapping contained in d_node2lit and d_lit2node. + * @param clause the clause to be asserted. */ - void assertClause(CVC4::prop::minisat::vec & c); + void assertClause(SatClause& clause); - /** The CNF converter in use */ - CVC4::prop::CnfStream *d_cnfStream; - + CnfStream* d_cnfStream; - void assertLit(CVC4::prop::minisat::Lit l); + void assertLit(SatLiteral lit); void signalBooleanPropHasEnded(); public: - /** * Create a PropEngine with a particular decision and theory engine. */ - CVC4_PUBLIC PropEngine(const CVC4::Options* opts, - CVC4::DecisionEngine&, - CVC4::TheoryEngine&); + PropEngine(const Options* opts, DecisionEngine*, TheoryEngine*); + + /** + * Destructor. + */ CVC4_PUBLIC ~PropEngine(); /** @@ -157,28 +150,27 @@ public: */ Result solve(); - };/* class PropEngine */ - -inline bool PropEngine::isAtomMapped(const Node & n) const{ +inline bool PropEngine::isAtomMapped(const Node & n) const { return d_atom2var.find(n) != d_atom2var.end(); } -inline CVC4::prop::minisat::Var PropEngine::lookupAtom(const Node & n) const{ +inline SatVariable PropEngine::lookupAtom(const Node & n) const { Assert(isAtomMapped(n)); return d_atom2var.find(n)->second; } -inline bool PropEngine::isVarMapped(CVC4::prop::minisat::Var v) const { +inline bool PropEngine::isVarMapped(SatVariable v) const { return d_var2atom.find(v) != d_var2atom.end(); } -inline Node PropEngine::lookupVar(CVC4::prop::minisat::Var v) const { +inline Node PropEngine::lookupVar(SatVariable v) const { Assert(isVarMapped(v)); return d_var2atom.find(v)->second; } +}/* prop namespace */ }/* CVC4 namespace */ #endif /* __CVC4__PROP_ENGINE_H */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 679b9da8c..195323755 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -16,10 +16,60 @@ #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H +#define __CVC4_USE_MINISAT + +#ifdef __CVC4_USE_MINISAT + +#include "prop/minisat/core/Solver.h" +#include "prop/minisat/core/SolverTypes.h" + namespace CVC4 { namespace prop { +/** The solver we are using */ +typedef minisat::Solver SatSolver; + +/** Type of the SAT variables */ +typedef minisat::Var SatVariable; + +/** Type of the Sat literals */ +typedef minisat::Lit SatLiteral; + +/** Type of the SAT clauses */ +typedef minisat::vec SatClause; + +/** + * Returns the variable of the literal. + * @param lit the literal + */ +inline SatVariable literalToVariable(SatLiteral lit) { + return minisat::var(lit); +} + +inline bool literalSign(SatLiteral lit) { + return minisat::sign(lit); +} + +inline std::ostream& operator << (std::ostream& out, SatLiteral lit) { + const char * s = (literalSign(lit)) ? "~" : " "; + out << s << literalToVariable(lit); + return out; +} + +inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { + out << "clause:"; + for(int i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; +} + + }/* CVC4::prop namespace */ }/* CVC4 namespace */ +#endif + + #endif /* __CVC4__PROP__SAT_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1555acb7d..a04d16d06 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -13,11 +13,14 @@ **/ #include "smt/smt_engine.h" -#include "util/exception.h" #include "expr/command.h" -#include "util/output.h" #include "expr/node_builder.h" +#include "util/output.h" +#include "util/exception.h" #include "util/options.h" +#include "prop/prop_engine.h" + +using namespace CVC4::prop; namespace CVC4 { @@ -25,13 +28,17 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_assertions(), d_publicEm(em), d_nm(em->getNodeManager()), - d_opts(opts), - d_de(), - d_te(), - d_prop(opts, d_de, d_te) { + d_opts(opts) +{ + d_de = new DecisionEngine(); + d_te = new TheoryEngine(); + d_prop = new PropEngine(opts, d_de, d_te); } SmtEngine::~SmtEngine() { + delete d_prop; + delete d_te; + delete d_de; } void SmtEngine::doCommand(Command* c) { @@ -45,7 +52,7 @@ Node SmtEngine::preprocess(const Node& e) { void SmtEngine::processAssertionList() { for(unsigned i = 0; i < d_assertions.size(); ++i) { - d_prop.assertFormula(d_assertions[i]); + d_prop->assertFormula(d_assertions[i]); } d_assertions.clear(); } @@ -54,7 +61,7 @@ void SmtEngine::processAssertionList() { Result SmtEngine::check() { Debug("smt") << "SMT check()" << std::endl; processAssertionList(); - return d_prop.solve(); + return d_prop->solve(); } Result SmtEngine::quickCheck() { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 79a35a6a1..eb9384ca5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -19,14 +19,10 @@ #include #include "cvc4_config.h" -#include "expr/node.h" #include "expr/expr.h" -#include "expr/node_manager.h" -#include "expr/node_builder.h" #include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" -#include "prop/prop_engine.h" #include "util/decision_engine.h" // In terms of abstraction, this is below (and provides services to) @@ -37,6 +33,11 @@ namespace CVC4 { class Command; class Options; +class TheoryEngine; + +namespace prop { + class PropEngine; +} // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass @@ -125,13 +126,13 @@ private: const Options* d_opts; /** The decision engine */ - DecisionEngine d_de; + DecisionEngine* d_de; /** The decision engine */ - TheoryEngine d_te; + TheoryEngine* d_te; /** The propositional engine */ - PropEngine d_prop; + prop::PropEngine* d_prop; /** -- 2.30.2