From d19b800ac00feb44bfc6302f02695c8700e15c12 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 24 Mar 2020 10:53:18 -0700 Subject: [PATCH] Int2BV fail on demand (#4079) This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node. --- .../smt-comp/run-script-smtcomp-current | 10 +-- src/preprocessing/passes/int_to_bv.cpp | 64 +++++++++++-------- src/smt/smt_engine.cpp | 10 +-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/bv/bv-abstr-bug2.smt2 | 2 +- .../bv/int_to_bv_err_on_demand_1.smt2 | 11 ++++ 6 files changed, 59 insertions(+), 39 deletions(-) create mode 100644 test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 4c781d47c..b46253851 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -39,11 +39,11 @@ QF_NIA) trywith 60 --nl-ext-tplanes --decision=justification trywith 60 --no-nl-ext-tplanes --decision=internal # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail - trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=2 --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=4 --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=8 --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=16 --bv-sat-solver=cadical --no-bv-abstraction + trywith 1200 --solve-int-as-bv=32 --bv-sat-solver=cadical --no-bv-abstraction finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 372df90ce..9fa9a0c05 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -44,6 +44,20 @@ struct intToBV_stack_element intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {} }; /* struct intToBV_stack_element */ +bool childrenTypesChanged(Node n, NodeMap& cache) { + bool result = false; + for (Node child : n) { + TypeNode originalType = child.getType(); + TypeNode newType = cache[child].getType(); + if (! newType.isSubtypeOf(originalType)) { + result = true; + break; + } + } + return result; +} + + Node intToBVMakeBinary(TNode n, NodeMap& cache) { // Do a topological sort of the subexpressions and substitute them @@ -84,6 +98,10 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) else { NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++i) { Assert(cache.find(current[i]) != cache.end()); @@ -203,13 +221,12 @@ Node intToBV(TNode n, NodeMap& cache) case kind::EQUAL: case kind::ITE: break; default: - if (Theory::theoryOf(current) == THEORY_BOOL) - { - break; - } - throw TypeCheckingException( + if (childrenTypesChanged(current, cache)) { + throw TypeCheckingException( current.toExpr(), string("Cannot translate to BV: ") + current.toString()); + } + break; } for (unsigned i = 0; i < children.size(); ++i) { @@ -229,6 +246,9 @@ Node intToBV(TNode n, NodeMap& cache) } } NodeBuilder<> builder(newKind); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } for (unsigned i = 0; i < children.size(); ++i) { builder << children[i]; @@ -271,10 +291,6 @@ Node intToBV(TNode n, NodeMap& cache) nm->mkBitVectorType(size), "Variable introduced in intToBV pass"); } - else - { - AlwaysAssert(current.getType() == nm->booleanType()); - } } else if (current.isConst()) { @@ -283,25 +299,21 @@ Node intToBV(TNode n, NodeMap& cache) case kind::CONST_RATIONAL: { Rational constant = current.getConst(); - AlwaysAssert(constant.isIntegral()); - AlwaysAssert(constant >= 0); - BitVector bv(size, constant.getNumerator()); - if (bv.toSignedInteger() != constant.getNumerator()) - { - throw TypeCheckingException( - current.toExpr(), - string("Not enough bits for constant in intToBV: ") - + current.toString()); + if (constant.isIntegral()) { + AlwaysAssert(constant >= 0); + BitVector bv(size, constant.getNumerator()); + if (bv.toSignedInteger() != constant.getNumerator()) + { + throw TypeCheckingException( + current.toExpr(), + string("Not enough bits for constant in intToBV: ") + + current.toString()); + } + result = nm->mkConst(bv); } - result = nm->mkConst(bv); break; } - case kind::CONST_BOOLEAN: break; - default: - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate const to BV: ") - + current.toString()); + default: break; } } else @@ -325,7 +337,7 @@ IntToBV::IntToBV(PreprocessingPassContext* preprocContext) PreprocessingPassResult IntToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) { - unordered_map cache; + NodeMap cache; for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { assertionsToPreprocess->replace( diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a367c8469..7d78e93f9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1192,13 +1192,9 @@ void SmtEngine::setDefaults() { if (options::solveIntAsBV() > 0) { - if (!(d_logic <= LogicInfo("QF_NIA"))) - { - throw OptionException( - "--solve-int-as-bv=X only supported for pure integer logics (QF_NIA, " - "QF_LIA, QF_IDL)"); - } - d_logic = LogicInfo("QF_BV"); + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableTheory(THEORY_BV); + d_logic.lock(); } if (options::solveBVAsInt() > 0) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4cd3c70d2..0eb6bc2d2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -358,6 +358,7 @@ set(regress_0_tests regress0/bv/fuzz40.smtv1.smt2 regress0/bv/fuzz41.smtv1.smt2 regress0/bv/issue3621.smt2 + regress0/bv/int_to_bv_err_on_demand_1.smt2 regress0/bv/mul-neg-unsat.smt2 regress0/bv/mul-negpow2.smt2 regress0/bv/mult-pow2-negative.smt2 diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2 index 939439adf..1c8f9b1df 100644 --- a/test/regress/regress0/bv/bv-abstr-bug2.smt2 +++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager +; COMMAND-LINE: --solve-int-as-bv=32 (set-logic QF_NIA) (set-info :status sat) (declare-fun _substvar_7_ () Bool) diff --git a/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 new file mode 100644 index 000000000..1ef63f365 --- /dev/null +++ b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models +; EXPECT: sat +(set-logic ALL) +(declare-sort S 0) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun A () (Array S S)) +(declare-fun f ((_ BitVec 4)) S) + +(assert (distinct (select A (f (_ bv0 4))) (select A (f (_ bv1 4))))) +(check-sat) -- 2.30.2