From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 7 Mar 2022 15:31:07 +0000 (+0100)
Subject: Try harder to show that a RAN is rational (#8230)
X-Git-Tag: cvc5-1.0.0~312
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=879f73516b9c0e0fe820adcdc3460cbb9c772062;p=cvc5.git

Try harder to show that a RAN is rational (#8230)

We try to rewrite real algebraic numbers to rationals. This is important to, e.g., allow the linear solver to see rational constants at all. Refining real algebraic numbers is done lazily, and (almost) any operation may trigger a refinement that makes libpoly realize it actually is rational. Thus, even the mere act of creating a node out of a real algebraic number may do this (it hashes it).
This PR thus introduces a fixed-point loop into the RAN node constructor that defends against this case.
Fixes #8226.
---

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 95fbf3c0f..e07b84273 100644
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1319,8 +1319,22 @@ Node NodeManager::mkRealAlgebraicNumber(const RealAlgebraicNumber& ran)
   {
     return mkConstReal(ran.toRational());
   }
-  return mkNode(Kind::REAL_ALGEBRAIC_NUMBER,
-                mkConst(Kind::REAL_ALGEBRAIC_NUMBER_OP, ran));
+  // Creating this node may refine the ran to the point where isRational returns
+  // true
+  Node inner = mkConst(Kind::REAL_ALGEBRAIC_NUMBER_OP, ran);
+
+  // Keep doing this until it either is rational or we have a fixed point.
+  while (true)
+  {
+    const RealAlgebraicNumber& cur = inner.getConst<RealAlgebraicNumber>();
+    if (cur.isRational())
+    {
+      return mkConstReal(cur.toRational());
+    }
+    if (cur == ran) break;
+    inner = mkConst(Kind::REAL_ALGEBRAIC_NUMBER_OP, cur);
+  }
+  return mkNode(Kind::REAL_ALGEBRAIC_NUMBER, inner);
 }
 
 }  // namespace cvc5
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2ce23a3ba..f659c200f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -785,6 +785,7 @@ set(regress_0_tests
   regress0/nl/issue6619-ran-model.smt2
   regress0/nl/issue8135-icp-candidates.smt2
   regress0/nl/issue8161-var-elim.smt2
+  regress0/nl/issue8226-ran-refinement.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/regress0/nl/issue8226-ran-refinement.smt2 b/test/regress/regress0/nl/issue8226-ran-refinement.smt2
new file mode 100644
index 000000000..8ce6f1273
--- /dev/null
+++ b/test/regress/regress0/nl/issue8226-ran-refinement.smt2
@@ -0,0 +1,10 @@
+;; needs --check-models, as --debug-check-models does not trigger the issue
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun r1 () Real)
+(declare-fun r2 () Real)
+(declare-fun r10 () Real)
+(assert (= r1 (- 0.0 (- 1 r1) (* r2 r2 0.059 (- 1.0)))))
+(assert (< 1.0 (+ 34 (- r1) (- 1.0 (- r1) (* r10 r2 r2)))))
+(check-sat)