From: Gereon Kremer <gkremer@stanford.edu>
Date: Thu, 3 Feb 2022 23:14:38 +0000 (-0800)
Subject: Improve theory combination over real algebraic models (#8045)
X-Git-Tag: cvc5-1.0.0~456
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=72bf82dade6b72cea4cb8bf86d03a7f6b875b3a9;p=cvc5.git

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 d9fe7db47..155a6cdce 100644
--- 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 67603be82..3bdecf556 100644
--- 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
index 000000000..c126e5b29
--- /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
index 000000000..0cd8f2645
--- /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)