beautification of the prop engine

1 files changed, 36 insertions, 42 deletions

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