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 /src/theory/fp | |
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.
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 10 |
1 files changed, 7 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]); |