Switched cnf conversion to go through CnfStream.

6 files changed, 735 insertions, 112 deletions

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 3473de30f..fc0697eda 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -8,6 +8,9 @@ noinst_LTLIBRARIES = libprop.la
 libprop_la_SOURCES = \
 	prop_engine.cpp \
 	prop_engine.h \
-	sat.h
+	sat.h \
+	cnf_stream.h \
+	cnf_stream.cpp \
+	cnf_conversion.h
 
 SUBDIRS = minisat
diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h
new file mode 100644
index 000000000..924cae063
--- /dev/null
+++ b/src/prop/cnf_conversion.h
@@ -0,0 +1,46 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_conversion.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A type for describing possible CNF conversions.
+ **/
+
+#ifndef __CVC4__CNF_CONVERSION_H
+#define __CVC4__CNF_CONVERSION_H
+
+namespace CVC4 {
+
+enum CnfConversion {
+  CNF_DIRECT_EXPONENTIAL = 0,
+  CNF_VAR_INTRODUCTION = 1
+};
+
+inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
+  using namespace CVC4;
+
+  switch(c) {
+  case CNF_DIRECT_EXPONENTIAL:
+    out << "CNF_DIRECT_EXPONENTIAL";
+    break;
+  case CNF_VAR_INTRODUCTION:
+    out << "CNF_VAR_INTRODUCTION";
+    break;
+  default:
+    out << "UNKNOWN-CONVERTER!" << int(c);
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CNF_CONVERSION_H */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
new file mode 100644
index 000000000..73c3f6c01
--- /dev/null
+++ b/src/prop/cnf_stream.cpp
@@ -0,0 +1,421 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_stream.cpp
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A CNF converter that takes in asserts and has the side effect
+ ** of given an equisatisfiable stream of assertions to PropEngine.
+ **/
+
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+#include <queue>
+
+using namespace CVC4::prop::minisat;
+using namespace std;
+
+
+namespace CVC4 {
+namespace prop {
+
+CnfStream::CnfStream(PropEngine *pe) :
+  d_propEngine(pe){}
+  
+TseitinCnfStream::TseitinCnfStream(PropEngine *pe):
+  CnfStream(pe){}
+
+
+void CnfStream::insertClauseIntoStream(vec<Lit> & c){
+  d_propEngine->assertClause(c);
+}
+
+void CnfStream::insertClauseIntoStream(minisat::Lit a){
+  vec<Lit> clause(1);
+  clause[0] = a;
+  insertClauseIntoStream(clause);
+}
+void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b){
+  vec<Lit> 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);
+  clause[0] = a;
+  clause[1] = b;
+  clause[2] = c;
+  insertClauseIntoStream(clause);
+}
+
+bool CnfStream::isCached(const Node & n) const {
+  return d_translationCache.find(n) != d_translationCache.end();
+}
+
+Lit CnfStream::lookupInCache(const Node & n) const {
+  Assert(isCached(n));
+  return d_translationCache.find(n)->second;
+}
+
+void CnfStream::flushCache(){
+  d_translationCache.clear();
+}
+
+void CnfStream::registerMapping(const Node & node, Lit lit, bool atom){
+  //Prop engine does not need to know this mapping
+  d_translationCache.insert(make_pair(node,lit));
+  if(atom)
+    d_propEngine->registerAtom(node, lit);
+}
+
+Lit CnfStream::acquireFreshLit(const Node & n){
+  return d_propEngine->requestFreshLit();
+}
+
+Lit CnfStream::aquireAndRegister(const Node & node, bool atom){
+  Lit l = acquireFreshLit(node);
+  registerMapping(node, l, atom);
+  return l;
+}
+
+/***********************************************/
+/***********************************************/
+/************ End of CnfStream *****************/
+/***********************************************/
+/***********************************************/
+
+Lit TseitinCnfStream::handleAtom(const Node & n){
+  Lit l = aquireAndRegister(n, true);
+  switch(n.getKind()){ /* TRUE and FALSE are handled specially. */
+  case TRUE:
+    insertClauseIntoStream( l );
+    break;
+  case FALSE:
+    insertClauseIntoStream( ~l );
+    break;
+  default: //Does nothing else
+    break;
+  }
+  return l;
+}
+
+Lit TseitinCnfStream::handleXor(const Node & n){
+  // n: a XOR b
+  
+  Lit a = recTransform(n[0]);
+  Lit b = recTransform(n[1]);
+  
+  Lit l = aquireAndRegister(n);
+  
+  insertClauseIntoStream( a,  b, ~l);
+  insertClauseIntoStream( a, ~b,  l);
+  insertClauseIntoStream(~a,  b,  l);
+  insertClauseIntoStream(~a, ~b, ~l);
+  
+  return l;
+}
+
+  /* For a small efficiency boost target needs to already be allocated to have
+     size of the number of children of n.
+  */
+void  TseitinCnfStream::mapRecTransformOverChildren(const Node& n, vec<Lit> & target){
+  Assert(target.size() == n.getNumChildren());
+
+  int i = 0;
+  Node::iterator subExprIter = n.begin();
+  
+  while(subExprIter != n.end()){
+    Lit equivalentLit = recTransform(*subExprIter);
+    target[i] = equivalentLit;
+    ++subExprIter; ++i;
+  }
+}
+
+Lit TseitinCnfStream::handleOr(const Node& n){
+  //child_literals
+  vec<Lit> lits(n.getNumChildren());
+  mapRecTransformOverChildren(n, lits);
+  
+  Lit e = aquireAndRegister(n);
+  
+  /* e <-> (a1 | a2 | a3 | ...)
+   *: e -> (a1 | a2 | a3 | ...)
+   * : ~e | (
+   * : ~e | a1 | a2 | a3 | ...
+   * e <- (a1 | a2 | a3 | ...)
+   * : e <- (a1 | a2 | a3 |...)
+   * : e | ~(a1 | a2 | a3 |...)
+   * : 
+   * : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
+   */
+
+  vec<Lit> c;
+  c.push(~e);
+  
+  for( int index = 0; index < lits.size(); ++index){
+    Lit a = lits[index];
+    c.push(a);
+    insertClauseIntoStream( e, ~a);
+  }
+  insertClauseIntoStream(c);
+  
+  return e;
+}
+
+
+/* TODO: this only supports 2-ary <=> nodes atm.
+ * Should this be changed?
+ */
+Lit 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]);
+    
+  Lit l = aquireAndRegister(n);
+    
+  /* l <-> (a<->b)
+   * : l -> ((a-> b) & (b->a))
+   * : ~l | ((~a | b) & (~b |a))
+   * : (~a | b | ~l ) & (~b | a | ~l)
+   * 
+   * : (a<->b) -> l
+   * : ~((a & b) | (~a & ~b)) | l
+   * : (~(a & b)) & (~(~a & ~b)) | l
+   * : ((~a | ~b) & (a | b)) | l
+   * : (~a | ~b | l) & (a | b | l)
+   */
+    
+  insertClauseIntoStream( ~a, b,~l);
+  insertClauseIntoStream(  a,~b,~l);
+  insertClauseIntoStream( ~a,~b, l);
+  insertClauseIntoStream(  a, b, l);
+  
+  return l;
+}
+
+Lit TseitinCnfStream::handleAnd(const Node& n){
+  //TODO: we know the exact size of the this.
+  //Dynamically allocated array would have less overhead no?
+  vec<Lit> lits(n.getNumChildren());
+  mapRecTransformOverChildren(n, lits);
+    
+  Lit e = aquireAndRegister(n);
+
+  /* e <-> (a1 & a2 & a3 & ...)
+   * : e -> (a1 & a2 & a3 & ...)
+   * : ~e | (a1 & a2 & a3 & ...)
+   * : (~e | a1) & (~e | a2) & ...
+   * e <- (a1 & a2 & a3 & ...)
+   * : e <- (a1 & a2 & a3 & ...)
+   * : e | ~(a1 & a2 & a3 & ...)
+   * : e | (~a1 | ~a2 | ~a3 | ...)
+   * : e | ~a1 | ~a2 | ~a3 | ...
+   */
+
+  vec<Lit> c;
+  c.push(e);
+  for(int index = 0; index < lits.size(); ++index){
+    Lit a = lits[index];
+    c.push(~a);
+    insertClauseIntoStream( ~e, a );
+  }
+  insertClauseIntoStream(c);
+  
+  return e;
+}
+
+Lit TseitinCnfStream::handleImplies(const Node & n){
+  Assert(n.getKind() == IMPLIES);
+  // n: a => b;
+
+  Lit a = recTransform(n[0]);
+  Lit b = recTransform(n[1]);
+  
+  Lit l = aquireAndRegister(n);
+  
+  /* l <-> (a->b)
+   * (l -> (a->b)) & (l <- (a->b))
+   *  : l -> (a -> b)
+   *  : ~l | (~ a | b)
+   *  : (~l | ~a | b)
+   * (~l | ~a | b) & (l<- (a->b))
+   *  : (a->b) -> l
+   *  : ~(~a | b) | l
+   *  : (a & ~b) | l
+   *  : (a | l) & (~b | l)
+   * (~l | ~a | b) & (a | l) & (~b | l)
+   */
+    
+  insertClauseIntoStream(  a, l);
+  insertClauseIntoStream( ~b, l);
+  insertClauseIntoStream( ~l, ~a, b);
+  
+  return l;
+}
+
+Lit TseitinCnfStream::handleNot(const Node & n){
+  Assert(n.getKind() == NOT);
+  
+  // n : NOT m
+  Node m = n[0];
+  Lit equivM = recTransform(m);
+
+  registerMapping(n, ~equivM, false);
+
+  return equivM;
+}
+
+//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){
+  Assert(n.getKind() == ITE);
+  
+  // n : IF c THEN t ELSE f ENDIF;
+  Lit c = recTransform(n[0]);
+  Lit t = recTransform(n[1]);
+  Lit f = recTransform(n[2]);
+  
+  // d <-> IF c THEN tB ELSE fb
+  // : d -> (c & tB) | (~c & fB)
+  // : ~d | ( (c & tB) | (~c & fB) )
+  // :          x | (y & z) = (x | y) & (x | z)
+  // : ~d | ( ((c & t) | ~c ) & ((c & t) | f ) )
+  // : ~d | ( (((c | ~c) & (~c | t))) & ((c | f) & (f | t)) )
+  // : ~d | ( (~c | t) & (c | f) & (f | t) )
+  // : (~d | ~c | t) & (~d | c | f) & (~d | f | t)
+
+  // : ~d | (c & t & f)
+  // : (~d | c)  & (~d | t) & (~d | f)
+  // ( IF c THEN tB ELSE fb) -> d
+  // :~((c & tB) | (~c & fB)) | d
+  // : ((~c | ~t)& ( c |~fb)) | d
+  // : (~c | ~ t | d) & (c | ~f | d)
+
+  Lit d = aquireAndRegister(n);
+
+  insertClauseIntoStream(~d , ~c , t);
+  insertClauseIntoStream(~d ,  c , f);
+  insertClauseIntoStream(~d ,  f , t);
+  insertClauseIntoStream(~c , ~t , d);
+  insertClauseIntoStream( c , ~f , d);
+
+  return d;
+}
+
+//FIXME: This function is a major hack! Should be changed ASAP
+//TODO: Should be moved. Not sure where...
+//TODO: Should use positive defintion, i.e. what kinds are atomic.
+bool atomic(const Node & n){
+  switch(n.getKind()){
+  case NOT:
+  case XOR:
+  case ITE:
+  case IFF:
+  case OR:
+  case AND:
+    return false;
+  default:
+    return true;
+  }
+}
+
+//TODO: The following code assumes everthing is either
+// an atom or is a logical connective. This ignores quantifiers and lambdas.
+Lit TseitinCnfStream::recTransform(const Node & n){
+  if(isCached(n)){
+    return lookupInCache(n);
+  }
+  
+  if(atomic(n)){
+    return handleAtom(n);
+  }else{
+    //Assume n is a logical connective
+    switch(n.getKind()){
+    case NOT:
+      return handleNot(n);
+    case XOR:
+      return handleXor(n);
+    case ITE:
+      return handleIte(n);
+    case IFF:
+      return handleIff(n);
+    case OR:
+      return handleOr(n);
+    case AND:
+      return handleAnd(n);
+    default:
+      Unreachable();
+    }
+  }
+}
+  
+void TseitinCnfStream::convertAndAssert(const Node & n){
+  //n has already been mapped so use the previous result
+  if(isCached(n)){
+    Lit l = lookupInCache(n);
+    insertClauseIntoStream(l);
+    return;
+  }
+  
+  Lit e = recTransform(n);
+  insertClauseIntoStream( e );
+
+  //I've commented the following section out because it uses a bit too much intelligence.
+
+  /*
+  if(n.getKind() == AND){
+    // this code is required to efficiently flatten and
+    // assert each part of the node.
+    // This would be rendered unnessecary if the input was given differently
+    queue<Node> and_queue;
+    and_queue.push(n);
+
+    //This was changed to use a queue due to pressure on the C stack.
+
+    //TODO: this does no cacheing of what has been asserted.
+    //Low hanging fruit
+    while(!and_queue.empty()){
+      Node curr = and_queue.front();
+      and_queue.pop();
+      if(curr.getKind() == AND){
+	for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
+	  and_queue.push(*i);
+	}
+      }else{
+	convertAndAssert(curr);
+      }
+    }
+  }else if(n.getKind() == OR){
+    //This is special cased so minimal translation is done for things that
+    //are already in CNF so minimal work is done on clauses.
+    vec<Lit> c;
+    for(Node::iterator i = n.begin(); i != n.end(); ++i){
+      Lit cl = recTransform(*i);
+      c.push(cl);
+    }
+    insertClauseIntoStream(c);
+  }else{
+    Lit e = recTransform(n);
+    insertClauseIntoStream( e );
+  }
+  */
+}
+
+
+
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
new file mode 100644
index 000000000..c0a70730a
--- /dev/null
+++ b/src/prop/cnf_stream.h
@@ -0,0 +1,165 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_stream.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositional
+ ** equisatisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Unlike other parts of the system it is aware of the PropEngine's
+ ** internals such as the representation and translation of 
+ **/
+
+
+#ifndef __CVC4__CNF_STREAM_H
+#define __CVC4__CNF_STREAM_H
+
+//TODO: Why am i including this? Who knows...
+#include "cvc4_config.h"
+
+#include "expr/node.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+#include "prop/prop_engine.h"
+
+#include <map>
+
+namespace CVC4 {
+  class PropEngine;
+}
+
+
+namespace CVC4 {
+namespace prop {
+
+class CnfStream {
+
+private:
+  /**
+   * d_propEngine is the PropEngine that the CnfStream interacts with directly through
+   * the follwoing functions:
+   *    - insertClauseIntoStream
+   *    - acquireFreshLit
+   *    - registerMapping
+   */
+  PropEngine *d_propEngine;
+
+  /**Cache of what literal have been registered to a node.
+   *Not strictly needed for correctness.
+   *This can be flushed when memory is under pressure.
+   */
+  std::map<Node,minisat::Lit> d_translationCache;
+  
+protected:
+
+  /**
+   * Uniform interface for sending a clause back to d_propEngine.
+   * May want to have internal datastructures 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);
+  
+
+  //utilities for the translation cache;
+  bool isCached(const Node & n) const;
+  minisat::Lit lookupInCache(const Node & n) const;
+
+  /**
+   * Empties the internal translation cache.
+   */
+  void flushCache();
+
+  //negotiates the mapping of atoms to literals with PropEngine
+  void registerMapping(const Node & node, minisat::Lit lit, bool atom = false);
+  minisat::Lit acquireFreshLit(const Node & n);
+  minisat::Lit aquireAndRegister(const Node & n, bool atom = false);
+
+public:
+  /**
+   * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
+   * and sends them to pe.
+   */
+  CnfStream(CVC4::PropEngine *pe);
+
+
+  /**
+   * Converts and asserts a formula.
+   * @param n node to convert and assert
+   */
+  virtual void convertAndAssert(const Node & n) = 0;
+
+}; /* class CnfStream */
+
+
+/**
+ * TseitinCnfStream is based on the following recursive algorithm
+ * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
+ * The general gist of the algorithm is to introduce a new literal that 
+ * will be equivalent to each subexpression in the constructed equisatisfiable formula
+ * then subsistute the new literal for the formula, and to do this recursively.
+ * 
+ * This implementation does this in a single recursive pass.
+ */
+class TseitinCnfStream : public CnfStream {
+
+public:
+  void convertAndAssert(const Node & n);
+  TseitinCnfStream(CVC4::PropEngine *pe);
+
+private:
+
+  /* Each of these formulas handles takes care of a Node of each Kind.
+   *
+   * Each handleX(Node &n) is responsibile for:
+   *   - constructing a new literal, l (if nessecary)
+   *   - calling registerNode(n,l)
+   *   - adding clauses asure that l is equivalent to the Node
+   *   - calling recTransform on its children (if nessecary)
+   *   - returning l
+   *
+   * 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);
+
+  minisat::Lit handleAnd(const Node& n);
+  minisat::Lit handleOr(const Node& n);
+
+    
+  /**
+   *Maps recTransform over the children of a node.
+   *This is very useful for n-ary Kinds (OR, AND).
+   *
+   *Non n-ary kinds (IMPLIES) should avoid using this as it requires a
+   *tiny bit of extra overhead, and it leads to less readable code.
+   *
+   * precondition: target.size() == n.getNumChildren()
+   */
+  void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
+
+  //Recurisively dispatches the various Kinds to the appropriate handler.
+  minisat::Lit recTransform(const Node & n);
+
+}; /* class TseitinCnfStream */
+
+}/* prop namespace */
+}/* CVC4 namespace */
+
+
+
+#endif /* __CVC4__CNF_STREAM_H */
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 */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 6e1f8cb61..f356c9e0b 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,6 +25,13 @@
 #include "prop/minisat/core/SolverTypes.h"
 
 #include <map>
+#include "prop/cnf_stream.h"
+
+namespace CVC4 {
+  namespace prop {
+    class CnfStream;
+  }
+}
 
 namespace CVC4 {
 
@@ -35,25 +42,80 @@ 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;
 
-  void addVars(CVC4::prop::minisat::SimpSolver*, std::map<Node, CVC4::prop::minisat::Var>*, std::map<CVC4::prop::minisat::Var, Node>*, Node);
+  friend class CVC4::prop::CnfStream;
+  
+  /* Morgan: I added these back.
+   * Why did you push these into solve()?
+   * I am guessing this is for either a technical reason I'm not seeing,
+   * or that you wanted to have a clean restart everytime solve() was called
+   * and to start from scratch everytime. (Avoid push/pop problems?)
+   * Is this right?
+   */
+  CVC4::prop::minisat::SimpSolver d_sat;
+
+
+  std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
+  std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom;
 
+  /** 
+   * Adds mapping of n -> l to d_node2lit, and
+   * a mapping of l -> n to d_lit2node.
+   */
+  void registerAtom(const Node & n, CVC4::prop::minisat::Lit l);
+
+
+
+  CVC4::prop::minisat::Lit requestFreshLit();
+  bool isNodeMapped(const Node & n) const;
+  CVC4::prop::minisat::Lit lookupLit(const Node & n) 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.
+   */
+  void assertClause(CVC4::prop::minisat::vec<CVC4::prop::minisat::Lit> & c);
+
+  
+  /** The CNF converter in use */
+  //CVC4::prop::CnfConverter d_cnfConverter;
+  CVC4::prop::CnfStream *d_cnfStream;
 public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
   CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
+  CVC4_PUBLIC ~PropEngine();
+
+  /**
+   * Converts the given formula to CNF and assert the CNF to the sat solver.
+   */
+  void assertFormula(const Node& node);
 
   /**
-   * Converts to CNF if necessary.
+   * Currently this takes a well-formed* Node,
+   * converts it to a propositionally equisatisifiable formula for a sat solver,
+   * and invokes the sat solver for a satisfying assignment.
+   * TODO: what does well-formed mean here?
    */
-  void solve(Node);
+  void solve();
 
 };/* class PropEngine */
 
+
+inline bool PropEngine::isNodeMapped(const Node & n) const{
+  return d_atom2lit.find(n) != d_atom2lit.end();
+}
+
+inline CVC4::prop::minisat::Lit PropEngine::lookupLit(const Node & n) const{
+  Assert(isNodeMapped(n));
+  return d_atom2lit.find(n)->second;
+}
+
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP_ENGINE_H */