summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp8
-rw-r--r--src/smt/set_defaults.cpp19
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp13
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/bv/bv-int-collapse1.smt22
-rw-r--r--test/regress/regress0/bv/bv-int-collapse2.smt22
-rw-r--r--test/regress/regress0/bv/bv2nat-simp-range.smt21
-rw-r--r--test/regress/regress1/bv/bv2nat-ground.smt22
-rw-r--r--test/regress/regress1/bv2int-isabelle.smt216
-rw-r--r--test/regress/regress2/bv_to_int_mask_array_1.smt22
10 files changed, 52 insertions, 14 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index b6f53f8c2..ad2707035 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -408,6 +408,14 @@ Node BVToInt::translateWithChildren(Node original,
returnNode = translated_children[0];
break;
}
+ case kind::INT_TO_BITVECTOR:
+ {
+ // ((_ int2bv n) t) ---> (mod t 2^n)
+ size_t sz = original.getOperator().getConst<IntToBitVector>().d_size;
+ returnNode = d_nm->mkNode(
+ kind::INTS_MODULUS_TOTAL, translated_children[0], pow2(sz));
+ }
+ break;
case kind::BITVECTOR_AND:
{
// We support three configurations:
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index b9095c91b..31d14c569 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -163,15 +163,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
}
}
- /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers
- * we need to eagerly eliminate the operators. */
- if (options::bvSolver() == options::BVSolver::SIMPLE
- || options::bvSolver() == options::BVSolver::BITBLAST)
- {
- opts.bv.bvLazyReduceExtf = false;
- opts.bv.bvLazyRewriteExtf = false;
- }
-
/* Disable bit-level propagation by default for the BITBLAST solver. */
if (options::bvSolver() == options::BVSolver::BITBLAST)
{
@@ -198,6 +189,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
{
+ // do not rewrite bv2nat eagerly
+ opts.bv.bvLazyRewriteExtf = true;
if (options::boolToBitvector() != options::BoolToBVMode::OFF)
{
throw OptionException(
@@ -222,6 +215,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
logic.lock();
}
}
+ else if (options::bvSolver() == options::BVSolver::SIMPLE
+ || options::bvSolver() == options::BVSolver::BITBLAST)
+ {
+ // Only BVSolver::LAZY natively supports int2bv and nat2bv, for other
+ // solvers we need to eagerly eliminate the operators. Note this is only
+ // applied if we are not eliminating BV (e.g. with solveBVAsInt).
+ opts.bv.bvLazyReduceExtf = false;
+ }
// set options about ackermannization
if (options::ackermann() && options::produceModels()
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 476803c59..4e1076763 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -64,7 +64,18 @@ TrustNode TheoryBVRewriter::expandDefinition(Node node)
case kind::BITVECTOR_SDIV:
case kind::BITVECTOR_SREM:
case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break;
-
+ case kind::BITVECTOR_TO_NAT:
+ if (!options::bvLazyReduceExtf())
+ {
+ ret = utils::eliminateBv2Nat(node);
+ }
+ break;
+ case kind::INT_TO_BITVECTOR:
+ if (!options::bvLazyReduceExtf())
+ {
+ ret = utils::eliminateInt2Bv(node);
+ }
+ break;
default: break;
}
if (!ret.isNull() && node != ret)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b94e06e47..9ad4f7e8a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1495,6 +1495,7 @@ set(regress_1_tests
regress1/bags/union_disjoint.smt2
regress1/bags/union_max1.smt2
regress1/bags/union_max2.smt2
+ regress1/bv2int-isabelle.smt2
regress1/bv/bench_38.delta.smt2
regress1/bv/bug787.smt2
regress1/bv/bug_extract_mult_leading_bit.smt2
diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2
index 1f5015d14..60826da85 100644
--- a/test/regress/regress0/bv/bv-int-collapse1.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=lazy
+; COMMAND-LINE: --solve-bv-as-int=sum
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2
index d56188dad..130b045d9 100644
--- a/test/regress/regress0/bv/bv-int-collapse2.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=lazy
+; COMMAND-LINE: --solve-bv-as-int=sum
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2
index 31e2b7bd1..daae6a1c3 100644
--- a/test/regress/regress0/bv/bv2nat-simp-range.smt2
+++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2
index 7e0da282e..b68051719 100644
--- a/test/regress/regress1/bv/bv2nat-ground.smt2
+++ b/test/regress/regress1/bv/bv2nat-ground.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=lazy
+; COMMAND-LINE: --solve-bv-as-int=sum
; EXPECT: unsat
(set-logic QF_BVLIA)
(set-info :status unsat)
diff --git a/test/regress/regress1/bv2int-isabelle.smt2 b/test/regress/regress1/bv2int-isabelle.smt2
new file mode 100644
index 000000000..e8d1efe51
--- /dev/null
+++ b/test/regress/regress1/bv2int-isabelle.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun s$ () (_ BitVec 32))
+(declare-fun x$ () (_ BitVec 32))
+(declare-fun i$ () (_ BitVec 32))
+(define-fun bound () Int (bv2nat ((_ int2bv 32) 2048)))
+(define-fun bseg ((x (_ BitVec 32)) (s (_ BitVec 32))) Bool (and (< (bv2nat x) bound) (<= (+ (bv2nat x) (bv2nat s)) bound)))
+
+;assumptions
+(assert (bseg x$ s$))
+(assert (<= (bv2nat i$) (bv2nat s$)))
+
+;conclusion
+(assert (not (= (bv2nat (bvadd x$ i$)) (+ (bv2nat x$) (bv2nat i$)))))
+(check-sat)
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 c8cf40abf..165e39e7a 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,7 +1,7 @@
; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
-; COMMAND-LINE: --solve-bv-as-int=bv
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
; EXPECT: unsat
(set-logic ALL)
(declare-fun A () (Array Int Int))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback