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 */