summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp53
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/bv/bv_to_int1.smt28
-rw-r--r--test/regress/regress0/bv/bv_to_int_5230_binary.smt29
-rw-r--r--test/regress/regress0/bv/bv_to_int_5230_missing_op.smt27
-rw-r--r--test/regress/regress0/bv/bv_to_int_5230_shift_const.smt212
-rw-r--r--test/regress/regress0/bv/bv_to_int_zext.smt22
-rw-r--r--test/regress/regress2/bv_to_int_ashr.smt24
-rw-r--r--test/regress/regress2/bv_to_int_mask_array_3.smt22
-rw-r--r--test/regress/regress2/bv_to_int_shifts.smt22
-rw-r--r--test/regress/regress3/bv_to_int_signed_sub_or.smt212
11 files changed, 57 insertions, 57 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 6f6ff3bae..8906ddeea 100644
--- 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 f239492af..aedc27924 100644
--- 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 9111ac25c..8410d04b9 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=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
index 000000000..32680d862
--- /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
index 000000000..757b00e5f
--- /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
index 000000000..e94e0cae5
--- /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 42e06a940..8bf4a825d 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=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 5516f974b..b95dc6b7f 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=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 37582d9d8..74e5ca95a 100644
--- 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 7971b2bfe..bcc31c38c 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=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
index 50cce4511..000000000
--- 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback