bv2int: rewritings and unsat cores (#5263)

This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:

1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 6f6ff3bae307709dc13316dc3b2cb21e711c2715..8906ddeeafc89ac7724bef0439016cfab871cdd7 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -260,6 +260,8 @@ Node BVToInt::eliminationPass(Node n)
  */
 Node BVToInt::bvToInt(Node n)
 {
+  // make sure the node is re-written before processing it.
+  n = Rewriter::rewrite(n);
   n = makeBinary(n);
   n = eliminationPass(n);
   // binarize again, in case the elimination pass introduced
@@ -947,26 +949,17 @@ PreprocessingPassResult BVToInt::applyInternal(
 void BVToInt::addFinalizeRangeAssertions(
     AssertionPipeline* assertionsToPreprocess)
 {
+  // collect the range assertions from d_rangeAssertions
+  // (which is a context-dependent set)
+  // into a vector.
   vector<Node> vec_range;
   vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
-  if (vec_range.size() == 0)
-  {
-    return;
-  }
-  if (vec_range.size() == 1)
-  {
-    assertionsToPreprocess->push_back(vec_range[0]);
-    Trace("bv-to-int-debug")
-        << "range constraints: " << vec_range[0].toString() << std::endl;
-  }
-  else if (vec_range.size() >= 2)
-  {
-    Node rangeAssertions =
-        Rewriter::rewrite(d_nm->mkNode(kind::AND, vec_range));
-    assertionsToPreprocess->push_back(rangeAssertions);
-    Trace("bv-to-int-debug")
-        << "range constraints: " << rangeAssertions.toString() << std::endl;
-  }
+  // conjoin all range assertions and add the conjunction
+  // as a new assertion
+  Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range));
+  assertionsToPreprocess->push_back(rangeAssertions);
+  Trace("bv-to-int-debug") << "range constraints: "
+                           << rangeAssertions.toString() << std::endl;
 }
 
 Node BVToInt::createShiftNode(vector<Node> children,
@@ -1046,24 +1039,12 @@ Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
                              newBoundVars.begin(),
                              newBoundVars.end());
   // A node to represent all the range constraints.
-  Node ranges;
-  if (rangeConstraints.size() > 0)
-  {
-    if (rangeConstraints.size() == 1)
-    {
-      ranges = rangeConstraints[0];
-    }
-    else
-    {
-      ranges = d_nm->mkNode(kind::AND, rangeConstraints);
-    }
-    // Add the range constraints to the body of the quantifier.
-    // For "exists", this is added conjunctively
-    // For "forall", this is added to the left side of an implication.
-    matrix = d_nm->mkNode(
-        k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix);
-  }
-
+  Node ranges = d_nm->mkAnd(rangeConstraints);
+  // Add the range constraints to the body of the quantifier.
+  // For "exists", this is added conjunctively
+  // For "forall", this is added to the left side of an implication.
+  matrix = d_nm->mkNode(
+      k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix);
   // create the new quantified formula and return it.
   Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars);
   Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f239492af5a44ce6b3e6fa6c354cfbc7964414a5..aedc27924aacf4fc9f45891f1947ba957dedec05 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -221,6 +221,9 @@ set(regress_0_tests
   regress0/bv/bv-to-bool1.smtv1.smt2
   regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv_to_int1.smt2
+  regress0/bv/bv_to_int_5230_shift_const.smt2
+  regress0/bv/bv_to_int_5230_binary.smt2
+  regress0/bv/bv_to_int_5230_missing_op.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2

diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 9111ac25c01b3819b247982ea1f9bf4cc5c5ce8a..8410d04b9de7c80c894ab38b364486667cc531d9 100644 (file)
--- 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=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))

diff --git a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2
new file mode 100644 (file)
index 0000000..32680d8
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2
@@ -0,0 +1,9 @@
+; REQUIRES: proof
+; EXPECT: sat
+(set-logic QF_UFBV)
+(set-option :produce-unsat-cores true)
+(set-option :solve-bv-as-int sum)
+(declare-const v8 Bool)
+(declare-const bv_14-0 (_ BitVec 14))
+(declare-const v12 Bool)
+(check-sat-assuming ((! (or (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) (= bv_14-0 bv_14-0 bv_14-0) (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7)))) v12) :named IP_71) (! (or v12 v8 v8 (= ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))) ((_ repeat 5) (bvurem (_ bv77 7) (_ bv77 7))))) :named IP_75)))

diff --git a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2
new file mode 100644 (file)
index 0000000..757b00e
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: proof
+; EXPECT: sat
+(set-logic ABV)
+(set-option :check-unsat-cores true)
+(set-option :solve-bv-as-int sum)
+(assert (! (exists ((q4 (_ BitVec 6))) true) :named IP_2))
+(check-sat)

diff --git a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2
new file mode 100644 (file)
index 0000000..e94e0ca
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: proof
+; EXPECT: sat
+(set-logic QF_UFBV)
+(set-option :check-unsat-cores true)
+(set-option :solve-bv-as-int sum)
+(declare-const v0 Bool)
+(declare-const v5 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110)))  
+(assert (or v0 v8))
+(check-sat)

diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index 42e06a940bea295e609eb1ee9e86c22f16c83a7c..8bf4a825d07692048407e70860941386b83c5f97 100644 (file)
--- 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=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))

diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 5516f974baa86bba83d2a67e89a096b7848f05cc..b95dc6b7f6600109c07b73c0856c68ee6b3a5b2c 100644 (file)
--- 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=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))

diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 37582d9d838bbb0c1a63e16af0d442b914cfbf1a..74e5ca95a46f21430b611078558ad63669aad4ce 100644 (file)
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))

diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index 7971b2bfed844b068eed84c8c3e8f30768185926..bcc31c38c4534b21df16a4502f350c5f61a54c8c 100644 (file)
--- 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=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))

diff --git a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 b/test/regress/regress3/bv_to_int_signed_sub_or.smt2
deleted file mode 100644 (file)
index 50cce45..0000000
--- a/test/regress/regress3/bv_to_int_signed_sub_or.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
-; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores
-; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
-; COMMAND-LINE: --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-unsat-cores
-; EXPECT: unsat
-(set-logic QF_BV)
-(declare-fun s () (_ BitVec 4))
-(declare-fun t () (_ BitVec 4))
-(assert (bvsgt s t))
-(assert (bvsge t (bvsub t (bvor (bvor s t) (bvneg s)))))
-(check-sat)
-(exit)