From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 5 Nov 2021 19:18:02 +0000 (-0700)
Subject: [FP] Do not assert that model has shared term (#7585)
X-Git-Tag: cvc5-1.0.0~879
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e187b4c5709fc7b15e3d4c0e751224824208d28b;p=cvc5.git

[FP] Do not assert that model has shared term (#7585)

Fixes #7569. Currently, the FP solver asserts that
m->hasTerm(sharedTerm) is always true for the real term in the
conversion from real to floating-point value. This is not necessarily
the case because the arithmetic solver computes values for the variables
in the shared terms but not necessarily for the terms themselves. This
commit removes the assertion and instead relies on the fact that a later
assertion checks that m->getValue(sharedTerm).isConst(), which is the
property that we are actually interested in.
---

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index e588bc1a9..6f2ddbf63 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -289,9 +289,13 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
   else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
   {
     // Get the values
-    Assert(m->hasTerm(abstract));
-    Assert(m->hasTerm(concrete[0]));
-    Assert(m->hasTerm(concrete[1]));
+    Assert(m->hasTerm(abstract)) << "Term " << abstract << " not in model";
+    Assert(m->hasTerm(concrete[0]))
+        << "Term " << concrete[0] << " not in model";
+    // Note: while the value for concrete[1] that we get from the model has to
+    // be const, it is not necessarily the case that `m->hasTerm(concrete[1])`.
+    // The arithmetic solver computes values for the variables in shared terms
+    // but does not necessarily add the shared terms themselves.
 
     Node abstractValue = m->getValue(abstract);
     Node rmValue = m->getValue(concrete[0]);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 25f61c27c..f322ffafc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -613,6 +613,7 @@ set(regress_0_tests
   regress0/fp/issue5734.smt2
   regress0/fp/issue6164.smt2
   regress0/fp/issue7002.smt2
+  regress0/fp/issue7569.smt2
   regress0/fp/proj-issue329-prereg-context.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
diff --git a/test/regress/regress0/fp/issue7569.smt2 b/test/regress/regress0/fp/issue7569.smt2
new file mode 100644
index 000000000..c4bffc3da
--- /dev/null
+++ b/test/regress/regress0/fp/issue7569.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_ALL)
+(declare-const X (_ FloatingPoint 8 24))
+(declare-const R Real)
+(assert (= X ((_ to_fp 8 24) RTZ (- R))))
+(assert (= X ((_ to_fp 8 24) RTZ 0)))
+(set-info :status sat)
+(check-sat)