From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Tue, 5 Apr 2022 04:32:43 +0000 (-0700)
Subject: Make rewriter more robust against RAN becoming rational (#8564)
X-Git-Tag: cvc5-1.0.0~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5495cc021e6e7a52c6e94d8be6a471168a91c691;p=cvc5.git

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.
---

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)