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

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index a7f8d439f2bc107eecfa80bc5cf8728c3562b4f2..6a0ca913b8381d07e54191c7797e7038e0b7c123 100644 (file)
--- 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 ca5a2773b5781023e6ccdd65c7217f024e884ab7..c8aecf288765cdafc69fe5747c4937554252c392 100644 (file)
--- 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 fd91d034625978f0348f966b46358db0f633671d..6f22d452052de0445d6c732d3f4db1805eb5ebe2 100644 (file)
--- 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 1e48be1da28d1091b5e521dc6a974b9095ca4953..2fff03c104fead323a44e48be977bdb7a4c90894 100644 (file)
--- 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<SdivEliminate>::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<SdivEliminateFewerBitwiseOps>::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<SremEliminate>::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<SremEliminateFewerBitwiseOps>::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 20dac35cd9d3450ead505d6c2348be8b2a6459ff..ca26577bf1d8618b2aeb101c3ea4f25c00bea661 100644 (file)
--- 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<ShiftZero>::apply(TNode node) {
 template <>
 inline bool RewriteRule<UgtUrem>::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 4f84facca06b9346c6def99a79d59ad44b6bc1fd..b883ab537438565aeb3408892cade426ca286ad8 100644 (file)
--- 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<BitVector>().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<BitVector>().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 b2712e520db5675d2b69a8d2cc32c5e34b02144e..f4552004483df937d39deac699a4ab14e6a6b162 100644 (file)
--- 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 c6748b19e3f5444952a54e4c29972eb1ee196a37..b53f6f0cceb4d4b2ee5770c2d53c0b7c598e99e2 100644 (file)
--- 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 0888031d5a6d5df95d63f806266cbc18ebda2802..a514d8b0927b76788cb32ad38e02748d8abc538c 100644 (file)
--- 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 25662d6eb7b4de5fc8efa6ac83bb3ef877f870a3..9852150d9749acba7ff632e1fc0fe825fa5aa829 100644 (file)
--- 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 5c2c42202f0b91b5cddca25c18ce4d19d34b347b..153e7a46b8a85617ce8ca15fb136d127265a0b9c 100644 (file)
--- 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 c7ef2d053288dfa5bba108168916162de11ca477..2935de44d5874999106664c2938c4cbeb1a83a8c 100644 (file)
--- 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)