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.

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ce423a7feb2ac6fc600ac4e181600d1d46b1d784..0a8c4ee0eedcafa6f66f3ac2992e5878a99e8263 100644 (file)
--- 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 341955cffeecf3eaf1eea1f9ab5ab917baa036be..1a745b3a33e6b687fbac943decd6f5eb957730fe 100644 (file)
--- 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. */