From 5495cc021e6e7a52c6e94d8be6a471168a91c691 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Mon, 4 Apr 2022 21:32:43 -0700
Subject: [PATCH] Make rewriter more robust against RAN becoming rational
 (#8564)

We use real algebraic number to represent multiplicities of sum terms within the arithmetic rewriter. Unfortunately, such real algebraic numbers can realize that they are in fact rational at awkward times. This makes isRational() unsuitable for checking this, instead we should construct the node and check afterwards.
---
 src/theory/arith/rewriter/node_utils.cpp           | 14 ++++++++------
 test/regress/cli/CMakeLists.txt                    |  1 +
 .../cli/regress0/arith/arith-rewrite-with-ran.smt2 | 14 ++++++++++++++
 3 files changed, 23 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/cli/regress0/arith/arith-rewrite-with-ran.smt2

diff --git a/src/theory/arith/rewriter/node_utils.cpp b/src/theory/arith/rewriter/node_utils.cpp
index b38e2af30..8f302502e 100644
--- a/src/theory/arith/rewriter/node_utils.cpp
+++ b/src/theory/arith/rewriter/node_utils.cpp
@@ -39,16 +39,17 @@ Node mkMultTerm(const Rational& multiplicity, TNode monomial)
 
 Node mkMultTerm(const RealAlgebraicNumber& multiplicity, TNode monomial)
 {
-  if (multiplicity.isRational())
+  Node mterm = mkConst(multiplicity);
+  if (mterm.isConst())
   {
-    return mkMultTerm(multiplicity.toRational(), monomial);
+    return mkMultTerm(mterm.getConst<Rational>(), monomial);
   }
   if (monomial.isConst())
   {
     return mkConst(multiplicity * monomial.getConst<Rational>());
   }
   std::vector<Node> prod;
-  prod.emplace_back(mkConst(multiplicity));
+  prod.emplace_back(mterm);
   if (monomial.getKind() == Kind::MULT || monomial.getKind() == Kind::NONLINEAR_MULT)
   {
     prod.insert(prod.end(), monomial.begin(), monomial.end());
@@ -68,12 +69,13 @@ Node mkMultTerm(const RealAlgebraicNumber& multiplicity,
   {
     return mkConst(multiplicity);
   }
-  if (multiplicity.isRational())
+  Node mterm = mkConst(multiplicity);
+  if (mterm.isConst())
   {
     std::sort(monomial.begin(), monomial.end(), rewriter::LeafNodeComparator());
-    return mkMultTerm(multiplicity.toRational(), mkNonlinearMult(monomial));
+    return mkMultTerm(mterm.getConst<Rational>(), mkNonlinearMult(monomial));
   }
-  monomial.emplace_back(mkConst(multiplicity));
+  monomial.emplace_back(mterm);
   std::sort(monomial.begin(), monomial.end(), rewriter::LeafNodeComparator());
   Assert(monomial.size() >= 2);
   return NodeManager::currentNM()->mkNode(Kind::NONLINEAR_MULT, monomial);
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 86fcbac90..9910f3115 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -26,6 +26,7 @@ set(regress_0_tests
   regress0/arith/arith.01.cvc.smt2
   regress0/arith/arith.02.cvc.smt2
   regress0/arith/arith.03.cvc.smt2
+  regress0/arith/arith-rewrite-with-ran.smt2
   regress0/arith/bug443.delta01.smtv1.smt2
   regress0/arith/bug547.2.smt2
   regress0/arith/bug549.cvc.smt2
diff --git a/test/regress/cli/regress0/arith/arith-rewrite-with-ran.smt2 b/test/regress/cli/regress0/arith/arith-rewrite-with-ran.smt2
new file mode 100644
index 000000000..f413737cc
--- /dev/null
+++ b/test/regress/cli/regress0/arith/arith-rewrite-with-ran.smt2
@@ -0,0 +1,14 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-const x Bool)
+(declare-const y Real)
+(declare-fun b () Real)
+(declare-fun a () Bool)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun e () Real)
+(declare-fun f () Real)
+(declare-fun g () Real)
+(assert (and (not a) (or x (= 1 e)) (or x (= 0.0 g)) (= 0.0 (+ b y d)) (or a (= 0.0 (+ c y))) (= 0.0 (+ 1.0 f y)) (= 0.0 (+ 1.0 b (* 49.0 f))) (= 0.0 (+ e (* g y) (* f f (- 49.0))))))
+(check-sat)
-- 
2.30.2