From e187b4c5709fc7b15e3d4c0e751224824208d28b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 5 Nov 2021 12:18:02 -0700 Subject: [PATCH] [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. --- src/theory/fp/theory_fp.cpp | 10 +++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/issue7569.smt2 | 7 +++++++ 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/fp/issue7569.smt2 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) -- 2.30.2