diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-05 12:18:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-05 19:18:02 +0000 |
| commit | e187b4c5709fc7b15e3d4c0e751224824208d28b (patch) | |
| tree | 0ec51d926687736c338f73da8e8ca6d910776df9 | |
| parent | 51c3b3d6bb992550476220dd44a57a3e7987dce0 (diff) | |
[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.
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 10 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/issue7569.smt2 | 7 |
3 files changed, 15 insertions, 3 deletions
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) |