From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 9 Feb 2010 23:07:33 +0000 (+0000)
Subject: Changes to the CNF conversion and the SAT solver. All regression pass now, and we... 
X-Git-Tag: cvc5-1.0.0~9265
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=044329296028ad944b703929fad4d85aa6183472;p=cvc5.git

Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
---

diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 7f4ce3c26..794f4706a 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -237,7 +237,7 @@ impliesFormula returns [CVC4::Expr f]
 }
   : f = orFormula 
     ( IMPLIES e = impliesFormula
-        { f = mkExpr(CVC4::IFF, f, e); }
+        { f = mkExpr(CVC4::IMPLIES, f, e); }
     )?
   ;
 
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 */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d30255e4f..8bca39df4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -24,25 +24,25 @@ using namespace CVC4::prop;
 
 namespace CVC4 {
 
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
   d_assertions(),
-  d_publicEm(em),
-  d_nm(em->getNodeManager()),
-  d_opts(opts)
+  d_exprManager(em),
+  d_nodeManager(em->getNodeManager()),
+  d_options(opts)
 {
-  d_de = new DecisionEngine();
-  d_te = new TheoryEngine(this);
-  d_prop = new PropEngine(opts, d_de, d_te);
+  d_decisionEngine = new DecisionEngine();
+  d_theoryEngine = new TheoryEngine(this);
+  d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
 }
 
 SmtEngine::~SmtEngine() {
-   delete d_prop;
-   delete d_te;
-   delete d_de;
+  delete d_propEngine;
+  delete d_theoryEngine;
+  delete d_decisionEngine;
 }
 
 void SmtEngine::doCommand(Command* c) {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   c->invoke(this);
 }
 
@@ -52,16 +52,15 @@ Node SmtEngine::preprocess(const Node& e) {
 
 void SmtEngine::processAssertionList() {
   for(unsigned i = 0; i < d_assertions.size(); ++i) {
-    d_prop->assertFormula(d_assertions[i]);
+    d_propEngine->assertFormula(d_assertions[i]);
   }
   d_assertions.clear();
 }
 
-
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
   processAssertionList();
-  return d_prop->solve();
+  return d_propEngine->checkSat();
 }
 
 Result SmtEngine::quickCheck() {
@@ -77,7 +76,7 @@ void SmtEngine::addFormula(const Node& e) {
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
   Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   Result r = check().asSatisfiabilityResult();
@@ -87,8 +86,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
 Result SmtEngine::query(const BoolExpr& e) {
   Debug("smt") << "SMT query(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
-  Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
+  NodeManagerScope nms(d_nodeManager);
+  Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode()));
   addFormula(node_e);
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
@@ -97,7 +96,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   return quickCheck().asValidityResult();
@@ -110,9 +109,11 @@ Expr SmtEngine::simplify(const Expr& e) {
 }
 
 void SmtEngine::push() {
+  Debug("smt") << "SMT push()" << std::endl;
 }
 
 void SmtEngine::pop() {
+  Debug("smt") << "SMT pop()" << std::endl;
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb9384ca5..d796959a9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -117,23 +117,22 @@ private:
   std::vector<Node> d_assertions;
 
   /** Our expression manager */
-  ExprManager* d_publicEm;
+  ExprManager* d_exprManager;
 
   /** Out internal expression/node manager */
-  NodeManager* d_nm;
+  NodeManager* d_nodeManager;
 
   /** User-level options */
-  const Options* d_opts;
+  const Options* d_options;
 
   /** The decision engine */
-  DecisionEngine* d_de;
+  DecisionEngine* d_decisionEngine;
 
   /** The decision engine */
-  TheoryEngine* d_te;
+  TheoryEngine* d_theoryEngine;
 
   /** The propositional engine */
-  prop::PropEngine* d_prop;
-
+  prop::PropEngine* d_propEngine;
 
   /**
    * Pre-process an Node.  This is expected to be highly-variable,
@@ -141,12 +140,12 @@ private:
    * passes over the Node.  TODO: may need to specify a LEVEL of
    * preprocessing (certain contexts need more/less ?).
    */
-  Node preprocess(const Node& e);
+  Node preprocess(const Node& node);
 
   /**
    * Adds a formula to the current context.
    */
-  void addFormula(const Node& e);
+  void addFormula(const Node& node);
 
   /**
    * Full check of consistency in current context.  Returns true iff
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index df0268f80..09be302af 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,19 +1,38 @@
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =	boolean.cvc \
-	bug1.cvc \
-	hole6.cvc \
-	logops.cvc \
-	queries0.cvc \
+TESTS =	hole6.cvc \
+	logops.01.cvc \
+	logops.02.cvc \
+	logops.03.cvc \
+	logops.04.cvc \
+	logops.05.cvc \
 	simple2.smt \
 	simple.cvc \
 	simple.smt \
-	simple-uf.smt \
 	smallcnf.cvc \
 	test11.cvc \
-	test12.cvc \
 	test9.cvc \
 	uf20-03.cvc \
-	wiki.cvc
+	wiki.01.cvc \
+	wiki.02.cvc \
+	wiki.03.cvc \
+	wiki.04.cvc \
+	wiki.05.cvc \
+	wiki.06.cvc \
+	wiki.07.cvc \
+	wiki.08.cvc \
+	wiki.09.cvc \
+	wiki.10.cvc \
+	wiki.11.cvc \
+	wiki.12.cvc \
+	wiki.13.cvc \
+	wiki.14.cvc \
+	wiki.15.cvc \
+	wiki.16.cvc \
+	wiki.17.cvc \
+	wiki.18.cvc \
+	wiki.19.cvc \
+	wiki.20.cvc \
+	wiki.21.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc
new file mode 100644
index 000000000..d947d1a27
--- /dev/null
+++ b/test/regress/regress0/logops.01.cvc
@@ -0,0 +1,3 @@
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc
new file mode 100644
index 000000000..ba2d55b4f
--- /dev/null
+++ b/test/regress/regress0/logops.02.cvc
@@ -0,0 +1,3 @@
+a, b, c: BOOLEAN;
+% EXPECT: INVALID
+QUERY NOT c AND b;
diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc
new file mode 100644
index 000000000..85b23d2b0
--- /dev/null
+++ b/test/regress/regress0/logops.03.cvc
@@ -0,0 +1,3 @@
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc
new file mode 100644
index 000000000..a71096542
--- /dev/null
+++ b/test/regress/regress0/logops.04.cvc
@@ -0,0 +1,3 @@
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY (a => b) <=> (NOT a OR b);
diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc
new file mode 100644
index 000000000..19bbae5b4
--- /dev/null
+++ b/test/regress/regress0/logops.05.cvc
@@ -0,0 +1,4 @@
+a, b, c: BOOLEAN;
+% EXPECT: VALID
+QUERY TRUE XOR FALSE;
+ 
diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc
deleted file mode 100644
index 7bd2a356d..000000000
--- a/test/regress/regress0/logops.cvc
+++ /dev/null
@@ -1,17 +0,0 @@
-a, b, c: BOOLEAN;
-
-% EXPECT: VALID
-QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
-
-% EXPECT: INVALID
-QUERY NOT c AND b;
-
-% EXPECT: VALID
-QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
-
-% EXPECT: VALID
-QUERY (a => b) <=> (NOT a OR b);
-
-% EXPECT: VALID
-QUERY TRUE XOR FALSE;
- 
diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc
new file mode 100644
index 000000000..57660b5a1
--- /dev/null
+++ b/test/regress/regress0/wiki.01.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (b OR c) <=> (a OR b) OR c;
diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc
new file mode 100644
index 000000000..baba45927
--- /dev/null
+++ b/test/regress/regress0/wiki.02.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (b AND c) <=> (a AND b) AND c;
diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc
new file mode 100644
index 000000000..791cc45c8
--- /dev/null
+++ b/test/regress/regress0/wiki.03.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR b <=> b OR a;
diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc
new file mode 100644
index 000000000..f0f73ce1f
--- /dev/null
+++ b/test/regress/regress0/wiki.04.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND b <=> b AND a;
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
new file mode 100644
index 000000000..afb094dae
--- /dev/null
+++ b/test/regress/regress0/wiki.05.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (a AND b) <=> a;
diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc
new file mode 100644
index 000000000..421bfbdfd
--- /dev/null
+++ b/test/regress/regress0/wiki.06.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (a OR b) <=> a;
diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc
new file mode 100644
index 000000000..a28cbf553
--- /dev/null
+++ b/test/regress/regress0/wiki.07.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc
new file mode 100644
index 000000000..70fc5f430
--- /dev/null
+++ b/test/regress/regress0/wiki.08.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc
new file mode 100644
index 000000000..d3118536d
--- /dev/null
+++ b/test/regress/regress0/wiki.09.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR NOT a;
diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc
new file mode 100644
index 000000000..41a9bcd3f
--- /dev/null
+++ b/test/regress/regress0/wiki.10.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND NOT a <=> FALSE;
diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc
new file mode 100644
index 000000000..e9c0b9cce
--- /dev/null
+++ b/test/regress/regress0/wiki.11.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR a <=> a;
diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc
new file mode 100644
index 000000000..d5e7bd776
--- /dev/null
+++ b/test/regress/regress0/wiki.12.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND a <=> a;
diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc
new file mode 100644
index 000000000..2674ba47b
--- /dev/null
+++ b/test/regress/regress0/wiki.13.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR FALSE <=> a;
diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc
new file mode 100644
index 000000000..378b84dcd
--- /dev/null
+++ b/test/regress/regress0/wiki.14.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND TRUE <=> a;
diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc
new file mode 100644
index 000000000..ca51c4632
--- /dev/null
+++ b/test/regress/regress0/wiki.15.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a OR TRUE <=> TRUE;
diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc
new file mode 100644
index 000000000..af47433f8
--- /dev/null
+++ b/test/regress/regress0/wiki.16.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY a AND FALSE <=> FALSE;
diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc
new file mode 100644
index 000000000..dc7e7a1c3
--- /dev/null
+++ b/test/regress/regress0/wiki.17.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT FALSE <=> TRUE;
diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc
new file mode 100644
index 000000000..21a87f4b5
--- /dev/null
+++ b/test/regress/regress0/wiki.18.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT TRUE <=> FALSE;
diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc
new file mode 100644
index 000000000..c6081c200
--- /dev/null
+++ b/test/regress/regress0/wiki.19.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT (a OR b) <=> NOT a AND NOT b;
diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc
new file mode 100644
index 000000000..3bec9348b
--- /dev/null
+++ b/test/regress/regress0/wiki.20.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT (a AND b) <=> NOT a OR NOT b;
diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc
new file mode 100644
index 000000000..e99ba2d68
--- /dev/null
+++ b/test/regress/regress0/wiki.21.cvc
@@ -0,0 +1,4 @@
+a, b, c : BOOLEAN;
+
+% EXPECT: VALID
+QUERY NOT NOT a <=> a;
diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc
deleted file mode 100644
index b5894dbad..000000000
--- a/test/regress/regress0/wiki.cvc
+++ /dev/null
@@ -1,58 +0,0 @@
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-% EXPECT: VALID
-
-a, b, c : BOOLEAN;
-
-QUERY a OR (b OR c) <=> (a OR b) OR c;
-QUERY a AND (b AND c) <=> (a AND b) AND c;
-
-QUERY a OR b <=> b OR a;
-QUERY a AND b <=> b AND a;
-
-QUERY a OR (a AND b) <=> a;
-QUERY a AND (a OR b) <=> a;
-
-QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
-QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
-
-QUERY a OR NOT a;
-QUERY a AND NOT a <=> FALSE;
-
-QUERY a OR a <=> a;
-QUERY a AND a <=> a;
-
-
-QUERY a OR FALSE <=> a;
-QUERY a AND TRUE <=> a;
-
-QUERY a OR TRUE <=> TRUE;
-QUERY a AND FALSE <=> FALSE;
-
-QUERY NOT FALSE <=> TRUE;
-QUERY NOT TRUE <=> FALSE;
-
-QUERY NOT (a OR b) <=> NOT a AND NOT b;
-QUERY NOT (a AND b) <=> NOT a OR NOT b;
-
-QUERY NOT NOT a <=> a;
-
-
diff --git a/test/regress/run_regression b/test/regress/run_regression
index c141cf43a..2be776b3f 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -56,8 +56,8 @@ expfile=`mktemp -t cvc4_expected.XXXXXXXXXX`
 outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
 echo "$expected_output" >"$expfile"
 
-echo "$cvc4" --segv-nospin "$benchmark"
-"$cvc4" --segv-nospin "$benchmark" | tee "$outfile"
+# echo "$cvc4" --segv-nospin "$benchmark"
+"$cvc4" --segv-nospin "$benchmark" > "$outfile"
 
 diffs=`diff -u "$expfile" "$outfile"`
 diffexit=$?