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
inline void toStream(std::ostream&) const;
bool isNull() const;
+ bool isAtomic() const;
/**
* Very basic pretty printer for Node.
#include <queue>
-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<Lit> & c) {
- out << "clause:";
- for(int i=0;i<c.size();i++){
- out << " ";
- printLit(out, c[i]) ;
- }
- out << ";" << endl;
-}
-
-
-
CnfStream::CnfStream(PropEngine *pe) :
d_propEngine(pe) {
}
CnfStream(pe) {
}
-
-
-void CnfStream::insertClauseIntoStream(vec<Lit> & 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<Lit> 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<Lit> 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<Lit> 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;
}
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);
}
/***********************************************/
/***********************************************/
-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);
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);
size of the number of children of n.
*/
void TseitinCnfStream::mapRecTransformOverChildren(const Node& n,
- vec<Lit> & 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<Lit> 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 | ...)
* : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
*/
- vec<Lit> 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);
}
/* 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))
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<Lit> 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 & ...)
* : e | ~a1 | ~a2 | ~a3 | ...
*/
- vec<Lit> 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);
}
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))
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)
// : ((~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);
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;
}
}
}
-void TseitinCnfStream::convertAndAssert(const Node & n) {
- Lit e = recTransform(n);
+void TseitinCnfStream::convertAndAssert(const Node& n) {
+ SatLiteral e = recTransform(n);
insertClauseIntoStream(e);
}
#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 <map>
-namespace CVC4 {
-class PropEngine;
-}
-
namespace CVC4 {
namespace prop {
+class PropEngine;
+
/**
* Comments for the behavior of the whole class...
* @author Tim King <taking@cs.nyu.edu>
* for correctness. This can be flushed when memory is under pressure.
* TODO: Use attributes when they arrive
*/
- std::map<Node, minisat::Lit> d_translationCache;
+ std::map<Node, SatLiteral> 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<minisat::Lit> & 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.
/**
* 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 */
class TseitinCnfStream : public CnfStream {
public:
- void convertAndAssert(const Node & n);
- TseitinCnfStream(CVC4::PropEngine *pe);
+
+ void convertAndAssert(const Node& node);
+
+ TseitinCnfStream(PropEngine* propEngine);
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
* @param n ...
* @param target ...
*/
- void mapRecTransformOverChildren(const Node& n,
- minisat::vec<minisat::Lit> & 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 */
#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"
#include <utility>
#include <map>
-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<Lit> & 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();
}
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<Node>::iterator iter = d_assertionList.begin();
- iter != d_assertionList.end(); ++iter){
+ for(vector<Node>::iterator iter = d_assertionList.begin(); iter
+ != d_assertionList.end(); ++iter) {
d_cnfStream->convertAndAssert(*iter);
}
}
-
Result PropEngine::solve() {
if(d_restartMayBeNeeded)
restart();
d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
bool result = d_sat->solve();
- if(!result){
+ if(!result) {
d_restartMayBeNeeded = true;
}
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 */
#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 <map>
-#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<Node, CVC4::prop::minisat::Var> d_atom2var;
- std::map<CVC4::prop::minisat::Var, Node> d_var2atom;
+ SatSolver* d_sat;
+ std::map<Node, SatVariable> d_atom2var;
+ std::map<SatVariable, Node> 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.
*/
*/
std::vector<Node> 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<CVC4::prop::minisat::Lit> & 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();
/**
*/
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 */
#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<SatLiteral> 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 */
**/
#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 {
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) {
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();
}
Result SmtEngine::check() {
Debug("smt") << "SMT check()" << std::endl;
processAssertionList();
- return d_prop.solve();
+ return d_prop->solve();
}
Result SmtEngine::quickCheck() {
#include <vector>
#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)
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
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;
/**
projects / cvc5.git / commitdiff