Merging in bvprop branch, with proper bit-vector propagation.

This should also fix bug 325. 

3 files changed, 73 insertions, 4 deletions

diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index 0dec26717..687272b56 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -31,6 +31,23 @@ namespace CVC4 {
 template<typename Visitor>
 class NodeVisitor {
 
+  /** For re-entry checking */
+  static bool d_inRun;
+
+  class GuardReentry {
+    bool& d_guard;
+  public:
+    GuardReentry(bool& guard)
+    : d_guard(guard) {
+      Assert(!d_guard);
+      d_guard = true;
+    }
+    ~GuardReentry() {
+      Assert(d_guard);
+      d_guard = false;
+    }
+  };
+
 public:
 
   /**
@@ -52,6 +69,8 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
+    GuardReentry guard(d_inRun);
+
     // Notify of a start
     visitor.start(node);
 
@@ -91,5 +110,8 @@ public:
 
 };
 
+template <typename Visitor>
+bool NodeVisitor<Visitor>::d_inRun = false;
+
 }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index e87c240a8..d72734f40 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -119,7 +119,11 @@ Options::Options() :
   threadArgv(),
   thread_id(-1),
   separateOutput(false),
-  sharingFilterByLength(-1)
+  sharingFilterByLength(-1),
+  bitvector_eager_bitblast(false),
+  bitvector_share_lemmas(false),
+  bitvector_eager_fullcheck(false),
+  sat_refine_conflicts(false)
 {
 }
 
@@ -187,10 +191,14 @@ Additional CVC4 options:\n\
    --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
    --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
-   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n \
+   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
    --threads=N            sets the number of solver threads\n\
    --threadN=string       configures thread N (0..#threads-1)\n\
    --filter-lemma-length=N don't share lemmas strictly longer than N\n\
+   --bitblast-eager       eagerly bitblast the bitvectors to the main SAT solver\n\
+   --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\
+   --bitblast-eager-fullcheck check the bitblasting eagerly\n\
+   --refine-conflicts     refine theory conflict clauses\n\
 ";
 
 
@@ -381,7 +389,11 @@ enum OptionValue {
   TIME_LIMIT,
   TIME_LIMIT_PER,
   RESOURCE_LIMIT,
-  RESOURCE_LIMIT_PER
+  RESOURCE_LIMIT_PER,
+  BITVECTOR_EAGER_BITBLAST,
+  BITVECTOR_SHARE_LEMMAS,
+  BITVECTOR_EAGER_FULLCHECK,
+  SAT_REFINE_CONFLICTS
 };/* enum OptionValue */
 
 /**
@@ -473,6 +485,10 @@ static struct option cmdlineOptions[] = {
   { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
   { "rlimit"     , required_argument, NULL, RESOURCE_LIMIT       },
   { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER   },
+  { "bitblast-eager", no_argument, NULL, BITVECTOR_EAGER_BITBLAST },
+  { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS },
+  { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK },
+  { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -894,7 +910,26 @@ throw(OptionException) {
         perCallResourceLimit = (unsigned long) i;
         break;
       }
-
+    case BITVECTOR_EAGER_BITBLAST:
+      {
+        bitvector_eager_bitblast = true;
+        break;
+      }
+    case BITVECTOR_EAGER_FULLCHECK:
+      {
+        bitvector_eager_fullcheck = true;
+        break;
+      }
+    case BITVECTOR_SHARE_LEMMAS:
+      {
+        bitvector_share_lemmas = true;
+        break;
+      }
+    case SAT_REFINE_CONFLICTS:
+      {
+        sat_refine_conflicts = true;
+        break;
+      }
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 6205c7543..eac09fabf 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -283,6 +283,18 @@ struct CVC4_PUBLIC Options {
   /** Filter depending on length of lemma */
   int sharingFilterByLength;
 
+  /** Bitblast eagerly to the main sat solver */
+  bool bitvector_eager_bitblast;
+
+  /** Fullcheck at each check */
+  bool bitvector_eager_fullcheck;
+
+  /** Bitblast eagerly to the main sat solver */
+  bool bitvector_share_lemmas;
+
+  /** Refine conflicts by doing another full check after a conflict */
+  bool sat_refine_conflicts;
+
   Options();
 
   /**