diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 136 |
1 files changed, 31 insertions, 105 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index bc46e39d5..875d0cd16 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -13,6 +13,8 @@ **/ #include "prop/prop_engine.h" +#include "prop/cnf_stream.h" + #include "theory/theory_engine.h" #include "util/decision_engine.h" #include "prop/minisat/mtl/Vec.h" @@ -30,123 +32,47 @@ using namespace std; namespace CVC4 { PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) : - d_de(de), d_te(te) { + d_de(de), + d_te(te){ + d_cnfStream = new CVC4::prop::TseitinCnfStream(this); +} + +PropEngine::~PropEngine(){ + delete d_cnfStream; +} + + +void PropEngine::assertClause(vec<Lit> & c){ + /*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); } -void PropEngine::addVars(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) { - Debug("prop") << "adding vars to " << e << endl; - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - Debug("prop") << "expr " << *i << endl; - if((*i).getKind() == VARIABLE) { - if(vars->find(*i) == vars->end()) { - Var v = minisat->newVar(); - Debug("prop") << "adding var " << *i << " <--> " << v << endl; - (*vars).insert(make_pair(*i, v)); - (*varsReverse).insert(make_pair(v, *i)); - } else Debug("prop") << "using var " << *i << " <--> " << (*vars)[*i] << endl; - } else addVars(minisat, vars, varsReverse, *i); - } +void PropEngine::registerAtom(const Node & n, Lit l){ + d_atom2lit.insert(make_pair(n,l)); + d_lit2atom.insert(make_pair(l,n)); } -static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>* c) { - if(e.getKind() == VARIABLE) { - map<Node, Var>::iterator v = vars->find(e); - Assert(v != vars->end()); - c->push(Lit(v->second, false)); - return; - } - if(e.getKind() == NOT) { - Assert(e.getNumChildren() == 1); - Node child = *e.begin(); - Assert(child.getKind() == VARIABLE); - map<Node, Var>::iterator v = vars->find(child); - Assert(v != vars->end()); - c->push(Lit(v->second, true)); - return; - } - if(e.getKind() == OR) { - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - doAtom(minisat, vars, *i, c); - } - return; - } - Unhandled(e.getKind()); +Lit PropEngine::requestFreshLit(){ + Var v = d_sat.newVar(); + Lit l(v,false); + return l; } -static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) { - vec<Lit> c; - Debug("prop") << " " << e << endl; - if(e.getKind() == VARIABLE || e.getKind() == NOT) { - doAtom(minisat, vars, e, &c); - } else if(e.getKind() == FALSE) { - // inconsistency - Notice() << "adding FALSE clause" << endl; - Var v = minisat->newVar(); - c.push(Lit(v, true)); - minisat->addClause(c); - Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl; - c.clear(); - c.push(Lit(v, false)); - minisat->addClause(c); - Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl; - } else if(e.getKind() == TRUE) { - Notice() << "adding TRUE clause (do nothing)" << endl; - // do nothing - } else { - Assert(e.getKind() == OR); - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - Debug("prop") << " " << *i << endl; - doAtom(minisat, vars, *i, &c); - } - } - Notice() << "added clause of length " << c.size() << endl; - for(int i = 0; i < c.size(); ++i) - Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]); - Notice() << " [["; - for(int i = 0; i < c.size(); ++i) - Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])]; - Notice() << " ]] " << endl; - minisat->addClause(c); +void PropEngine::assertFormula(const Node& node) { + d_cnfStream->convertAndAssert(node); } -void PropEngine::solve(Node e) { - // FIXME: when context mgr comes online, keep the solver around - // between solve() calls if we can - CVC4::prop::minisat::SimpSolver sat; - std::map<Node, CVC4::prop::minisat::Var> vars; - std::map<CVC4::prop::minisat::Var, Node> varsReverse; +void PropEngine::solve() { - Debug("prop") << "SOLVING " << e << endl; - addVars(&sat, &vars, &varsReverse, e); - if(e.getKind() == AND) { - Debug("prop") << "AND" << endl; - for(Node::iterator i = e.begin(); i != e.end(); ++i) - doClause(&sat, &vars, &varsReverse, *i); - } else doClause(&sat, &vars, &varsReverse, e); + //TODO: may need to restart if a previous query returned false - sat.verbosity = 1; - bool result = sat.solve(); + d_sat.verbosity = 1; + bool result = d_sat.solve(); Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; - if(result) { - Notice() << "model:" << endl; - for(int i = 0; i < sat.model.size(); ++i) - Notice() << " " << toInt(sat.model[i]); - Notice() << endl; - for(int i = 0; i < sat.model.size(); ++i) - Notice() << " " << varsReverse[i] << " is " - << (sat.model[i] == l_False ? "FALSE" : - (sat.model[i] == l_Undef ? "UNDEF" : - "TRUE")) << endl; - } else { - Notice() << "conflict:" << endl; - for(int i = 0; i < sat.conflict.size(); ++i) - Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << var(sat.conflict[i]); - Notice() << " [["; - for(int i = 0; i < sat.conflict.size(); ++i) - Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << varsReverse[var(sat.conflict[i])]; - Notice() << " ]] " << endl; - } } }/* CVC4 namespace */ |