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 b38e2af30081640a8a10e550bfb94a26d2503ae8..8f302502e678b6132d023a93e3438e5c5e01a1b2 100644 (file)
--- 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 86fcbac906add60b3908b7e06461137f37a21ab7..9910f31152aa11969522c9f0c277dce681d81ca4 100644 (file)
--- 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 (file)
index 0000000..f413737
--- /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)