diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
commit | 39b707ad22813c184da61c3e2337359ca8061797 (patch) | |
tree | f1e4f3476822c4da3f423dc114ca1583bdcf063e /src/prop | |
parent | e081fe6309b02a23b81330c151876f04ad774465 (diff) |
cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 52 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 8 |
2 files changed, 33 insertions, 27 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 16b807904..bc46e39d5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -30,21 +30,21 @@ using namespace std; namespace CVC4 { PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) : - d_de(de), d_te(te), d_sat() { + d_de(de), d_te(te) { } -void PropEngine::addVars(Node e) { +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(d_vars.find(*i) == d_vars.end()) { - Var v = d_sat.newVar(); + if(vars->find(*i) == vars->end()) { + Var v = minisat->newVar(); Debug("prop") << "adding var " << *i << " <--> " << v << endl; - d_vars.insert(make_pair(*i, v)); - d_varsReverse.insert(make_pair(v, *i)); - } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl; - } else addVars(*i); + (*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); } } @@ -110,35 +110,41 @@ static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, 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; + Debug("prop") << "SOLVING " << e << endl; - addVars(e); + addVars(&sat, &vars, &varsReverse, e); if(e.getKind() == AND) { Debug("prop") << "AND" << endl; for(Node::iterator i = e.begin(); i != e.end(); ++i) - doClause(&d_sat, &d_vars, &d_varsReverse, *i); - } else doClause(&d_sat, &d_vars, &d_varsReverse, e); + doClause(&sat, &vars, &varsReverse, *i); + } else doClause(&sat, &vars, &varsReverse, e); - d_sat.verbosity = 1; - bool result = d_sat.solve(); + sat.verbosity = 1; + bool result = sat.solve(); Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; if(result) { Notice() << "model:" << endl; - for(int i = 0; i < d_sat.model.size(); ++i) - Notice() << " " << toInt(d_sat.model[i]); + for(int i = 0; i < sat.model.size(); ++i) + Notice() << " " << toInt(sat.model[i]); Notice() << endl; - for(int i = 0; i < d_sat.model.size(); ++i) - Notice() << " " << d_varsReverse[i] << " is " - << (d_sat.model[i] == l_False ? "FALSE" : - (d_sat.model[i] == l_Undef ? "UNDEF" : + 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 < d_sat.conflict.size(); ++i) - Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]); + for(int i = 0; i < sat.conflict.size(); ++i) + Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << var(sat.conflict[i]); Notice() << " [["; - for(int i = 0; i < d_sat.conflict.size(); ++i) - Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])]; + for(int i = 0; i < sat.conflict.size(); ++i) + Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << varsReverse[var(sat.conflict[i])]; Notice() << " ]] " << endl; } } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6cb818d10..6e1f8cb61 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -35,11 +35,11 @@ namespace CVC4 { class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; - CVC4::prop::minisat::SimpSolver d_sat; - std::map<Node, CVC4::prop::minisat::Var> d_vars; - std::map<CVC4::prop::minisat::Var, Node> d_varsReverse; + //CVC4::prop::minisat::SimpSolver d_sat; + //std::map<Node, CVC4::prop::minisat::Var> d_vars; + //std::map<CVC4::prop::minisat::Var, Node> d_varsReverse; - void addVars(Node); + void addVars(CVC4::prop::minisat::SimpSolver*, std::map<Node, CVC4::prop::minisat::Var>*, std::map<CVC4::prop::minisat::Var, Node>*, Node); public: /** |