Merge branch 'master' into rmExprSequencermExprSequence

20 files changed, 61 insertions, 36 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 13791bfd6..80183b71f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -639,11 +639,26 @@ header = "options/smt_options.h"
 [[option]]
   name       = "solveBVAsInt"
   category   = "undocumented"
-  long       = "solve-bv-as-int=N"
+  long       = "solve-bv-as-int=MODE"
+  type       = "SolveBVAsIntMode"
+  default    = "OFF"
+  help       = "mode for translating BVAnd to integer"
+  help_mode  = "solve-bv-as-int modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not translate bit-vectors to integers"
+[[option.mode.SUM]]
+  name = "sum"
+  help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
+
+[[option]]
+  name       = "BVAndIntegerGranularity"
+  category   = "undocumented"
+  long       = "bvand-integer-granularity=N"
   type       = "uint32_t"
-  default    = "0"
+  default    = "1"
   read_only  = true
-  help       = "attempt to solve BV formulas by translation to integer arithmetic (experimental)"
+  help       = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)"
 
 [[option]]
   name       = "iandMode"
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 5b125b4b6..bb0bde2f9 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -269,7 +269,7 @@ Node BVToInt::bvToInt(Node n)
   n = makeBinary(n);
   vector<Node> toVisit;
   toVisit.push_back(n);
-  uint64_t granularity = options::solveBVAsInt();
+  uint64_t granularity = options::BVAndIntegerGranularity();
 
   while (!toVisit.empty())
   {
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 4eedfd863..4fed33f3c 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -222,7 +222,7 @@ bool ProcessAssertions::apply(AssertionPipeline& assertions)
   {
     d_passes["bv-to-bool"]->apply(&assertions);
   }
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     d_passes["bv-to-int"]->apply(&assertions);
   }
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4ce4b8db8..11751079e 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -154,7 +154,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     logic.lock();
   }
 
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     // not compatible with incremental
     if (options::incrementalSolving())
@@ -168,7 +168,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       throw OptionException(
           "solving bitvectors as integers is incompatible with --bool-to-bv.");
     }
-    if (options::solveBVAsInt() > 8)
+    if (options::BVAndIntegerGranularity() > 8)
     {
       /**
        * The granularity sets the size of the ITE in each element
@@ -382,7 +382,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
 
 
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     /**
      * Operations on 1 bits are better handled as Boolean operations
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 851ae414e..2bbdcceb3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1787,6 +1787,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
           new std::set<Node>(proofRecipe->getStep(0)->getAssertions()));
     }
   });
+  // cache of nodes we have already explained by some theory
+  std::unordered_set<Node, NodeHashFunction> cache;
 
   while (i < explanationVector.size()) {
     // Get the current literal to explain
@@ -1868,7 +1870,15 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         continue;
       }
     }
-
+    // We must cache after checking the timestamp in the block of code above.
+    // Afterwards, we can ignore this timestamp, as well as caching the Node,
+    // since any theory's explanation will suffice.
+    if (cache.find(toExplain.d_node) != cache.end())
+    {
+      ++i;
+      continue;
+    }
+    cache.insert(toExplain.d_node);
     // It was produced by the theory, so ask for an explanation
     Node explanation;
     if (toExplain.d_theory == THEORY_BUILTIN)
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 1df9ec2d6..d9190128e 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
-; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
index ab1bf10f3..00fd51baf 100644
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ b/test/regress/regress0/bv/bv_to_int2.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
index 52eb78830..4bcbac20c 100644
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
index d0d699b4d..ec4206812 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 541229813..05cd312d7 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
index 16731b01e..b17aeeacf 100644
--- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2
+++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models 
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun _substvar_183_ () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index 3525cebb6..5c6be19b5 100644
--- a/test/regress/regress0/bv/bv_to_int_zext.smt2
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2
index 7176f4012..c621aa112 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
index 297bb2422..3db8e87ee 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
@@ -1,4 +1,4 @@
-;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
 ;EXPECT: unsat
 
 (set-logic QF_UFBV)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
index 873acd6c4..8fbe96eab 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index e3fcb1790..3e0151076 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
-; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index c1f20a41b..a2d90be2d 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index b88f71064..9bab0c71c 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index 39dace123..998234a17 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 64))
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
index 54a491093..185f1b5ec 100644
--- a/test/regress/regress3/bv_to_int_and_or.smt2
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -1,8 +1,8 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
-; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
 (assert (bvult (bvor a b) (bvand a b)))
 (check-sat)