From 027ed263703823adf3c9f7e9fa11df0832f538b0 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 19 Mar 2020 10:12:10 -0700 Subject: [PATCH] Bv2int fail on demand Postpone failure in bv-to-int preprocessing pass. --- src/preprocessing/passes/bv_to_int.cpp | 85 +++++++++++++------ src/preprocessing/passes/bv_to_int.h | 2 + src/smt/smt_engine.cpp | 1 - test/regress/CMakeLists.txt | 2 + .../regress2/bv_to_int_mask_array_1.smt2 | 10 +++ .../regress2/bv_to_int_mask_array_2.smt2 | 9 ++ 6 files changed, 82 insertions(+), 27 deletions(-) create mode 100644 test/regress/regress2/bv_to_int_mask_array_1.smt2 create mode 100644 test/regress/regress2/bv_to_int_mask_array_2.smt2 diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 75136913c..cb78b0897 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -23,6 +23,7 @@ #include #include "expr/node.h" +#include "options/uf_options.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" @@ -315,9 +316,7 @@ Node BVToInt::bvToInt(Node n) } else { - // Boolean variables are left unchanged. - AlwaysAssert(current.getType() == d_nm->booleanType() - || current.getType().isSort()); + // variables other than bit-vector variables are left intact d_bvToIntCache[current] = current; } } @@ -696,6 +695,8 @@ Node BVToInt::bvToInt(Node n) * We cache both the term itself (e.g., f(a)) and the function * symbol f. */ + + //Construct the function itself Node bvUF = current.getOperator(); Node intUF; TypeNode tn = current.getOperator().getType(); @@ -729,38 +730,57 @@ Node BVToInt::bvToInt(Node n) // Insert the function symbol itself to the cache d_bvToIntCache[bvUF] = intUF; } - translated_children.insert(translated_children.begin(), intUF); - // Insert the term to the cache - d_bvToIntCache[current] = - d_nm->mkNode(kind::APPLY_UF, translated_children); + if (childrenTypesChanged(current) && options::ufHo()) { /** - * Add range constraints if necessary. - * If the original range was a BV sort, the current application of - * the fucntion Must be within the range determined by the - * bitwidth. + * higher order logic allows comparing between functions + * The current translation does not support this, + * as the translated functions may be different outside + * of the bounds that were relevant for the original + * bit-vectors. */ - if (bvRange.isBitVector()) - { - d_rangeAssertions.insert( - mkRangeConstraint(d_bvToIntCache[current], - current.getType().getBitVectorSize())); + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to Int: ") + current.toString()); } - break; + else { + translated_children.insert(translated_children.begin(), intUF); + // Insert the term to the cache + d_bvToIntCache[current] = + d_nm->mkNode(kind::APPLY_UF, translated_children); + /** + * Add range constraints if necessary. + * If the original range was a BV sort, the current application of + * the function Must be within the range determined by the + * bitwidth. + */ + if (bvRange.isBitVector()) + { + d_rangeAssertions.insert( + mkRangeConstraint(d_bvToIntCache[current], + current.getType().getBitVectorSize())); + } + } + break; } default: { - if (Theory::theoryOf(current) == THEORY_BOOL) - { + if (childrenTypesChanged(current)) { + /** + * This is "failing on demand": + * We throw an exception if we encounter a case + * that we do not know how to translate, + * only if we actually need to construct a new + * node for such a case. + */ + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to Int: ") + current.toString()); + } + else { d_bvToIntCache[current] = d_nm->mkNode(oldKind, translated_children); - break; - } - else - { - // Currently, only QF_UFBV formulas are handled. - // In the future, more theories should be supported, e.g., arrays. - Unimplemented(); } + break; } } } @@ -771,6 +791,19 @@ Node BVToInt::bvToInt(Node n) return d_bvToIntCache[n]; } +bool BVToInt::childrenTypesChanged(Node n) { + bool result = false; + for (Node child : n) { + TypeNode originalType = child.getType(); + TypeNode newType = d_bvToIntCache[child].getType(); + if (! newType.isSubtypeOf(originalType)) { + result = true; + break; + } + } + return result; +} + BVToInt::BVToInt(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-int"), d_binarizeCache(), diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index dd02d98ec..f0e0ea02e 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -231,6 +231,8 @@ class BVToInt : public PreprocessingPass */ Node modpow2(Node n, uint64_t exponent); + bool childrenTypesChanged(Node n); + /** * Add the range assertions collected in d_rangeAssertions * (using mkRangeConstraint) to the assertion pipeline. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d096e1fe..d3ba34b6c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1206,7 +1206,6 @@ void SmtEngine::setDefaults() { if (d_logic.isTheoryEnabled(THEORY_BV)) { d_logic = d_logic.getUnlockedCopy(); - d_logic.disableTheory(THEORY_BV); d_logic.enableTheory(THEORY_ARITH); d_logic.arithNonLinear(); d_logic.lock(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 02eb15826..fd4f2aef0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1976,6 +1976,8 @@ set(regress_2_tests regress2/bug765.smt2 regress2/bug812.smt2 regress2/bv_to_int_ashr.smt2 + regress2/bv_to_int_mask_array_1.smt2 + regress2/bv_to_int_mask_array_2.smt2 regress2/bv_to_int_shifts.smt2 regress2/error0.smt2 regress2/error1.smtv1.smt2 diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 new file mode 100644 index 000000000..c1f20a41b --- /dev/null +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic ALL) +(declare-fun A () (Array Int Int)) +(declare-fun f ((_ BitVec 3)) Int) +(declare-fun x () (_ BitVec 3)) +(declare-fun y () (_ BitVec 3)) +(assert (distinct (select A (f (bvand x y))) (select A (f (bvor x y))))) +(assert (= x y)) +(check-sat) diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 new file mode 100644 index 000000000..b88f71064 --- /dev/null +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models --no-check-unsat-cores --no-check-proofs +; EXPECT: sat +(set-logic ALL) +(declare-fun A () (Array Int Int)) +(declare-fun f ((_ BitVec 3)) Int) +(declare-fun x () (_ BitVec 3)) +(declare-fun y () (_ BitVec 3)) +(assert (distinct (select A (f (bvand x y))) (select A (f (bvor x y))))) +(check-sat) -- 2.30.2