* added propagation as lemmas to TheoryBV:

   * modified BVMinisat to work incrementally
   * added more bv regressions 

3 files changed, 170 insertions, 30 deletions

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 7ff7b50db..5066d5d8f 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -22,8 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "mtl/Sort.h"
 #include "core/Solver.h"
+#include <vector>
 #include <iostream>
 #include "util/output.h"
+#include "util/utility.h"
 
 using namespace BVMinisat;
 
@@ -64,7 +66,7 @@ static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction o
 // Constructor/Destructor:
 
 
-Solver::Solver() :
+Solver::Solver(CVC4::context::Context* c) :
 
     // Parameters (user settable):
     //
@@ -112,6 +114,8 @@ Solver::Solver() :
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
+  , only_bcp(false)
+  , d_explanations(c)
 {}
 
 
@@ -134,6 +138,7 @@ Var Solver::newVar(bool sign, bool dvar)
     watches  .init(mkLit(v, true ));
     assigns  .push(l_Undef);
     vardata  .push(mkVarData(CRef_Undef, 0));
+    marker   .push(0);
     //activity .push(0);
     activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
     seen     .push(0);
@@ -226,13 +231,20 @@ void Solver::cancelUntil(int level) {
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
+            if (marker[x] == 2) marker[x] = 1;
             if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
                 polarity[x] = sign(trail[c]);
             insertVarOrder(x); }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
-    } }
+    }
+
+    if (level < atom_propagations_lim.size()) {
+      atom_propagations.shrink(atom_propagations.size() - atom_propagations_lim[level]);
+      atom_propagations_lim.shrink(atom_propagations_lim.size() - level);
+    }
+}
 
 
 //=================================================================================================
@@ -278,7 +290,7 @@ Lit Solver::pickBranchLit()
 |        rest of literals. There may be others from the same level though.
 |  
 |________________________________________________________________________________________________@*/
-void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
+void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip)
 {
     int pathC = 0;
     Lit p     = lit_Undef;
@@ -288,6 +300,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     out_learnt.push();      // (leave room for the asserting literal)
     int index   = trail.size() - 1;
 
+    bool done = false;
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
         Clause& c = ca[confl];
@@ -315,7 +328,18 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         seen[var(p)] = 0;
         pathC--;
 
-    }while (pathC > 0);
+        switch (uip) {
+        case UIP_FIRST:
+          done = pathC == 0;
+          break;
+        case UIP_LAST:
+          done = confl == CRef_Undef || (pathC == 0 && marker[var(p)] == 2);
+          break;
+        default:
+          Unreachable();
+          break;
+        }
+    } while (!done);
     out_learnt[0] = ~p;
 
     // Simplify conflict clause:
@@ -427,8 +451,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
         Var x = var(trail[i]);
         if (seen[x]){
             if (reason(x) == CRef_Undef){
+              if (marker[x] == 2) {
                 assert(level(x) > 0);
                 out_conflict.push(~trail[i]);
+              }
             }else{
                 Clause& c = ca[reason(x)];
                 for (int j = 1; j < c.size(); j++)
@@ -449,8 +475,34 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     assigns[var(p)] = lbool(!sign(p));
     vardata[var(p)] = mkVarData(from, decisionLevel());
     trail.push_(p);
+    if (only_bcp && marker[var(p)] == 1 && from != CRef_Undef) {
+      atom_propagations.push(p);
+    }
+}
+
+void Solver::popAssumption() {
+  marker[var(assumptions.last())] = 1;
+  assumptions.pop();
+  conflict.clear();
+  cancelUntil(assumptions.size());
 }
 
+lbool Solver::assertAssumption(Lit p, bool propagate) {
+
+  assert(marker[var(p)] == 1);
+
+  // add to the assumptions
+  assumptions.push(p);
+  conflict.clear();
+
+  // run the propagation
+  if (propagate) {
+    only_bcp = true;
+    return search(-1, UIP_FIRST);
+  } else {
+    return l_True;
+  }
+}
 
 /*_________________________________________________________________________________________________
 |
@@ -628,7 +680,7 @@ bool Solver::simplify()
 |    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
 |    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
 |________________________________________________________________________________________________@*/
-lbool Solver::search(int nof_conflicts)
+lbool Solver::search(int nof_conflicts, UIP uip)
 {
     assert(ok);
     int         backtrack_level;
@@ -644,17 +696,27 @@ lbool Solver::search(int nof_conflicts)
             if (decisionLevel() == 0) return l_False;
 
             learnt_clause.clear();
-            analyze(confl, learnt_clause, backtrack_level);
+            analyze(confl, learnt_clause, backtrack_level, uip);
             cancelUntil(backtrack_level);
 
+            Lit p = learnt_clause[0];
+            bool assumption = marker[var(p)] == 2;
+
             if (learnt_clause.size() == 1){
-                uncheckedEnqueue(learnt_clause[0]);
+                uncheckedEnqueue(p);
             }else{
                 CRef cr = ca.alloc(learnt_clause, true);
                 learnts.push(cr);
                 attachClause(cr);
                 claBumpActivity(ca[cr]);
-                uncheckedEnqueue(learnt_clause[0], cr);
+                uncheckedEnqueue(p, cr);
+            }
+
+            // if an assumption, we're done
+            if (assumption) {
+              assert(decisionLevel() < assumptions.size());
+              analyzeFinal(p, conflict);
+              return l_False;
             }
 
             varDecayActivity();
@@ -699,12 +761,18 @@ lbool Solver::search(int nof_conflicts)
                     analyzeFinal(~p, conflict);
                     return l_False;
                 }else{
+                    marker[var(p)] = 2;
                     next = p;
                     break;
                 }
             }
 
             if (next == lit_Undef){
+
+                if (only_bcp) {
+                  return l_True;
+                }
+
                 // New variable decision:
                 decisions++;
                 next = pickBranchLit();
@@ -767,10 +835,12 @@ static double luby(double y, int x){
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
-  Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n";
-  Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n"; 
+    Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n";
+    Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n";
+
     model.clear();
     conflict.clear();
+
     if (!ok) return l_False;
 
     solves++;
@@ -799,19 +869,56 @@ lbool Solver::solve_()
     if (verbosity >= 1)
         printf("===============================================================================\n");
 
-
     if (status == l_True){
         // Extend & copy model:
-        model.growTo(nVars());
-        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+        // model.growTo(nVars());
+        // for (int i = 0; i < nVars(); i++) model[i] = value(i);
     }else if (status == l_False && conflict.size() == 0)
         ok = false;
 
-    cancelUntil(0);
     return status;
 }
 
 //=================================================================================================
+// Bitvector propagations
+// 
+
+void Solver::storeExplanation(Lit p) {
+}
+
+void Solver::explainPropagation(Lit p, std::vector<Lit>& explanation) {
+  vec<Lit> queue;
+  queue.push(p);
+
+  __gnu_cxx::hash_set<Var> visited;
+  visited.insert(var(p));
+  while(queue.size() > 0) {
+    Lit l = queue.last();
+    assert(value(l) == l_True);
+    queue.pop();
+    if (reason(var(l)) == CRef_Undef) {
+      if (marker[var(l)] == 2) {
+        explanation.push_back(l);
+        visited.insert(var(l));
+      }
+    } else {
+      Clause& c = ca[reason(var(l))];
+      for (int i = 1; i < c.size(); ++i) {
+        if (var(c[i]) >= vardata.size()) {
+          std::cerr << "BOOM" << std::endl;
+        }
+        if (visited.count(var(c[i])) == 0) {
+          queue.push(~c[i]);
+          visited.insert(var(c[i]));
+        }
+      }
+    }
+  }
+}
+
+  
+
+//=================================================================================================
 // Writing CNF to DIMACS:
 // 
 // FIXME: this needs to be rewritten completely.
@@ -872,13 +979,13 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
         }
 
     // Assumptions are added as unit clauses:
-    cnt += assumptions.size();
+    cnt += assumps.size();
 
     fprintf(f, "p cnf %d %d\n", max, cnt);
 
-    for (int i = 0; i < assumptions.size(); i++){
-        assert(value(assumptions[i]) != l_False);
-        fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
+    for (int i = 0; i < assumps.size(); i++){
+        assert(value(assumps[i]) != l_False);
+        fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
     }
 
     for (int i = 0; i < clauses.size(); i++)
@@ -940,4 +1047,3 @@ void Solver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
-
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index f364a2937..33d1900c9 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -27,6 +27,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Alg.h"
 #include "prop/bvminisat/utils/Options.h"
 
+#include "context/cdhashmap.h"
+
+#include <ext/hash_set>
+#include <vector>
 
 namespace BVMinisat {
 
@@ -38,7 +42,7 @@ public:
 
     // Constructor/Destructor:
     //
-    Solver();
+    Solver(CVC4::context::Context* c);
     virtual ~Solver();
 
     // Problem specification:
@@ -63,6 +67,8 @@ public:
     bool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
     bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
+    lbool   assertAssumption(Lit p, bool propagate);  // Assert a new assumption, start BCP if propagate = true
+    void    popAssumption();                        // Pop an assumption
 
     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
     void    toDimacs     (const char *file, const vec<Lit>& assumps);
@@ -138,7 +144,20 @@ public:
     uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 
-     
+    // Bitvector Propagations
+    //
+
+    void addMarkerLiteral(Var var) {
+      marker[var] = 1;
+    }
+
+    __gnu_cxx::hash_set<Var> assumptions_vars; // all the variables that appear in the current assumptions
+    vec<Lit> atom_propagations;         // the atom literals implied by the last call to solve with assumptions
+    vec<int> atom_propagations_lim;     // for backtracking
+
+    bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
+    void setOnlyBCP (bool val) { only_bcp = val;}
+    void explainPropagation(Lit l, std::vector<Lit>& explanation);
 protected:
 
     // Helper structures:
@@ -179,6 +198,7 @@ protected:
                         watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
     vec<lbool>          assigns;          // The current assignments.
     vec<char>           polarity;         // The preferred polarity of each variable.
+    vec<char>           marker;           // Is the variable a marker literal
     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
@@ -220,10 +240,19 @@ protected:
     bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
     CRef     propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
-    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
+
+    enum UIP {
+      UIP_FIRST,
+      UIP_LAST
+    };
+
+    CVC4::context::CDHashMap<Lit, std::vector<Lit>, LitHashFunction> d_explanations;
+
+    void     storeExplanation (Lit p);                                                 // make sure that the explanation of p is cached
+    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST);    // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
-    lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
+    lbool    search           (int nof_conflicts, UIP uip = UIP_FIRST);                // Search for a given number of conflicts.
     lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').
     void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
     void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.
@@ -275,8 +304,8 @@ protected:
 //=================================================================================================
 // Implementation of inline methods:
 
-inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
-inline int  Solver::level (Var x) const { return vardata[x].level; }
+inline CRef Solver::reason(Var x) const { assert(x < vardata.size()); return vardata[x].reason; }
+inline int  Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; }
 
 inline void Solver::insertVarOrder(Var x) {
     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
@@ -315,7 +344,7 @@ inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); atom_propagations_lim.push(atom_propagations.size()); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 0439a46c4..89ffc8a00 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -53,7 +53,6 @@ struct Lit {
     bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
 };
 
-
 inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
 inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
 inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
@@ -61,9 +60,15 @@ inline  bool sign      (Lit p)              { return p.x & 1; }
 inline  int  var       (Lit p)              { return p.x >> 1; }
 
 // Mapping Literals to and from compact integers suitable for array indexing:
-inline  int  toInt     (Var v)              { return v; } 
-inline  int  toInt     (Lit p)              { return p.x; } 
-inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; } 
+inline  int  toInt     (Var v)              { return v; }
+inline  int  toInt     (Lit p)              { return p.x; }
+inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; }
+
+struct LitHashFunction {
+  size_t operator () (const Lit& l) const {
+    return toInt(l);
+  }
+};
 
 //const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
 //const Lit lit_Error = mkLit(var_Undef, true );  // }