From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 4 Feb 2010 23:50:23 +0000 (+0000)
Subject: beautification of the prop engine
X-Git-Tag: cvc5-1.0.0~9282
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc4b8296ded0a2288fbfeb71b9ded9217bad6b86;p=cvc5.git

beautification of the prop engine
---

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 72ad61e95..6f1c525ca 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -37,6 +37,23 @@ bool Node::isNull() const {
   return d_ev == &NodeValue::s_null;
 }
 
+////FIXME: This function is a major hack! Should be changed ASAP
+////TODO: Should use positive definition, i.e. what kinds are atomic.
+bool Node::isAtomic() const {
+  switch(getKind()) {
+  case NOT:
+  case XOR:
+  case ITE:
+  case IFF:
+  case IMPLIES:
+  case OR:
+  case AND:
+    return false;
+  default:
+    return true;
+  }
+}
+
 Node::Node() :
   d_ev(&NodeValue::s_null) {
   // No refcount needed
diff --git a/src/expr/node.h b/src/expr/node.h
index 63bacaa52..3b0cb8abb 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -153,6 +153,7 @@ public:
   inline void toStream(std::ostream&) const;
 
   bool isNull() const;
+  bool isAtomic() const;
 
    /**
    * Very basic pretty printer for Node.
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e333543b4..b4a0a297e 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -22,36 +22,11 @@
 
 #include <queue>
 
-using namespace CVC4::prop::minisat;
 using namespace std;
 
 namespace CVC4 {
 namespace prop {
 
-bool atomic(const Node & n);
-
-
-static void printVar(ostream & out, Var v){
-  out << v;
-}
-
-static void printLit(ostream & out, Lit l) {
-  const char * s = (sign(l))?"~":" ";
-  out << s << var(l);
-}
-
-
-static void printClause(ostream & out, vec<Lit> & c) {
-  out << "clause:";  
-  for(int i=0;i<c.size();i++){
-    out << " ";
-    printLit(out, c[i]) ;
-  }
-  out << ";" << endl;
-}
-
-
-
 CnfStream::CnfStream(PropEngine *pe) :
   d_propEngine(pe) {
 }
@@ -60,42 +35,37 @@ TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
   CnfStream(pe) {
 }
 
-
-
-void CnfStream::insertClauseIntoStream(vec<Lit> & c) {
-  Debug("cnf") << "Inserting into stream ";
-  printClause(Debug("cnf"),c);
-
+void CnfStream::insertClauseIntoStream(SatClause& c) {
+  Debug("cnf") << "Inserting into stream " << c << endl;
   d_propEngine->assertClause(c);
 }
 
-void CnfStream::insertClauseIntoStream(minisat::Lit a) {
-  vec<Lit> clause(1);
+void CnfStream::insertClauseIntoStream(SatLiteral a) {
+  SatClause clause(1);
   clause[0] = a;
   insertClauseIntoStream(clause);
 }
-void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b) {
-  vec<Lit> clause(2);
+void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b) {
+  SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
   insertClauseIntoStream(clause);
 }
-void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b,
-                                       minisat::Lit c) {
-  vec<Lit> clause(3);
+void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c) {
+  SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
   insertClauseIntoStream(clause);
 }
 
-bool CnfStream::isCached(const Node & n) const {
+bool CnfStream::isCached(const Node& n) const {
   return d_translationCache.find(n) != d_translationCache.end();
 }
 
-Lit CnfStream::lookupInCache(const Node & n) const {
+SatLiteral CnfStream::lookupInCache(const Node& n) const {
   Assert(isCached(n),
-	 "Node is not in cnf translation cache");
+      "Node is not in cnf translation cache");
   return d_translationCache.find(n)->second;
 }
 
@@ -104,28 +74,24 @@ void CnfStream::flushCache() {
   d_translationCache.clear();
 }
 
-void CnfStream::cacheTranslation(const Node & node, Lit lit) {
-  Debug("cnf") << "cacheing translation "<< node << " to ";
-  printLit(Debug("cnf"),lit);
-  Debug("cnf") << endl;
-  
+void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) {
+  Debug("cnf") << "caching translation " << node << " to " << lit << endl;
   d_translationCache.insert(make_pair(node, lit));
 }
 
-Lit CnfStream::aquireAndRegister(const Node & node, bool atom) {
-  Var v = atom ?
-      d_propEngine->registerAtom(node)
-    : d_propEngine->requestFreshVar();
-  Lit l(v);
-  cacheTranslation(node, l);
-  return l;
+SatLiteral CnfStream::aquireAndRegister(const Node& node, bool atom) {
+  SatVariable var = atom ? d_propEngine->registerAtom(node)
+      : d_propEngine->requestFreshVar();
+  SatLiteral lit(var);
+  cacheTranslation(node, lit);
+  return lit;
 }
 
-bool CnfStream::isAtomMapped(const Node & n) const{
+bool CnfStream::isAtomMapped(const Node& n) const {
   return d_propEngine->isAtomMapped(n);
 }
-  
-Var CnfStream::lookupAtom(const Node & n) const{
+
+SatVariable CnfStream::lookupAtom(const Node& n) const {
   return d_propEngine->lookupAtom(n);
 }
 
@@ -135,12 +101,12 @@ Var CnfStream::lookupAtom(const Node & n) const{
 /***********************************************/
 /***********************************************/
 
-Lit TseitinCnfStream::handleAtom(const Node & n) {
-  Assert(atomic(n), "handleAtom(n) expects n to be an atom");
+SatLiteral TseitinCnfStream::handleAtom(const Node& n) {
+  Assert(n.isAtomic(), "handleAtom(n) expects n to be an atom");
 
   Debug("cnf") << "handling atom" << endl;
 
-  Lit l = aquireAndRegister(n, true);
+  SatLiteral l = aquireAndRegister(n, true);
   switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
   case TRUE:
     insertClauseIntoStream(l);
@@ -154,13 +120,13 @@ Lit TseitinCnfStream::handleAtom(const Node & n) {
   return l;
 }
 
-Lit TseitinCnfStream::handleXor(const Node & n) {
+SatLiteral TseitinCnfStream::handleXor(const Node& n) {
   // n: a XOR b
 
-  Lit a = recTransform(n[0]);
-  Lit b = recTransform(n[1]);
+  SatLiteral a = recTransform(n[0]);
+  SatLiteral b = recTransform(n[1]);
 
-  Lit l = aquireAndRegister(n);
+  SatLiteral l = aquireAndRegister(n);
 
   insertClauseIntoStream(a, b, ~l);
   insertClauseIntoStream(a, ~b, l);
@@ -174,27 +140,27 @@ Lit TseitinCnfStream::handleXor(const Node & n) {
  size of the number of children of n.
  */
 void TseitinCnfStream::mapRecTransformOverChildren(const Node& n,
-                                                   vec<Lit> & target) {
-  Assert(target.size() == n.getNumChildren(),
-	 "Size of the children must be the same the constructed clause");
+                                                   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()) {
-    Lit equivalentLit = recTransform(*subExprIter);
+    SatLiteral equivalentLit = recTransform(*subExprIter);
     target[i] = equivalentLit;
     ++subExprIter;
     ++i;
   }
 }
 
-Lit TseitinCnfStream::handleOr(const Node& n) {
+SatLiteral TseitinCnfStream::handleOr(const Node& n) {
   //child_literals
-  vec<Lit> lits(n.getNumChildren());
+  SatClause lits(n.getNumChildren());
   mapRecTransformOverChildren(n, lits);
 
-  Lit e = aquireAndRegister(n);
+  SatLiteral e = aquireAndRegister(n);
 
   /* e <-> (a1 | a2 | a3 | ...)
    *: e -> (a1 | a2 | a3 | ...)
@@ -207,11 +173,10 @@ Lit TseitinCnfStream::handleOr(const Node& n) {
    * : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
    */
 
-  vec<Lit> c(1 + lits.size());
-
+  SatClause c(1 + lits.size());
 
   for(int index = 0; index < lits.size(); ++index) {
-    Lit a = lits[index];
+    SatLiteral a = lits[index];
     c[index] = a;
     insertClauseIntoStream(e, ~a);
   }
@@ -224,15 +189,15 @@ Lit TseitinCnfStream::handleOr(const Node& n) {
 /* TODO: this only supports 2-ary <=> nodes atm.
  * Should this be changed?
  */
-Lit TseitinCnfStream::handleIff(const Node& n) {
-  Assert(n.getKind() == IFF); 
+SatLiteral TseitinCnfStream::handleIff(const Node& n) {
+  Assert(n.getKind() == IFF);
   Assert(n.getNumChildren() == 2);
   // n: a <=> b;
 
-  Lit a = recTransform(n[0]);
-  Lit b = recTransform(n[1]);
+  SatLiteral a = recTransform(n[0]);
+  SatLiteral b = recTransform(n[1]);
 
-  Lit l = aquireAndRegister(n);
+  SatLiteral l = aquireAndRegister(n);
 
   /* l <-> (a<->b)
    * : l -> ((a-> b) & (b->a))
@@ -254,16 +219,16 @@ Lit TseitinCnfStream::handleIff(const Node& n) {
   return l;
 }
 
-Lit TseitinCnfStream::handleAnd(const Node& n) {  
-  Assert(n.getKind() == AND); 
+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?
-  vec<Lit> lits(n.getNumChildren());
+  SatClause lits(n.getNumChildren());
   mapRecTransformOverChildren(n, lits);
 
-  Lit e = aquireAndRegister(n);
+  SatLiteral e = aquireAndRegister(n);
 
   /* e <-> (a1 & a2 & a3 & ...)
    * : e -> (a1 & a2 & a3 & ...)
@@ -276,9 +241,9 @@ Lit TseitinCnfStream::handleAnd(const Node& n) {
    * : e | ~a1 | ~a2 | ~a3 | ...
    */
 
-  vec<Lit> c(lits.size()+1);
+  SatClause c(lits.size() + 1);
   for(int index = 0; index < lits.size(); ++index) {
-    Lit a = lits[index];
+    SatLiteral a = lits[index];
     c[index] = (~a);
     insertClauseIntoStream(~e, a);
   }
@@ -289,15 +254,15 @@ Lit TseitinCnfStream::handleAnd(const Node& n) {
   return e;
 }
 
-Lit TseitinCnfStream::handleImplies(const Node & n) {
+SatLiteral TseitinCnfStream::handleImplies(const Node& n) {
   Assert(n.getKind() == IMPLIES);
   Assert(n.getNumChildren() == 2);
   // n: a => b;
 
-  Lit a = recTransform(n[0]);
-  Lit b = recTransform(n[1]);
+  SatLiteral a = recTransform(n[0]);
+  SatLiteral b = recTransform(n[1]);
 
-  Lit l = aquireAndRegister(n);
+  SatLiteral l = aquireAndRegister(n);
 
   /* l <-> (a->b)
    * (l -> (a->b)) & (l <- (a->b))
@@ -319,31 +284,29 @@ Lit TseitinCnfStream::handleImplies(const Node & n) {
   return l;
 }
 
-Lit TseitinCnfStream::handleNot(const Node & n) {
+SatLiteral TseitinCnfStream::handleNot(const Node& n) {
   Assert(n.getKind() == NOT);
   Assert(n.getNumChildren() == 1);
 
   // n : NOT m
   Node m = n[0];
-  Lit equivM = recTransform(m);
+  SatLiteral equivM = recTransform(m);
 
-  Lit equivN = ~equivM;
+  SatLiteral equivN = ~equivM;
 
   cacheTranslation(n, equivN);
 
   return equivN;
 }
 
-//FIXME: This function is a major hack! Should be changed ASAP
-//Assumes binary no else if branchs, and that ITEs 
-Lit TseitinCnfStream::handleIte(const Node & n) {
+SatLiteral TseitinCnfStream::handleIte(const Node& n) {
   Assert(n.getKind() == ITE);
   Assert(n.getNumChildren() == 3);
 
   // n : IF c THEN t ELSE f ENDIF;
-  Lit c = recTransform(n[0]);
-  Lit t = recTransform(n[1]);
-  Lit f = recTransform(n[2]);
+  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)
@@ -361,7 +324,7 @@ Lit TseitinCnfStream::handleIte(const Node & n) {
   // : ((~c | ~t)& ( c |~fb)) | d
   // : (~c | ~ t | d) & (c | ~f | d)
 
-  Lit d = aquireAndRegister(n);
+  SatLiteral d = aquireAndRegister(n);
 
   insertClauseIntoStream(~d, ~c, t);
   insertClauseIntoStream(~d, c, f);
@@ -372,45 +335,27 @@ Lit TseitinCnfStream::handleIte(const Node & n) {
   return d;
 }
 
-//FIXME: This function is a major hack! Should be changed ASAP
-//TODO: Should be moved. Not sure where...
-//TODO: Should use positive definition, i.e. what kinds are atomic.
-bool atomic(const Node & n) {
-  switch(n.getKind()) {
-  case NOT:
-  case XOR:
-  case ITE:
-  case IFF:
-  case IMPLIES:
-  case OR:
-  case AND:
-    return false;
-  default:
-    return true;
-  }
-}
-
-//TODO: The following code assumes everthing is either
+//TODO: The following code assumes everything is either
 // an atom or is a logical connective. This ignores quantifiers and lambdas.
-Lit TseitinCnfStream::recTransform(const Node & n) {
+SatLiteral TseitinCnfStream::recTransform(const Node& n) {
   if(isCached(n)) {
     return lookupInCache(n);
   }
 
-  if(atomic(n)) {
-    
-    /* Unforunately we need to potentially allow
+  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)){
+    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.
        */
-      Lit l(lookupAtom(n));
+      SatLiteral l(lookupAtom(n));
       cacheTranslation(n, l);
       return l;
     }
@@ -438,8 +383,8 @@ Lit TseitinCnfStream::recTransform(const Node & n) {
   }
 }
 
-void TseitinCnfStream::convertAndAssert(const Node & n) {
-  Lit e = recTransform(n);
+void TseitinCnfStream::convertAndAssert(const Node& n) {
+  SatLiteral e = recTransform(n);
   insertClauseIntoStream(e);
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 97f1ee801..0cc8cb425 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -23,19 +23,15 @@
 #define __CVC4__CNF_STREAM_H
 
 #include "expr/node.h"
-#include "prop/minisat/simp/SimpSolver.h"
-#include "prop/minisat/core/SolverTypes.h"
-#include "prop/prop_engine.h"
+#include "prop/sat.h"
 
 #include <map>
 
-namespace CVC4 {
-class PropEngine;
-}
-
 namespace CVC4 {
 namespace prop {
 
+class PropEngine;
+
 /**
  * Comments for the behavior of the whole class...
  * @author Tim King <taking@cs.nyu.edu>
@@ -58,44 +54,46 @@ private:
    * for correctness. This can be flushed when memory is under pressure.
    * TODO: Use attributes when they arrive
    */
-  std::map<Node, minisat::Lit> d_translationCache;
+  std::map<Node, SatLiteral> d_translationCache;
 
 protected:
-  bool isAtomMapped(const Node & n) const;
-  minisat::Var lookupAtom(const Node & n) const;
+
+  bool isAtomMapped(const Node& n) const;
+
+  SatVariable lookupAtom(const Node& node) const;
 
   /**
    * Uniform interface for sending a clause back to d_propEngine.
    * May want to have internal data-structures later on
    */
-  void insertClauseIntoStream(minisat::vec<minisat::Lit> & c);
-  void insertClauseIntoStream(minisat::Lit a);
-  void insertClauseIntoStream(minisat::Lit a, minisat::Lit b);
-  void insertClauseIntoStream(minisat::Lit a, minisat::Lit b, minisat::Lit c);
+  void insertClauseIntoStream(SatClause& clause);
+  void insertClauseIntoStream(SatLiteral a);
+  void insertClauseIntoStream(SatLiteral a, SatLiteral b);
+  void insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c);
 
   //utilities for the translation cache;
-  bool isCached(const Node & n) const;
+  bool isCached(const Node& node) const;
 
   /**
    * Method comments...
    * @param n
    * @return returns ...
    */
-  minisat::Lit lookupInCache(const Node & n) const;
-
+  SatLiteral lookupInCache(const Node& n) const;
 
   //negotiates the mapping of atoms to literals with PropEngine
-  void cacheTranslation(const Node & node, minisat::Lit lit);
-  minisat::Lit aquireAndRegister(const Node & n, bool atom = false);
+  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 pe
+   * @param propEngine
    */
-  CnfStream(CVC4::PropEngine *pe);
-
+  CnfStream(PropEngine* propEngine);
 
   /**
    * Empties the internal translation cache.
@@ -104,9 +102,9 @@ public:
 
   /**
    * Converts and asserts a formula.
-   * @param n node to convert and assert
+   * @param node node to convert and assert
    */
-  virtual void convertAndAssert(const Node & n) = 0;
+  virtual void convertAndAssert(const Node& node) = 0;
 
 }; /* class CnfStream */
 
@@ -123,8 +121,10 @@ public:
 class TseitinCnfStream : public CnfStream {
 
 public:
-  void convertAndAssert(const Node & n);
-  TseitinCnfStream(CVC4::PropEngine *pe);
+
+  void convertAndAssert(const Node& node);
+
+  TseitinCnfStream(PropEngine* propEngine);
 
 private:
 
@@ -139,15 +139,15 @@ private:
    *
    * handleX( n ) can assume that n is not in d_translationCache
    */
-  minisat::Lit handleAtom(const Node & n);
-  minisat::Lit handleNot(const Node & n);
-  minisat::Lit handleXor(const Node & n);
-  minisat::Lit handleImplies(const Node & n);
-  minisat::Lit handleIff(const Node & n);
-  minisat::Lit handleIte(const Node & n);
+  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);
 
-  minisat::Lit handleAnd(const Node& n);
-  minisat::Lit handleOr(const Node& n);
+  SatLiteral handleAnd(const Node& node);
+  SatLiteral handleOr(const Node& node);
 
   /**
    * Maps recTransform over the children of a node. This is very useful for
@@ -159,11 +159,10 @@ private:
    * @param n ...
    * @param target ...
    */
-  void mapRecTransformOverChildren(const Node& n,
-                                   minisat::vec<minisat::Lit> & target);
+  void mapRecTransformOverChildren(const Node& node, SatClause& target);
 
   //Recursively dispatches the various Kinds to the appropriate handler.
-  minisat::Lit recTransform(const Node & n);
+  SatLiteral recTransform(const Node& node);
 
 }; /* class TseitinCnfStream */
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ad38c2a1f..5889ba504 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -17,9 +17,6 @@
 
 #include "theory/theory_engine.h"
 #include "util/decision_engine.h"
-#include "prop/minisat/mtl/Vec.h"
-#include "prop/minisat/simp/SimpSolver.h"
-#include "prop/minisat/core/SolverTypes.h"
 #include "util/Assert.h"
 #include "util/output.h"
 #include "util/options.h"
@@ -28,44 +25,42 @@
 #include <utility>
 #include <map>
 
-using namespace CVC4::prop::minisat;
 using namespace std;
 
 namespace CVC4 {
+namespace prop {
 
-PropEngine::PropEngine(const Options* opts,
-                       DecisionEngine& de,
-                       TheoryEngine& te) :
+PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
+                       TheoryEngine* te) :
   d_opts(opts),
-  d_de(de), 
-  d_te(te), 
-  d_restartMayBeNeeded(false){
-  d_sat = new Solver();
+  d_de(de),
+  d_te(te),
+  d_restartMayBeNeeded(false) {
+  d_sat = new SatSolver();
   d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
 }
 
-PropEngine::~PropEngine(){
+PropEngine::~PropEngine() {
   delete d_cnfStream;
   delete d_sat;
 }
 
-
-void PropEngine::assertClause(vec<Lit> & c){
+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(c);
+  d_sat->addClause(clause);
 }
 
-Var PropEngine::registerAtom(const Node & n){
-  Var v = requestFreshVar();
-  d_atom2var.insert(make_pair(n,v));
-  d_var2atom.insert(make_pair(v,n));
+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;
 }
 
-Var PropEngine::requestFreshVar(){
+SatVariable PropEngine::requestFreshVar() {
   return d_sat->newVar();
 }
 
@@ -79,20 +74,19 @@ void PropEngine::assertFormula(const Node& node) {
   d_assertionList.push_back(node);
 }
 
-void PropEngine::restart(){
+void PropEngine::restart() {
   delete d_sat;
-  d_sat = new Solver();
+  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){
+  for(vector<Node>::iterator iter = d_assertionList.begin(); iter
+      != d_assertionList.end(); ++iter) {
     d_cnfStream->convertAndAssert(*iter);
   }
 }
 
-
 Result PropEngine::solve() {
   if(d_restartMayBeNeeded)
     restart();
@@ -100,7 +94,7 @@ Result PropEngine::solve() {
   d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
   bool result = d_sat->solve();
 
-  if(!result){
+  if(!result) {
     d_restartMayBeNeeded = true;
   }
 
@@ -109,22 +103,22 @@ Result PropEngine::solve() {
   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::assertLit(Lit l){
-    Var v = var(l);
-    if(isVarMapped(v)){
-      Node atom = lookupVar(v);
-      //Theory* t = ...;
-      //t must be the corresponding theory for the atom
-      
-      //Literal l(atom, sign(l));
-      //t->assertLiteral(l );
-    }
-  } 
-  
-  void PropEngine::signalBooleanPropHasEnded(){}
-  //TODO decisionEngine should be told
-  //TODO theoryEngine to call lightweight theory propogation
-  
+void PropEngine::signalBooleanPropHasEnded() {
+}
+//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 afeee3a41..d60771e95 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -21,76 +21,72 @@
 #include "expr/node.h"
 #include "util/decision_engine.h"
 #include "theory/theory_engine.h"
-#include "prop/minisat/simp/SimpSolver.h"
-#include "prop/minisat/core/SolverTypes.h"
+#include "sat.h"
 #include "util/result.h"
+#include "util/options.h"
 
 #include <map>
-#include "prop/cnf_stream.h"
 
 namespace CVC4 {
-  namespace prop {
-    class CnfStream;
-  }
+namespace prop {
 
-  class Options;
-}
-
-namespace CVC4 {
+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.
 
 class PropEngine {
+
+  friend class CnfStream;
+
+  /** The global options */
   const Options *d_opts;
-  DecisionEngine &d_de;
-  TheoryEngine &d_te;
+  /** The decision engine we will be using */
+  DecisionEngine *d_de;
+  /** The theory engine we will be using */
+  TheoryEngine *d_te;
 
-  friend class CVC4::prop::CnfStream;
-  
   /**
    * The SAT solver.
    */
-  CVC4::prop::minisat::Solver* d_sat;
-
-  std::map<Node, CVC4::prop::minisat::Var> d_atom2var;
-  std::map<CVC4::prop::minisat::Var, Node> d_var2atom;
+  SatSolver* d_sat;
 
+  std::map<Node, SatVariable> d_atom2var;
+  std::map<SatVariable, Node> d_var2atom;
 
   /** 
    * 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.
    */
-  CVC4::prop::minisat::Var registerAtom(const Node & n);
+  SatVariable registerAtom(const Node& node);
 
   /**
    * Requests a fresh variable from d_sat.
    */
-  CVC4::prop::minisat::Var requestFreshVar();
-
+  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 & n) const;
+  bool isAtomMapped(const Node& node) const;
 
   /**
    * Returns the variable mapped by the atom Node.
    * @param n the atom to do the lookup by
    * @return the corresponding variable
    */
-  CVC4::prop::minisat::Var lookupAtom(const Node & n) const;
+  SatVariable lookupAtom(const Node& node) const;
 
   /**
    * Flags whether the solver may need to have its state reset before
    * solving occurs
    */
   bool d_restartMayBeNeeded;
-  
+
   /**
    * Cleans existing state in the PropEngine and reinitializes the state.
    */
@@ -101,47 +97,44 @@ class PropEngine {
    */
   std::vector<Node> d_assertionList;
 
-  
   /**
-   * Returns true iff the minisat var has been mapped to an atom.
-   * @param v variable to check if it is mapped
+   * 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(CVC4::prop::minisat::Var v) const;
+  bool isVarMapped(SatVariable var) const;
 
   /**
    * Returns the atom mapped by the variable v.
-   * @param v the variable to do the lookup by
+   * @param var the variable to do the lookup by
    * @return an atom
    */
-  Node lookupVar(CVC4::prop::minisat::Var v) const;
-
-
+  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 & d_lit2node.
-   * @param c the clause to be asserted.
+   * 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(CVC4::prop::minisat::vec<CVC4::prop::minisat::Lit> & c);
+  void assertClause(SatClause& clause);
 
-  
   /** The CNF converter in use */
-  CVC4::prop::CnfStream *d_cnfStream;
-
+  CnfStream* d_cnfStream;
 
-  void assertLit(CVC4::prop::minisat::Lit l);
+  void assertLit(SatLiteral lit);
   void signalBooleanPropHasEnded();
 
 public:
 
-
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  CVC4_PUBLIC PropEngine(const CVC4::Options* opts,
-                         CVC4::DecisionEngine&,
-                         CVC4::TheoryEngine&);
+  PropEngine(const Options* opts, DecisionEngine*, TheoryEngine*);
+
+  /**
+   * Destructor.
+   */
   CVC4_PUBLIC ~PropEngine();
 
   /**
@@ -157,28 +150,27 @@ public:
    */
   Result solve();
 
-
 };/* class PropEngine */
 
-
-inline bool PropEngine::isAtomMapped(const Node & n) const{
+inline bool PropEngine::isAtomMapped(const Node & n) const {
   return d_atom2var.find(n) != d_atom2var.end();
 }
 
-inline CVC4::prop::minisat::Var PropEngine::lookupAtom(const Node & n) const{
+inline SatVariable PropEngine::lookupAtom(const Node & n) const {
   Assert(isAtomMapped(n));
   return d_atom2var.find(n)->second;
 }
 
-inline bool PropEngine::isVarMapped(CVC4::prop::minisat::Var v) const {
+inline bool PropEngine::isVarMapped(SatVariable v) const {
   return d_var2atom.find(v) != d_var2atom.end();
 }
 
-inline Node PropEngine::lookupVar(CVC4::prop::minisat::Var v) const {
+inline Node PropEngine::lookupVar(SatVariable v) const {
   Assert(isVarMapped(v));
   return d_var2atom.find(v)->second;
 }
 
+}/* prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP_ENGINE_H */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 679b9da8c..195323755 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -16,10 +16,60 @@
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H
 
+#define __CVC4_USE_MINISAT
+
+#ifdef __CVC4_USE_MINISAT
+
+#include "prop/minisat/core/Solver.h"
+#include "prop/minisat/core/SolverTypes.h"
+
 namespace CVC4 {
 namespace prop {
 
+/** The solver we are using */
+typedef minisat::Solver SatSolver;
+
+/** Type of the SAT variables */
+typedef minisat::Var SatVariable;
+
+/** Type of the Sat literals */
+typedef minisat::Lit SatLiteral;
+
+/** Type of the SAT clauses */
+typedef minisat::vec<SatLiteral> SatClause;
+
+/**
+ * Returns the variable of the literal.
+ * @param lit the literal
+ */
+inline SatVariable literalToVariable(SatLiteral lit) {
+  return minisat::var(lit);
+}
+
+inline bool literalSign(SatLiteral lit) {
+  return minisat::sign(lit);
+}
+
+inline std::ostream& operator << (std::ostream& out, SatLiteral lit) {
+  const char * s = (literalSign(lit)) ? "~" : " ";
+  out << s << literalToVariable(lit);
+  return out;
+}
+
+inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
+  out << "clause:";
+  for(int i = 0; i < clause.size(); ++i) {
+    out << " " << clause[i];
+  }
+  out << ";";
+  return out;
+}
+
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
+#endif
+
+
 #endif /* __CVC4__PROP__SAT_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1555acb7d..a04d16d06 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -13,11 +13,14 @@
  **/
 
 #include "smt/smt_engine.h"
-#include "util/exception.h"
 #include "expr/command.h"
-#include "util/output.h"
 #include "expr/node_builder.h"
+#include "util/output.h"
+#include "util/exception.h"
 #include "util/options.h"
+#include "prop/prop_engine.h"
+
+using namespace CVC4::prop;
 
 namespace CVC4 {
 
@@ -25,13 +28,17 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_assertions(),
   d_publicEm(em),
   d_nm(em->getNodeManager()),
-  d_opts(opts),
-  d_de(),
-  d_te(),
-  d_prop(opts, d_de, d_te) {
+  d_opts(opts)
+{
+  d_de = new DecisionEngine();
+  d_te = new TheoryEngine();
+  d_prop = new PropEngine(opts, d_de, d_te);
 }
 
 SmtEngine::~SmtEngine() {
+   delete d_prop;
+   delete d_te;
+   delete d_de;
 }
 
 void SmtEngine::doCommand(Command* c) {
@@ -45,7 +52,7 @@ 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_prop->assertFormula(d_assertions[i]);
   }
   d_assertions.clear();
 }
@@ -54,7 +61,7 @@ void SmtEngine::processAssertionList() {
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
   processAssertionList();
-  return d_prop.solve();
+  return d_prop->solve();
 }
 
 Result SmtEngine::quickCheck() {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 79a35a6a1..eb9384ca5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,14 +19,10 @@
 #include <vector>
 
 #include "cvc4_config.h"
-#include "expr/node.h"
 #include "expr/expr.h"
-#include "expr/node_manager.h"
-#include "expr/node_builder.h"
 #include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
-#include "prop/prop_engine.h"
 #include "util/decision_engine.h"
 
 // In terms of abstraction, this is below (and provides services to)
@@ -37,6 +33,11 @@ namespace CVC4 {
 
 class Command;
 class Options;
+class TheoryEngine;
+
+namespace prop {
+  class PropEngine;
+}
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -125,13 +126,13 @@ private:
   const Options* d_opts;
 
   /** The decision engine */
-  DecisionEngine d_de;
+  DecisionEngine* d_de;
 
   /** The decision engine */
-  TheoryEngine d_te;
+  TheoryEngine* d_te;
 
   /** The propositional engine */
-  PropEngine d_prop;
+  prop::PropEngine* d_prop;
 
 
   /**