From cedb607a0017bff88f6d0be3d7295e87843c1662 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 2 May 2022 17:32:39 -0500
Subject: [PATCH] More robust treatment of flattening in arith rewriter (#8695)

Currently can allow rewritten forms to be rewritable.

Fixes #8692. Fixes #8693. Fixes #8697.
---
 src/theory/arith/arith_rewriter.cpp               | 12 +++---------
 test/regress/cli/CMakeLists.txt                   |  2 ++
 .../cli/regress0/nl/issue8692-idem-flatten.smt2   |  6 ++++++
 .../regress2/nl/issue8693-flatten-to-real.smt2    | 15 +++++++++++++++
 4 files changed, 26 insertions(+), 9 deletions(-)
 create mode 100644 test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2
 create mode 100644 test/regress/cli/regress2/nl/issue8693-flatten-to-real.smt2

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index be0a35736..8920c51aa 100644
--- 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 183c90049..0c8b54bb2 100644
--- 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
index 000000000..9fea58744
--- /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
index 000000000..ff9bb2a3d
--- /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)
-- 
2.30.2