From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 11 Jan 2021 14:48:01 +0000 (-0600)
Subject: Remove extended rewrite for arithmetic (#5760)
X-Git-Tag: cvc5-1.0.0~2387
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae82eb306143ade54a6f99b2aae0b62b8c77cd35;p=cvc5.git

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 6897287d6..37a3396e2 100644
--- 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 8b5f74a2f..e5e95b3f6 100644
--- 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 7ceb3b4b2..dd6956b09 100644
--- 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
index 000000000..59de5a3fb
--- /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
index 000000000..01930da6d
--- /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
index 000000000..e1287dacb
--- /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)