* added propagation as lemmas to TheoryBV:

   * modified BVMinisat to work incrementally
   * added more bv regressions 

1 files changed, 7 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 36ba17b52..d147c8bb5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,6 +24,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/stats.h"
 
@@ -41,7 +42,6 @@ class Bitblaster;
 
 class TheoryBV : public Theory {
 
-public:
 
 private:
 
@@ -54,7 +54,11 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
   Node d_true;
-    
+
+  /** Context dependent set of atoms we already propagated */
+  context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
+
+  bool hasBeenPropagated(TNode node); 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
@@ -66,7 +70,7 @@ public:
 
   void check(Effort e);
 
-  void propagate(Effort e) { }
+  void propagate(Effort e);
 
   Node explain(TNode n);