* simplifying equality engine interface

* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations

12 files changed, 100 insertions, 8 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 124fc35f1..4868db6f5 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -73,7 +73,7 @@ SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) {
   return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate));
 }
 
-void BVMinisatSatSolver::notify() {
+void BVMinisatSatSolver::contextNotifyPop() {
   while (d_assertionsCount > d_assertionsRealCount) {
     popAssumption();
     d_assertionsCount --;
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index cd2a2c6b9..60cdd1c28 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -54,6 +54,10 @@ private:
   context::CDO<unsigned> d_assertionsRealCount;
   context::CDO<unsigned> d_lastPropagation;
 
+protected:
+
+  void contextNotifyPop();
+
 public:
 
   BVMinisatSatSolver() :
@@ -70,10 +74,12 @@ public:
 
   SatVariable newVar(bool theoryAtom = false);
 
+  SatVariable trueVar() { return d_minisat->trueVar(); }
+  SatVariable falseVar() { return d_minisat->falseVar(); }
+
   void markUnremovable(SatLiteral lit);
 
   void interrupt();
-  void notify(); 
   
   SatValue solve();
   SatValue solve(long unsigned int&);
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index e24fcac1a..c96b6e4b2 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -119,7 +119,15 @@ Solver::Solver(CVC4::context::Context* c) :
   , propagation_budget (-1)
   , asynch_interrupt   (false)
   , clause_added(false)
-{}
+{
+  // Create the constant variables
+  varTrue = newVar(true, false);
+  varFalse = newVar(false, false);
+
+  // Assert the constants
+  uncheckedEnqueue(mkLit(varTrue, false));
+  uncheckedEnqueue(mkLit(varFalse, true));
+}
 
 
 Solver::~Solver()
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index c323bfe2b..ae5efd81e 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -64,6 +64,12 @@ class Solver {
     /** Cvc4 context */
     CVC4::context::Context* c;
 
+    /** True constant */
+    Var varTrue;
+
+    /** False constant */
+    Var varFalse;
+
 public:
 
     // Constructor/Destructor:
@@ -76,6 +82,9 @@ public:
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+    Var     trueVar() const { return varTrue; }
+    Var     falseVar() const { return varFalse; }
+
 
     bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. 
     bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index c8ce13410..59820e9e3 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -63,11 +63,25 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) :
   , bwdsub_assigns     (0)
   , n_touched          (0)
 {
-  CVC4::StatisticsRegistry::registerStat(&total_eliminate_time); 
+    CVC4::StatisticsRegistry::registerStat(&total_eliminate_time);
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(dummy);
     remove_satisfied      = false;
+
+    // add the initialization for all the internal variables
+    for (int i = frozen.size(); i < vardata.size(); ++ i) {
+      frozen    .push(1);
+      eliminated.push(0);
+      if (use_simplification){
+          n_occ     .push(0);
+          n_occ     .push(0);
+          occurs    .init(i);
+          touched   .push(0);
+          elim_heap .insert(i);
+      }
+    }
+
 }
 
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 3a4fa781a..d18ec6e69 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -175,7 +175,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   SatLiteral lit;
   if (!hasLiteral(node)) {
     // If no literal, we'll make one
-    lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
+    if (node.getKind() == kind::CONST_BOOLEAN) {
+      if (node.getConst<bool>()) {
+        lit = SatLiteral(d_satSolver->trueVar());
+      } else {
+        lit = SatLiteral(d_satSolver->falseVar());
+      }
+    } else {
+      lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
+    }
     d_translationCache[node].literal = lit;
     d_translationCache[node.notNode()].literal = ~lit;
   } else {
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5e1b032a3..6ee508eba 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -126,6 +126,14 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
   , asynch_interrupt   (false)
 {
   PROOF(ProofManager::initSatProof(this);)
+
+  // Create the constant variables
+  varTrue = newVar(true, false, false);
+  varFalse = newVar(false, false, false);
+
+  // Assert the constants
+  uncheckedEnqueue(mkLit(varTrue, false));
+  uncheckedEnqueue(mkLit(varFalse, true));
 }
 
 
@@ -190,16 +198,26 @@ CRef Solver::reason(Var x) {
 
     // Compute the assertion level for this clause
     int explLevel = 0;
-    for (int i = 0; i < explanation.size(); ++ i) {
+    int i, j;
+    for (i = 0, j = 0; i < explanation.size(); ++ i) {
       int varLevel = intro_level(var(explanation[i]));
       if (varLevel > explLevel) {
         explLevel = varLevel;
       }
       Assert(value(explanation[i]) != l_Undef);
       Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i])));
+      // ignore zero level literals
+      if (i == 0 || level(var(explanation[i])) > 0) {
+        explanation[j++] = explanation[i];
+      }
+    }
+    explanation.shrink(i - j);
+    if (j == 1) {
+      // Add not TRUE to the clause
+      explanation.push(mkLit(varTrue, true));
     }
 
-    // Construct the reason (level 0)
+    // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
     vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index cfeb06211..e677d7220 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -65,6 +65,13 @@ protected:
 
   /** The current assertion level (user) */
   int assertionLevel; 
+
+  /** Variable representing true */
+  Var varTrue;
+
+  /** Variable representing false */
+  Var varFalse;
+
 public:
   /** Returns the current user assertion level */
   int getAssertionLevel() const { return assertionLevel; }
@@ -108,6 +115,8 @@ public:
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
+    Var     trueVar() const { return varTrue; }
+    Var     falseVar() const { return varFalse; }
 
     // Less than for literals in a lemma
     struct lemma_lt {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bed30d658..4f2a16670 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -121,7 +121,6 @@ SatVariable MinisatSatSolver::newVar(bool theoryAtom) {
   return d_minisat->newVar(true, true, theoryAtom);
 }
 
-
 SatValue MinisatSatSolver::solve(unsigned long& resource) {
   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 9cf75a12e..19ade8ffa 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -56,6 +56,8 @@ public:
   void addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool theoryAtom = false);
+  SatVariable trueVar() { return d_minisat->trueVar(); }
+  SatVariable falseVar() { return d_minisat->falseVar(); }
 
   SatValue solve();
   SatValue solve(long unsigned int&);
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 2cacfbcc0..8da3856ff 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -67,6 +67,19 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(0, dummy);
     remove_satisfied      = false;
+
+    // add the initialization for all the internal variables
+    for (int i = frozen.size(); i < vardata.size(); ++ i) {
+      frozen    .push(1);
+      eliminated.push(0);
+      if (use_simplification){
+          n_occ     .push(0);
+          n_occ     .push(0);
+          occurs    .init(i);
+          touched   .push(0);
+          elim_heap .insert(i);
+      }
+    }
 }
 
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 898709c43..2865f2cb5 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -46,6 +46,12 @@ public:
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
  
+  /** Create a new (or return an existing) boolean variable representing the constant true */
+  virtual SatVariable trueVar() = 0;
+
+  /** Create a new (or return an existing) boolean variable representing the constant false */
+  virtual SatVariable falseVar() = 0;
+
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve() = 0;