7 files changed, 472 insertions, 516 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index b4a0a297e..011d8ba5a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -27,36 +27,36 @@ using namespace std;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(PropEngine *pe) :
-  d_propEngine(pe) {
+CnfStream::CnfStream(SatSolver *satSolver) :
+  d_satSolver(satSolver) {
 }
 
-TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
-  CnfStream(pe) {
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver) :
+  CnfStream(satSolver) {
 }
 
-void CnfStream::insertClauseIntoStream(SatClause& c) {
+void CnfStream::assertClause(SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
-  d_propEngine->assertClause(c);
+  d_satSolver->addClause(c);
 }
 
-void CnfStream::insertClauseIntoStream(SatLiteral a) {
+void CnfStream::assertClause(SatLiteral a) {
   SatClause clause(1);
   clause[0] = a;
-  insertClauseIntoStream(clause);
+  assertClause(clause);
 }
-void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(SatLiteral a, SatLiteral b) {
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
-  insertClauseIntoStream(clause);
+  assertClause(clause);
 }
-void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
   SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
-  insertClauseIntoStream(clause);
+  assertClause(clause);
 }
 
 bool CnfStream::isCached(const Node& n) const {
@@ -64,328 +64,261 @@ bool CnfStream::isCached(const Node& n) const {
 }
 
 SatLiteral CnfStream::lookupInCache(const Node& n) const {
-  Assert(isCached(n),
-      "Node is not in cnf translation cache");
+  Assert(isCached(n), "Node is not in CNF translation cache");
   return d_translationCache.find(n)->second;
 }
 
-void CnfStream::flushCache() {
-  Debug("cnf") << "flushing the translation cache" << endl;
-  d_translationCache.clear();
-}
-
 void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) {
   Debug("cnf") << "caching translation " << node << " to " << lit << endl;
   d_translationCache.insert(make_pair(node, lit));
 }
 
-SatLiteral CnfStream::aquireAndRegister(const Node& node, bool atom) {
-  SatVariable var = atom ? d_propEngine->registerAtom(node)
-      : d_propEngine->requestFreshVar();
-  SatLiteral lit(var);
+SatLiteral CnfStream::newLiteral(const Node& node) {
+  SatLiteral lit = SatLiteral(d_satSolver->newVar());
   cacheTranslation(node, lit);
   return lit;
 }
 
-bool CnfStream::isAtomMapped(const Node& n) const {
-  return d_propEngine->isAtomMapped(n);
-}
-
-SatVariable CnfStream::lookupAtom(const Node& n) const {
-  return d_propEngine->lookupAtom(n);
-}
-
-/***********************************************/
-/***********************************************/
-/************ End of CnfStream *****************/
-/***********************************************/
-/***********************************************/
+SatLiteral TseitinCnfStream::handleAtom(const Node& node) {
+  Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
+  Assert(!isCached(node), "atom already mapped!");
 
-SatLiteral TseitinCnfStream::handleAtom(const Node& n) {
-  Assert(n.isAtomic(), "handleAtom(n) expects n to be an atom");
+  Debug("cnf") << "handleAtom(" << node << ")" << endl;
 
-  Debug("cnf") << "handling atom" << endl;
+  SatLiteral lit = newLiteral(node);
 
-  SatLiteral l = aquireAndRegister(n, true);
-  switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
+  switch(node.getKind()) {
   case TRUE:
-    insertClauseIntoStream(l);
+    assertClause(lit);
     break;
   case FALSE:
-    insertClauseIntoStream(~l);
+    assertClause(~lit);
     break;
-  default: //Does nothing else
+  default:
     break;
   }
-  return l;
+
+  return lit;
 }
 
-SatLiteral TseitinCnfStream::handleXor(const Node& n) {
-  // n: a XOR b
+SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) {
+  Assert(!isCached(xorNode), "Atom already mapped!");
+  Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
+  Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
-  SatLiteral a = recTransform(n[0]);
-  SatLiteral b = recTransform(n[1]);
+  SatLiteral a = toCNF(xorNode[0]);
+  SatLiteral b = toCNF(xorNode[1]);
 
-  SatLiteral l = aquireAndRegister(n);
+  SatLiteral xorLit = newLiteral(xorNode);
 
-  insertClauseIntoStream(a, b, ~l);
-  insertClauseIntoStream(a, ~b, l);
-  insertClauseIntoStream(~a, b, l);
-  insertClauseIntoStream(~a, ~b, ~l);
+  assertClause(a, b, ~xorLit);
+  assertClause(~a, ~b, ~xorLit);
+  assertClause(a, ~b, xorLit);
+  assertClause(~a, b, xorLit);
 
-  return l;
+  return xorLit;
 }
 
-/* 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,
-                                                   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()) {
-    SatLiteral equivalentLit = recTransform(*subExprIter);
-    target[i] = equivalentLit;
-    ++subExprIter;
-    ++i;
+SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
+  Assert(!isCached(orNode), "Atom already mapped!");
+  Assert(orNode.getKind() == OR, "Expecting an OR expression!");
+  Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
+
+  // Number of children
+  unsigned n_children = orNode.getNumChildren();
+
+  // Transform all the children first
+  Node::iterator node_it = orNode.begin();
+  Node::iterator node_it_end = orNode.end();
+  SatClause clause(n_children + 1);
+  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
+    clause[i] = toCNF(*node_it);
   }
-}
 
-SatLiteral TseitinCnfStream::handleOr(const Node& n) {
-  //child_literals
-  SatClause lits(n.getNumChildren());
-  mapRecTransformOverChildren(n, lits);
-
-  SatLiteral 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) & ...
-   */
-
-  SatClause c(1 + lits.size());
-
-  for(int index = 0; index < lits.size(); ++index) {
-    SatLiteral a = lits[index];
-    c[index] = a;
-    insertClauseIntoStream(e, ~a);
+  // Get the literal for this node
+  SatLiteral orLit = newLiteral(orNode);
+
+  // lit <- (a_1 | a_2 | a_3 | ... | a_n)
+  // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
+  // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
+  for(unsigned i = 0; i < n_children; ++i) {
+    assertClause(orLit, ~clause[i]);
   }
-  c[lits.size()] = ~e;
-  insertClauseIntoStream(c);
 
-  return e;
-}
+  // lit -> (a_1 | a_2 | a_3 | ... | a_n)
+  // ~lit | a_1 | a_2 | a_3 | ... | a_n
+  clause[n_children] = ~orLit;
+  // This needs to go last, as the clause might get modified by the SAT solver
+  assertClause(clause);
 
-/* TODO: this only supports 2-ary <=> nodes atm.
- * Should this be changed?
- */
-SatLiteral TseitinCnfStream::handleIff(const Node& n) {
-  Assert(n.getKind() == IFF);
-  Assert(n.getNumChildren() == 2);
-  // n: a <=> b;
-
-  SatLiteral a = recTransform(n[0]);
-  SatLiteral b = recTransform(n[1]);
-
-  SatLiteral 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;
+  // Return the literal
+  return orLit;
 }
 
-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?
-  SatClause lits(n.getNumChildren());
-  mapRecTransformOverChildren(n, lits);
-
-  SatLiteral 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 | ...
-   */
-
-  SatClause c(lits.size() + 1);
-  for(int index = 0; index < lits.size(); ++index) {
-    SatLiteral a = lits[index];
-    c[index] = (~a);
-    insertClauseIntoStream(~e, a);
+SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
+  Assert(!isCached(andNode), "Atom already mapped!");
+  Assert(andNode.getKind() == AND, "Expecting an AND expression!");
+  Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
+
+  // Number of children
+  unsigned n_children = andNode.getNumChildren();
+
+  // Transform all the children first (remembering the negation)
+  Node::iterator node_it = andNode.begin();
+  Node::iterator node_it_end = andNode.end();
+  SatClause clause(n_children + 1);
+  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
+    clause[i] = ~toCNF(*node_it);
   }
-  c[lits.size()] = e;
 
-  insertClauseIntoStream(c);
+  // Get the literal for this node
+  SatLiteral andLit = newLiteral(andNode);
+
+  // lit -> (a_1 & a_2 & a_3 & ... & a_n)
+  // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
+  // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
+  for(unsigned i = 0; i < n_children; ++i) {
+    assertClause(~andLit, ~clause[i]);
+  }
+
+  // lit <- (a_1 & a_2 & a_3 & ... a_n)
+  // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
+  // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
+  clause[n_children] = andLit;
+  // This needs to go last, as the clause might get modified by the SAT solver
+  assertClause(clause);
+  return andLit;
+}
+
+SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) {
+  Assert(!isCached(impliesNode), "Atom already mapped!");
+  Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
+  Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+
+  // Convert the children to cnf
+  SatLiteral a = toCNF(impliesNode[0]);
+  SatLiteral b = toCNF(impliesNode[1]);
+
+  SatLiteral impliesLit = newLiteral(impliesNode);
+
+  // lit -> (a->b)
+  // ~lit | ~ a | b
+  assertClause(~impliesLit, ~a, b);
+
+  // (a->b) -> lit
+  // ~(~a | b) | lit
+  // (a | l) & (~b | l)
+  assertClause(a, impliesLit);
+  assertClause(~b, impliesLit);
 
-  return e;
+  return impliesLit;
 }
 
-SatLiteral TseitinCnfStream::handleImplies(const Node& n) {
-  Assert(n.getKind() == IMPLIES);
-  Assert(n.getNumChildren() == 2);
-  // n: a => b;
-
-  SatLiteral a = recTransform(n[0]);
-  SatLiteral b = recTransform(n[1]);
-
-  SatLiteral 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;
+
+SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) {
+  Assert(!isCached(iffNode), "Atom already mapped!");
+  Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
+  Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+
+  // Convert the children to CNF
+  SatLiteral a = toCNF(iffNode[0]);
+  SatLiteral b = toCNF(iffNode[1]);
+
+  // Get the now literal
+  SatLiteral iffLit = newLiteral(iffNode);
+
+  // lit -> ((a-> b) & (b->a))
+  // ~lit | ((~a | b) & (~b | a))
+  // (~a | b | ~lit) & (~b | a | ~lit)
+  assertClause(~a, b, ~iffLit);
+  assertClause(a, ~b, ~iffLit);
+
+  // (a<->b) -> lit
+  // ~((a & b) | (~a & ~b)) | lit
+  // (~(a & b)) & (~(~a & ~b)) | lit
+  // ((~a | ~b) & (a | b)) | lit
+  // (~a | ~b | lit) & (a | b | lit)
+  assertClause(~a, ~b, iffLit);
+  assertClause(a, b, iffLit);
+
+  return iffLit;
 }
 
-SatLiteral TseitinCnfStream::handleNot(const Node& n) {
-  Assert(n.getKind() == NOT);
-  Assert(n.getNumChildren() == 1);
 
-  // n : NOT m
-  Node m = n[0];
-  SatLiteral equivM = recTransform(m);
+SatLiteral TseitinCnfStream::handleNot(const Node& notNode) {
+  Assert(!isCached(notNode), "Atom already mapped!");
+  Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
+  Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
 
-  SatLiteral equivN = ~equivM;
+  SatLiteral notLit = ~toCNF(notNode[0]);
 
-  cacheTranslation(n, equivN);
+  // Since we don't introduce new variables, we need to cache the translation
+  cacheTranslation(notNode, notLit);
 
-  return equivN;
+  return notLit;
 }
 
-SatLiteral TseitinCnfStream::handleIte(const Node& n) {
-  Assert(n.getKind() == ITE);
-  Assert(n.getNumChildren() == 3);
-
-  // n : IF c THEN t ELSE f ENDIF;
-  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)
-  // : ~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)
-
-  SatLiteral 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;
+SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) {
+  Assert(iteNode.getKind() == ITE);
+  Assert(iteNode.getNumChildren() == 3);
+
+  SatLiteral condLit = toCNF(iteNode[0]);
+  SatLiteral thenLit = toCNF(iteNode[1]);
+  SatLiteral elseLit = toCNF(iteNode[2]);
+
+  SatLiteral iteLit = newLiteral(iteNode);
+
+  // If ITE is true then one of the branches is true and the condition
+  // implies which one
+  assertClause(~iteLit, ~condLit, thenLit);
+  assertClause(~iteLit, condLit, elseLit);
+  assertClause(~iteLit, elseLit, thenLit);
+
+  // If ITE is false then one of the branches is false and the condition
+  // implies which one
+  assertClause(iteLit, ~condLit, ~thenLit);
+  assertClause(iteLit, condLit, ~elseLit);
+  assertClause(iteLit, ~thenLit, ~elseLit);
+
+  return iteLit;
 }
 
-//TODO: The following code assumes everything is either
-// an atom or is a logical connective. This ignores quantifiers and lambdas.
-SatLiteral TseitinCnfStream::recTransform(const Node& n) {
-  if(isCached(n)) {
-    return lookupInCache(n);
+SatLiteral TseitinCnfStream::toCNF(const Node& node) {
+
+  // If the node has already been translated, return the previous translation
+  if(isCached(node)) {
+    return lookupInCache(node);
+  }
+
+  // Atomic nodes are treated specially
+  if(node.isAtomic()) {
+    return handleAtom(node);
   }
 
-  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)) {
-      /* Puts the atom in the translation cache after looking it up.
-       * Avoids doing 2 map lookups for this atom in the future.
-       */
-      SatLiteral l(lookupAtom(n));
-      cacheTranslation(n, l);
-      return l;
-    }
-    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 IMPLIES:
-      return handleImplies(n);
-    case OR:
-      return handleOr(n);
-    case AND:
-      return handleAnd(n);
-    default:
-      Unreachable();
-    }
+  // Handle each Boolean operator case
+  switch(node.getKind()) {
+  case NOT:
+    return handleNot(node);
+  case XOR:
+    return handleXor(node);
+  case ITE:
+    return handleIte(node);
+  case IFF:
+    return handleIff(node);
+  case IMPLIES:
+    return handleImplies(node);
+  case OR:
+    return handleOr(node);
+  case AND:
+    return handleAnd(node);
+  default:
+    Unreachable();
   }
 }
 
-void TseitinCnfStream::convertAndAssert(const Node& n) {
-  SatLiteral e = recTransform(n);
-  insertClauseIntoStream(e);
+void TseitinCnfStream::convertAndAssert(const Node& node) {
+  Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
+  assertClause(toCNF(node));
 }
 
 }/* CVC4::prop namespace */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 0cc8cb425..9fb5858b3 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -25,7 +25,16 @@
 #include "expr/node.h"
 #include "prop/sat.h"
 
-#include <map>
+#include <ext/hash_map>
+
+namespace __gnu_cxx {
+template<>
+  struct hash<CVC4::Node> {
+    size_t operator()(const CVC4::Node& node) const {
+      return (size_t)node.hash();
+    }
+  };
+} /* __gnu_cxx namespace */
 
 namespace CVC4 {
 namespace prop {
@@ -40,69 +49,84 @@ class CnfStream {
 
 private:
 
+  /** The SAT solver we will be using */
+  SatSolver *d_satSolver;
+
+  /** Cache of what literal have been registered to a node. */
+  __gnu_cxx::hash_map<Node, SatLiteral> d_translationCache;
+
+protected:
+
   /**
-   * d_propEngine is the PropEngine that the CnfStream interacts with directly
-   * through the following functions:
-   *    - insertClauseIntoStream
-   *    - acquireFreshLit
-   *    - registerMapping
+   * Asserts the given clause to the sat solver.
+   * @param clause the clasue to assert
    */
-  PropEngine *d_propEngine;
+  void assertClause(SatClause& clause);
 
   /**
-   * Cache of what literal have been registered to a node. Not strictly needed
-   * for correctness. This can be flushed when memory is under pressure.
-   * TODO: Use attributes when they arrive
+   * Asserts the unit clause to the sat solver.
+   * @param a the unit literal of the clause
    */
-  std::map<Node, SatLiteral> d_translationCache;
-
-protected:
+  void assertClause(SatLiteral a);
 
-  bool isAtomMapped(const Node& n) const;
-
-  SatVariable lookupAtom(const Node& node) const;
+  /**
+   * Asserts the binary clause to the sat solver.
+   * @param a the first literal in the clause
+   * @param b the second literal in the clause
+   */
+  void assertClause(SatLiteral a, SatLiteral b);
 
   /**
-   * Uniform interface for sending a clause back to d_propEngine.
-   * May want to have internal data-structures later on
+   * Asserts the ternary clause to the sat solver.
+   * @param a the first literal in the clause
+   * @param b the second literal in the clause
+   * @param c the thirs literal in the clause
    */
-  void insertClauseIntoStream(SatClause& clause);
-  void insertClauseIntoStream(SatLiteral a);
-  void insertClauseIntoStream(SatLiteral a, SatLiteral b);
-  void insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c);
+  void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
 
-  //utilities for the translation cache;
+  /**
+   * Returns true if the node has been cashed in the translation cache.
+   * @param node the node
+   * @return true if the node has been cached
+   */
   bool isCached(const Node& node) const;
 
   /**
-   * Method comments...
-   * @param n
-   * @return returns ...
+   * Returns the cashed literal corresponding to the given node.
+   * @param node the node to lookup
+   * @return returns the corresponding literal
    */
   SatLiteral lookupInCache(const Node& n) const;
 
-  //negotiates the mapping of atoms to literals with PropEngine
+  /**
+   * Caches the pair of the node and the literal corresponding to the
+   * translation.
+   * @param node node
+   * @param lit
+   */
   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 propEngine
+   * Acquires a new variable from the SAT solver to represent the node and
+   * inserts the necessary data it into the mapping tables.
+   * @param node a formula
+   * @return the literal corresponding to the formula
    */
-  CnfStream(PropEngine* propEngine);
+  SatLiteral newLiteral(const Node& node);
+
+public:
 
   /**
-   * Empties the internal translation cache.
+   * Constructs a CnfStream that sends constructs an equi-satisfiable set of clauses
+   * and sends them to the given sat solver.
+   * @param satSolver the sat solver to use
    */
-  void flushCache();
+  CnfStream(SatSolver* satSolver);
 
   /**
    * Converts and asserts a formula.
    * @param node node to convert and assert
+   * @param whether the sat solver can choose to remove this clause
    */
   virtual void convertAndAssert(const Node& node) = 0;
 
@@ -122,47 +146,45 @@ class TseitinCnfStream : public CnfStream {
 
 public:
 
+  /**
+   * Convert a given formula to CNF and assert it to the SAT solver.
+   * @param node the formula to assert
+   */
   void convertAndAssert(const Node& node);
 
-  TseitinCnfStream(PropEngine* propEngine);
+  /**
+   * Constructs the stream to use the given sat solver.
+   * @param satSolver the sat solver to use
+   */
+  TseitinCnfStream(SatSolver* satSolver);
 
 private:
 
-  /* Each of these formulas handles takes care of a Node of each Kind.
-   *
-   * Each handleX(Node &n) is responsible for:
-   *   - constructing a new literal, l (if necessary)
-   *   - calling registerNode(n,l)
-   *   - adding clauses assure that l is equivalent to the Node
-   *   - calling recTransform on its children (if necessary)
-   *   - returning l
-   *
-   * handleX( n ) can assume that n is not in d_translationCache
-   */
+  // Each of these formulas handles takes care of a Node of each Kind.
+  //
+  // Each handleX(Node &n) is responsible for:
+  //   - constructing a new literal, l (if necessary)
+  //   - calling registerNode(n,l)
+  //   - adding clauses assure that l is equivalent to the Node
+  //   - calling toCNF on its children (if necessary)
+  //   - returning l
+  //
+  // handleX( n ) can assume that n is not in d_translationCache
   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);
-
   SatLiteral handleAnd(const Node& node);
   SatLiteral handleOr(const Node& node);
 
   /**
-   * 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()
-   * @param n ...
-   * @param target ...
+   * Transforms the node into CNF recursively.
+   * @param node the formula to transform
+   * @return the literal representing the root of the formula
    */
-  void mapRecTransformOverChildren(const Node& node, SatClause& target);
-
-  //Recursively dispatches the various Kinds to the appropriate handler.
-  SatLiteral recTransform(const Node& node);
+  SatLiteral toCNF(const Node& node);
 
 }; /* class TseitinCnfStream */
 
diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
new file mode 100644
index 000000000..a36116451
--- /dev/null
+++ b/src/prop/minisat/CVC4-README
@@ -0,0 +1,68 @@
+* Accessing the internals of the SAT solver
+
+The non-public parts of the SAT solver are accessed via the static methods in 
+the SatSolverProxy class. SatSolverProxy is declared as a friend of the 
+SatSolver and has all-privileges access to the internals -- use with care!!!
+
+* Clause Database and CNF
+
+The clause database consists of two parts:
+
+    vec<Clause*>        clauses;          // List of problem clauses.
+    vec<Clause*>        learnts;          // List of learnt clauses.
+
+Clauses is the original problem clauses, and learnts are the clauses learned 
+during the search. I have disabled removal of satisfied problem clauses by 
+setting the remove_satisfied flag to false.
+
+The learnt clauses get removed every once in a while by removing the half of
+clauses with the low activity (reduceDB())
+
+Since the clause database backtracks with the SMT solver, the CNF cache should
+be context dependent and everything will be in sync. 
+
+* Adding a Clause
+
+The only method in the interface that allows addition of clauses in MiniSAT is
+
+    bool Solver::addClause(vec<Lit>& ps),
+
+but it only adds the problem clauses. 
+
+In order to add the clauses to the removable database the interface is now 
+
+    bool Solver::addClause(vec<Lit>& ps, bool removable).      
+
+Clauses added with removable=true might get removed by the SAT solver when 
+compacting the database.
+
+The question is whether to add the propagation/conflict lemmas as removable or 
+not?
+
+* Making it Backtrackable
+
+First, whenever we push a context, we have to know which clauses to remove from
+the clauses vector (the problem clauses). For this we keep a CDO<int> that tells
+us how many clauses are in the database. 
+
+We do the same for the learnt (removable) clauses, but this involves a little 
+bit more work. When removing clauses, minisat will sort the learnt clauses and 
+then remove the first half on non-locked clauses. We remember a CDO<int> for 
+the current context and sort/remove from that index on in the vector. 
+
+Also, each time we push a context, we need to remember the SAT solvers decision 
+level in order to make it the "0" decision level. We also keep this in a 
+CDO<int>, but the actual level has to be kept in the SAT solver and hard-coded 
+in the routines.
+
+* Literal Activities
+
+We do not backtrack literal activities. This does not semantically change the 
+equivalence of the context, but does change solve times if the same problem is
+run several times.
+
+* Conflict Analysis
+
+TODO
+
+* Do we need to assign literals that only appear in satisfied clauses?
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 2383fd68c..5e51e5f5a 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -36,9 +36,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace CVC4 {
 namespace prop {
+
+class SatSolverProxy;
+
 namespace minisat {
 
 class Solver {
+
+  /** The only CVC4 entry point to the private solver data */
+  friend class CVC4::prop::SatSolverProxy;
+
 public:
 
     // Constructor/Destructor:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5889ba504..80a8819b9 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -31,94 +31,59 @@ namespace CVC4 {
 namespace prop {
 
 PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
-                       TheoryEngine* te) :
-  d_opts(opts),
-  d_de(de),
-  d_te(te),
-  d_restartMayBeNeeded(false) {
-  d_sat = new SatSolver();
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
+                       TheoryEngine* te)
+: d_inCheckSat(false),
+  d_options(opts),
+  d_decisionEngine(de),
+  d_theoryEngine(te) 
+{
+  Debug("prop") << "Constructing the PropEngine" << endl;
+  d_satSolver = new SatSolver();
+  SatSolverProxy::initSatSolver(d_satSolver, d_options);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
 }
 
 PropEngine::~PropEngine() {
+  Debug("prop") << "Destructing the PropEngine" << endl;
   delete d_cnfStream;
-  delete d_sat;
-}
-
-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(clause);
-}
-
-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;
-}
-
-SatVariable PropEngine::requestFreshVar() {
-  return d_sat->newVar();
+  delete d_satSolver;
 }
 
 void PropEngine::assertFormula(const Node& node) {
-
-  Debug("prop") << "Asserting ";
-  node.printAst(Debug("prop"));
-  Debug("prop") << endl;
-
+  Assert(!d_inCheckSat, "Sat solver in solve()!");
+  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  // Assert as non-removable
   d_cnfStream->convertAndAssert(node);
-  d_assertionList.push_back(node);
 }
 
-void PropEngine::restart() {
-  delete d_sat;
-  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) {
-    d_cnfStream->convertAndAssert(*iter);
-  }
+void PropEngine::assertLemma(const Node& node) {
+  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  // Assert as removable
+  d_cnfStream->convertAndAssert(node);
 }
 
-Result PropEngine::solve() {
-  if(d_restartMayBeNeeded)
-    restart();
-
-  d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
-  bool result = d_sat->solve();
-
-  if(!result) {
-    d_restartMayBeNeeded = true;
-  }
-
-  Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
-
+Result PropEngine::checkSat() {
+  Assert(!d_inCheckSat, "Sat solver in solve()!");
+  Debug("prop") << "solve()" << endl;
+  // Mark that we are in the checkSat
+  d_inCheckSat = true;
+  // Check the problem
+  bool result = d_satSolver->solve();
+  // Not in checkSat any more
+  d_inCheckSat = false;
+  Debug("prop") << "solve() => " << (result ? "true" : "false") << endl;
   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::push() {
+  Assert(!d_inCheckSat, "Sat solver in solve()!");
+  Debug("prop") << "push()" << endl;
 }
 
-void PropEngine::signalBooleanPropHasEnded() {
+void PropEngine::pop() {
+  Assert(!d_inCheckSat, "Sat solver in solve()!");
+  Debug("prop") << "pop()" << endl;
 }
-//TODO decisionEngine should be told
-//TODO theoryEngine to call lightweight theory propogation
 
 }/* prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d60771e95..9aa1ecff8 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -19,118 +19,53 @@
 
 #include "cvc4_config.h"
 #include "expr/node.h"
-#include "util/decision_engine.h"
-#include "theory/theory_engine.h"
-#include "sat.h"
 #include "util/result.h"
 #include "util/options.h"
-
-#include <map>
+#include "util/decision_engine.h"
+#include "theory/theory_engine.h"
+#include "prop/sat.h"
 
 namespace CVC4 {
 namespace prop {
 
 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.
-
+/**
+ * PropEngine is the abstraction of a Sat Solver, providing methods for
+ * solving the SAT problem and conversion to CNF (via the CnfStream).
+ */
 class PropEngine {
 
-  friend class CnfStream;
-
-  /** The global options */
-  const Options *d_opts;
-  /** The decision engine we will be using */
-  DecisionEngine *d_de;
-  /** The theory engine we will be using */
-  TheoryEngine *d_te;
-
   /**
-   * The SAT solver.
+   * Indicates that the sat solver is currently solving something and we should
+   * not mess with it's internal state.
    */
-  SatSolver* d_sat;
-
-  std::map<Node, SatVariable> d_atom2var;
-  std::map<SatVariable, Node> d_var2atom;
+  bool d_inCheckSat;
 
-  /** 
-   * 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.
-   */
-  SatVariable registerAtom(const Node& node);
-
-  /**
-   * Requests a fresh variable from d_sat.
-   */
-  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& node) const;
+  /** The global options */
+  const Options *d_options;
 
-  /**
-   * Returns the variable mapped by the atom Node.
-   * @param n the atom to do the lookup by
-   * @return the corresponding variable
-   */
-  SatVariable lookupAtom(const Node& node) const;
+  /** The decision engine we will be using */
+  DecisionEngine *d_decisionEngine;
 
-  /**
-   * Flags whether the solver may need to have its state reset before
-   * solving occurs
-   */
-  bool d_restartMayBeNeeded;
+  /** The theory engine we will be using */
+  TheoryEngine *d_theoryEngine;
 
-  /**
-   * Cleans existing state in the PropEngine and reinitializes the state.
-   */
-  void restart();
+  /** The SAT solver*/
+  SatSolver* d_satSolver;
 
-  /**
-   * Keeps track of all of the assertions that need to be made.
-   */
+  /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
-  /**
-   * 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(SatVariable var) const;
-
-  /**
-   * Returns the atom mapped by the variable v.
-   * @param var the variable to do the lookup by
-   * @return an atom
-   */
-  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 and d_lit2node.
-   * @param clause the clause to be asserted.
-   */
-  void assertClause(SatClause& clause);
-
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
-  void assertLit(SatLiteral lit);
-  void signalBooleanPropHasEnded();
-
 public:
 
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options* opts, DecisionEngine*, TheoryEngine*);
+  PropEngine(const Options*, DecisionEngine*, TheoryEngine*);
 
   /**
    * Destructor.
@@ -139,36 +74,34 @@ public:
 
   /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * The formula is asserted permanently for the current context.
+   * @param node the formula to assert
    */
   void assertFormula(const Node& node);
 
   /**
-   * 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?
+   * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * The formula can be removed by the sat solver.
+   * @param node the formula to assert
    */
-  Result solve();
+  void assertLemma(const Node& node);
 
-};/* class PropEngine */
-
-inline bool PropEngine::isAtomMapped(const Node & n) const {
-  return d_atom2var.find(n) != d_atom2var.end();
-}
+  /**
+   * Checks the current context for satisfiability.
+   */
+  Result checkSat();
 
-inline SatVariable PropEngine::lookupAtom(const Node & n) const {
-  Assert(isAtomMapped(n));
-  return d_atom2var.find(n)->second;
-}
+  /**
+   * Push the context level.
+   */
+  void push();
 
-inline bool PropEngine::isVarMapped(SatVariable v) const {
-  return d_var2atom.find(v) != d_var2atom.end();
-}
+  /**
+   * Pop the context level.
+   */
+  void pop();
 
-inline Node PropEngine::lookupVar(SatVariable v) const {
-  Assert(isVarMapped(v));
-  return d_var2atom.find(v)->second;
-}
+};/* class PropEngine */
 
 }/* prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 195323755..9375e37ec 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -20,6 +20,7 @@
 
 #ifdef __CVC4_USE_MINISAT
 
+#include "util/options.h"
 #include "prop/minisat/core/Solver.h"
 #include "prop/minisat/core/SolverTypes.h"
 
@@ -65,6 +66,33 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
   return out;
 }
 
+/**
+ * The proxy class that allows us to modify the internals of the SAT solver.
+ * It's only accessible from the PropEngine, and should be treated with major
+ * care.
+ */
+class SatSolverProxy {
+
+  /** Only the prop engine can modify the internals of the SAT solver */
+  friend class PropEngine;
+
+  private:
+
+    /**
+     * Initializes the given sat solver with the given options.
+     * @param satSolver the SAT solver
+     * @param options the options
+     */
+    inline static void initSatSolver(SatSolver* satSolver,
+                                     const Options* options) {
+      // Setup the verbosity
+      satSolver->verbosity = (options->verbosity > 0) ? 1 : -1;
+      // Do not delete the satisfied clauses, just the learnt ones
+      satSolver->remove_satisfied = false;
+    }
+};
+
+
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */