From 879f73516b9c0e0fe820adcdc3460cbb9c772062 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 7 Mar 2022 16:31:07 +0100 Subject: [PATCH] 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. --- src/expr/node_manager_template.cpp | 18 ++++++++++++++++-- test/regress/CMakeLists.txt | 1 + .../regress0/nl/issue8226-ran-refinement.smt2 | 10 ++++++++++ 3 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/nl/issue8226-ran-refinement.smt2 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(); + 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) -- 2.30.2