More robust treatment of flattening in arith rewriter (#8695)

Currently can allow rewritten forms to be rewritable.

Fixes #8692. Fixes #8693. Fixes #8697.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index be0a3573670f70ea414c311534db92cf0d4a1a05..8920c51aa10c4a769dbaf903d09ca88314f48fe9 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -433,12 +433,12 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t)
   Assert(t.getNumChildren() > 1);
 
   std::vector<TNode> children;
-  expr::algorithm::flatten(t, children);
+  expr::algorithm::flatten(t, children, Kind::ADD, Kind::TO_REAL);
 
   rewriter::Sum sum;
   for (const auto& child : children)
   {
-    rewriter::addToSum(sum, removeToReal(child));
+    rewriter::addToSum(sum, child);
   }
   Node retSum = rewriter::collectSum(sum);
   retSum = maybeEnsureReal(t.getType(), retSum);
@@ -462,19 +462,13 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   Assert(t.getNumChildren() >= 2);
 
   std::vector<TNode> children;
-  expr::algorithm::flatten(t, children, Kind::MULT, Kind::NONLINEAR_MULT);
+  expr::algorithm::flatten(t, children, Kind::MULT, Kind::NONLINEAR_MULT, Kind::TO_REAL);
 
   if (auto res = rewriter::getZeroChild(children); res)
   {
     return RewriteResponse(REWRITE_DONE, maybeEnsureReal(t.getType(), *res));
   }
 
-  // remove TO_REAL
-  for (TNode& tc : children)
-  {
-    tc = removeToReal(tc);
-  }
-
   Node ret;
   // Distribute over addition
   if (std::any_of(children.begin(), children.end(), [](TNode child) {

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 183c90049cc38c1686f508095a9997d984f5b457..0c8b54bb28189c72749eff7e14bea65ad5978b7c 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -811,6 +811,7 @@ set(regress_0_tests
   regress0/nl/issue8638-cov-resultants.smt2
   regress0/nl/issue8691-msum-subtypes.smt2
   regress0/nl/issue8691-3-msum-subtypes.smt2
+  regress0/nl/issue8692-idem-flatten.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
@@ -2915,6 +2916,7 @@ set(regress_2_tests
   regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
+  regress2/nl/issue8693-flatten-to-real.smt2
   regress2/nl/ufnia-factor-open-proof.smt2
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2

diff --git a/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2 b/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
new file mode 100644 (file)
index 0000000..9fea587
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (= 0 (* b (/ a (- 1)))))
+(check-sat)

diff --git a/test/regress/cli/regress2/nl/issue8693-flatten-to-real.smt2 b/test/regress/cli/regress2/nl/issue8693-flatten-to-real.smt2
new file mode 100644 (file)
index 0000000..ff9bb2a
--- /dev/null
+++ b/test/regress/cli/regress2/nl/issue8693-flatten-to-real.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(declare-fun a () Int)
+(declare-fun f () Int)
+(declare-fun e () Int)
+(assert (>= 1 b))
+(assert (< f 0))
+(assert (> e 0 (/ 1 d)))
+(assert (> (- d (* a c)) 0))
+(assert (< (+ d (* b f c)) 0))
+(assert (> (/ (* b c) (- 0 1 (/ 1 e))) 0))
+(check-sat)