From 002955063ecf1b4b190717a7a0b2aec79ac7b6d9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Dec 2020 14:04:27 -0600 Subject: [PATCH] Remove bv divide by zero option (#5672) This is required to avoid failures in the planned refactoring of check-models. This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem. It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM. FYI @barrettcw --- src/options/bv_options.toml | 8 ------ src/smt/set_defaults.cpp | 26 ------------------- src/theory/bv/theory_bv.cpp | 24 ++++------------- ...ry_bv_rewrite_rules_operator_elimination.h | 24 +++-------------- .../theory_bv_rewrite_rules_simplification.h | 3 +-- src/theory/bv/theory_bv_rewriter.cpp | 12 ++------- test/regress/regress0/bv/divtest_2_5.smt2 | 5 ++-- .../regress0/bv/pr4993-bvugt-bvurem-a.smt2 | 2 +- .../regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 6 ++--- .../regress/regress1/ho/issue4065-no-rep.smt2 | 5 +--- .../qbv-test-invert-bvudiv-1-neq.smt2 | 2 +- .../quantifiers/qbv-test-invert-bvudiv-1.smt2 | 2 +- 12 files changed, 21 insertions(+), 98 deletions(-) diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index a7f8d439f..6a0ca913b 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -129,14 +129,6 @@ header = "options/bv_options.h" default = "true" help = "lift equivalence with one-bit bit-vectors to be boolean operations" -[[option]] - name = "bitvectorDivByZeroConst" - category = "regular" - long = "bv-div-zero-const" - type = "bool" - default = "true" - help = "always return -1 on (bvudiv s 0) and s on (bvurem s 0)" - [[option]] name = "bvExtractArithRewrite" category = "expert" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index ca5a2773b..c8aecf288 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -82,15 +82,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::bitvectorAlgebraicSolver.set(true); } - // Language-based defaults - if (!options::bitvectorDivByZeroConst.wasSetByUser()) - { - // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we - // set this option if the input format is SMT LIB 2.6. We also set this - // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus. - options::bitvectorDivByZeroConst.set( - !language::isInputLang_smt2_5(options::inputLanguage(), true)); - } bool is_sygus = language::isInputLangSygus(options::inputLanguage()); if (options::bitblastMode() == options::BitblastMode::EAGER) @@ -569,10 +560,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // eliminated altogether (or otherwise fail at preprocessing). || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() && options::solveIntAsBV() == 0) - // If division/mod-by-zero is not treated as a constant value in BV, we - // need UF. - || (logic.isTheoryEnabled(THEORY_BV) - && !options::bitvectorDivByZeroConst()) // FP requires UF since there are multiple operators that are partially // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more // details). @@ -1065,19 +1052,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE); } } - // do not allow partial functions - if (!options::bitvectorDivByZeroConst()) - { - if (options::bitvectorDivByZeroConst.wasSetByUser()) - { - throw OptionException( - "--no-bv-div-zero-const is not supported with SyGuS"); - } - Notice() - << "SmtEngine: setting bv-div-zero-const to true to support SyGuS" - << std::endl; - options::bitvectorDivByZeroConst.set(true); - } if (!options::dtRewriteErrorSel.wasSetByUser()) { options::dtRewriteErrorSel.set(true); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fd91d0346..6f22d4520 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -131,25 +131,11 @@ TrustNode TheoryBV::expandDefinition(Node node) NodeManager* nm = NodeManager::currentNM(); unsigned width = node.getType().getBitVectorSize(); - if (options::bitvectorDivByZeroConst()) - { - Kind kind = node.getKind() == kind::BITVECTOR_UDIV - ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UREM_TOTAL; - ret = nm->mkNode(kind, node[0], node[1]); - break; - } - - TNode num = node[0], den = node[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width)); - Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV - ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UREM_TOTAL, - num, - den); - Node divByZero = getUFDivByZero(node.getKind(), width); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); - ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + Kind kind = node.getKind() == kind::BITVECTOR_UDIV + ? kind::BITVECTOR_UDIV_TOTAL + : kind::BITVECTOR_UREM_TOTAL; + ret = nm->mkNode(kind, node[0], node[1]); + break; } break; diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 1e48be1da..2fff03c10 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -464,11 +464,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = - nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UDIV, - abs_a, - abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -506,11 +502,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = - nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UDIV, - abs_a, - abs_b); + Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b); @@ -544,11 +536,7 @@ inline Node RewriteRule::apply(TNode node) Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = - nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL - : kind::BITVECTOR_UREM, - abs_a, - abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); @@ -583,11 +571,7 @@ inline Node RewriteRule::apply(TNode node) nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = - nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL - : kind::BITVECTOR_UREM, - abs_a, - abs_b); + Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b); Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 20dac35cd..ca26577bf 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1589,8 +1589,7 @@ Node RewriteRule::apply(TNode node) { template <> inline bool RewriteRule::applies(TNode node) { - return (options::bitvectorDivByZeroConst() - && node.getKind() == kind::BITVECTOR_UGT + return (node.getKind() == kind::BITVECTOR_UGT && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL && node[0][1] == node[1]); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 4f84facca..b883ab537 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -440,21 +440,13 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ Node resultNode = node; - if(node[1].isConst() && node[1].getConst().getValue() != 0) { - return RewriteUdivTotal(node, prerewrite); - } - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteUdivTotal(node, prerewrite); } RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){ Node resultNode = node; - if(node[1].isConst() && node[1].getConst().getValue() != 0) { - return RewriteUremTotal(node, prerewrite); - } - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteUremTotal(node, prerewrite); } RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ diff --git a/test/regress/regress0/bv/divtest_2_5.smt2 b/test/regress/regress0/bv/divtest_2_5.smt2 index b2712e520..f45520044 100644 --- a/test/regress/regress0/bv/divtest_2_5.smt2 +++ b/test/regress/regress0/bv/divtest_2_5.smt2 @@ -1,7 +1,6 @@ -; EXPECT: sat -(set-info :smt-lib-version 2.5) +; EXPECT: unsat (set-logic QF_BV) -(set-info :status sat) +(set-info :status unsat) (declare-fun x () (_ BitVec 8)) (declare-fun y () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 index c6748b19e..b53f6f0cc 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-div-zero-const --no-check-unsat-cores +; COMMAND-LINE: --no-check-unsat-cores (set-logic QF_BV) (set-info :status unsat) (declare-const x (_ BitVec 4)) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 index 0888031d5..a514d8b09 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores -; COMMAND-LINE: --bv-solver=simple --no-bv-div-zero-const --no-check-unsat-cores +; COMMAND-LINE: --no-check-unsat-cores +; COMMAND-LINE: --bv-solver=simple --no-check-unsat-cores (set-logic QF_BV) -(set-info :status sat) +(set-info :status unsat) (declare-const x (_ BitVec 4)) (declare-const y (_ BitVec 4)) (assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false)))) diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 index 25662d6eb..9852150d9 100644 --- a/test/regress/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -1,8 +1,5 @@ -; COMMAND-LINE: -q -; EXPECT: sat (set-logic AUFBV) -(set-info :status sat) -(set-option :bv-div-zero-const false) +(set-info :status unsat) (set-option :fmf-bound-int true) (set-option :uf-ho true) (declare-fun _substvar_20_ () Bool) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 index 5c2c42202..153e7a46b 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: unsat (set-logic BV) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 index c7ef2d053..2935de44d 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q ; EXPECT: sat (set-logic BV) (set-info :status sat) -- 2.30.2