Remove extended rewrite for arithmetic (#5760)

This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.

Fixes #5737, fixes #5740.

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 6897287d660b0dde36778e25f1bf761a796d0e3d..37a3396e24a5f5ea49a5686429782c9c4f43f04f 100644 (file)
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -243,11 +243,7 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     }
     Trace("q-ext-rewrite-debug") << "theoryOf( " << ret << " )= " << tid
                                  << std::endl;
-    if (tid == THEORY_ARITH)
-    {
-      new_ret = extendedRewriteArith(ret);
-    }
-    else if (tid == THEORY_STRINGS)
+    if (tid == THEORY_STRINGS)
     {
       new_ret = extendedRewriteStrings(ret);
     }
@@ -1695,41 +1691,6 @@ bool ExtendedRewriter::inferSubstitution(Node n,
   return false;
 }
 
-Node ExtendedRewriter::extendedRewriteArith(Node ret)
-{
-  Kind k = ret.getKind();
-  NodeManager* nm = NodeManager::currentNM();
-  Node new_ret;
-  if (k == DIVISION || k == INTS_DIVISION || k == INTS_MODULUS)
-  {
-    // rewrite as though total
-    std::vector<Node> children;
-    bool all_const = true;
-    for (unsigned i = 0, size = ret.getNumChildren(); i < size; i++)
-    {
-      if (ret[i].isConst())
-      {
-        children.push_back(ret[i]);
-      }
-      else
-      {
-        all_const = false;
-        break;
-      }
-    }
-    if (all_const)
-    {
-      Kind new_k = (ret.getKind() == DIVISION ? DIVISION_TOTAL
-                                              : (ret.getKind() == INTS_DIVISION
-                                                     ? INTS_DIVISION_TOTAL
-                                                     : INTS_MODULUS_TOTAL));
-      new_ret = nm->mkNode(new_k, children);
-      debugExtendedRewrite(ret, new_ret, "total-interpretation");
-    }
-  }
-  return new_ret;
-}
-
 Node ExtendedRewriter::extendedRewriteStrings(Node ret)
 {
   Node new_ret;

diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 8b5f74a2fc258310d03c01ddaa8bb9850d6cfc5c..e5e95b3f67d3fc9e0ccefbe93d69a9070597d874 100644 (file)
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -239,12 +239,6 @@ class ExtendedRewriter
   //--------------------------------------end generic utilities
 
   //--------------------------------------theory-specific top-level calls
-  /** extended rewrite arith
-   *
-   * If this method returns a non-null node ret', then ret is equivalent to
-   * ret'.
-   */
-  Node extendedRewriteArith(Node ret);
   /** extended rewrite strings
    *
    * If this method returns a non-null node ret', then ret is equivalent to

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7ceb3b4b2f82871e0ac946dc1487bcb8f3c5425b..dd6956b0900665afe62d0da3494215c7acbbbdfd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -686,6 +686,9 @@ set(regress_0_tests
   regress0/nl/issue5534-no-assertions.smt2
   regress0/nl/issue5726-downpolys.smt2
   regress0/nl/issue5726-sqfactor.smt2
+  regress0/nl/issue5737-div00.smt2
+  regress0/nl/issue5740-mod00.smt2
+  regress0/nl/issue5740-2-mod00.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2

diff --git a/test/regress/regress0/nl/issue5737-div00.smt2 b/test/regress/regress0/nl/issue5737-div00.smt2
new file mode 100644 (file)
index 0000000..59de5a3
--- /dev/null
+++ b/test/regress/regress0/nl/issue5737-div00.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --ext-rew-prep -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (> (div 0 0) 0))
+(check-sat)

diff --git a/test/regress/regress0/nl/issue5740-2-mod00.smt2 b/test/regress/regress0/nl/issue5740-2-mod00.smt2
new file mode 100644 (file)
index 0000000..01930da
--- /dev/null
+++ b/test/regress/regress0/nl/issue5740-2-mod00.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ext-rewrite-quant --sygus-inst --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun c (Int) Bool)
+(define-fun d ((e Int)) Bool (forall ((a Int) (b Int)) (! true :pattern ((c a) (c b)))))
+(assert (exists ((e Int)) (distinct (d e) (= (ite (= e 0) (mod 0 e) 0) 0))))
+(check-sat)

diff --git a/test/regress/regress0/nl/issue5740-mod00.smt2 b/test/regress/regress0/nl/issue5740-mod00.smt2
new file mode 100644 (file)
index 0000000..e1287da
--- /dev/null
+++ b/test/regress/regress0/nl/issue5740-mod00.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --ext-rewrite-quant -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(define-fun f ((a Int) (b Int)) Int (ite (= b 0) 0 a))
+(assert (exists ((c Int)) (distinct (f c (mod 0 0)) 0)))
+(check-sat)