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 95fbf3c0fd372eef5d1a3e26d051a9ab4bc68fda..e07b842731ebde991d4812cc041c4ae125b2322a 100644 (file)
--- 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 2ce23a3bad562ba175fc690e36e691a46c757804..f659c200fcabdcf6b65368562bacf2b726d61c9d 100644 (file)
--- 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 (file)
index 0000000..8ce6f12
--- /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)