diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-08 19:59:51 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 19:59:51 -0600 |
| commit | 6444abbbcf5f298045c32ce3d69033b8f93a41d8 (patch) | |
| tree | 225299c73758c80330f63e2300c1e1207a0c4ed2 /src/theory/fp | |
| parent | d4b2f061182734c8c8efdea38e7afeaca7122fad (diff) | |
Do not check FP at last call if not necessary (#5627)
This makes the theory of floating points not request a last call effort check, if that call is known to do nothing.
This should make CVC4 (more) agnostic to whether --symfpu is enabled during configuration.
Diffstat (limited to 'src/theory/fp')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 8 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.h | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ce423a7fe..0a8c4ee0e 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -951,6 +951,14 @@ void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2) return; } + +bool TheoryFp::needsCheckLastEffort() +{ + // only need to check if we have added to the abstraction map, otherwise + // postCheck below is a no-op. + return !d_abstractionMap.empty(); +} + void TheoryFp::postCheck(Effort level) { // Resolve the abstractions for the conversion lemmas diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 341955cff..1a745b3a3 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -66,7 +66,7 @@ class TheoryFp : public Theory //--------------------------------- standard check /** Do we need a check call at last call effort? */ - bool needsCheckLastEffort() override { return true; } + bool needsCheckLastEffort() override; /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Effort level) override; /** Pre-notify fact, return true if processed. */ |