Improve theory combination over real algebraic models (#8045)

Though we support real algebraic models now for theory combination, cvc5/cvc5-projects#451 uncovered the possibility to assert if an equality was in fact not equal during theory combination and the difference was real algebraic.
This PR fixes this issue by adding the proper check.
Fixes cvc5/cvc5-projects#451.

diff --git a/src/theory/arith/arith_evaluator.cpp b/src/theory/arith/arith_evaluator.cpp
index d9fe7db470ba9c935473d87976eede430d6c9087..155a6cdce1cfbf167355197cf606d1268cb92201 100644 (file)
--- a/src/theory/arith/arith_evaluator.cpp
+++ b/src/theory/arith/arith_evaluator.cpp
@@ -37,7 +37,10 @@ std::optional<bool> isExpressionZero(Env& env,
   {
     return expr.getConst<Rational>().isZero();
   }
-  Assert(expr.getKind() != Kind::REAL_ALGEBRAIC_NUMBER);
+  if (expr.getKind() == Kind::REAL_ALGEBRAIC_NUMBER)
+  {
+    return isZero(expr.getOperator().getConst<RealAlgebraicNumber>());
+  }
   return std::nullopt;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 67603be826577032bf3f19fcac8b47b2e8411c8a..3bdecf5561b2d3b2d51f1c7bec898cab1a10a011 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -780,6 +780,8 @@ set(regress_0_tests
   regress0/nl/pow2-pow-isabelle.smt2
   regress0/nl/proj-issue-348.smt2
   regress0/nl/proj-issue-444-memout-eqelim.smt2
+  regress0/nl/proj-issue-451-ran-combination-1.smt2
+  regress0/nl/proj-issue-451-ran-combination-2.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
   regress0/nl/sin-cos-346-b-chunk-0169.smt2

diff --git a/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 b/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2
new file mode 100644 (file)
index 0000000..c126e5b
--- /dev/null
+++ b/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-option :global-declarations true)
+(set-logic QF_NRA)
+(set-option :produce-unsat-cores true)
+(declare-const _x0 Real)
+(check-sat-assuming ( (>= (/ _x0 _x0) (/ (/ 2079598914 691107) _x0)) (and (> (/ (/ (/ 2079598914 691107) _x0) _x0) _x0) (> (- _x0) _x0))))

diff --git a/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 b/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2
new file mode 100644 (file)
index 0000000..0cd8f26
--- /dev/null
+++ b/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-const x6 Real)
+(set-option :produce-unsat-cores true)
+(declare-const x Real)
+(assert (= x6 (/ x x)))
+(assert (> (- x) 0.0))
+(assert (> (/ 2 x x) x))
+(check-sat)