From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Dec 2020 01:59:51 +0000 (-0600)
Subject: Do not check FP at last call if not necessary (#5627)
X-Git-Tag: cvc5-1.0.0~2473
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6444abbbcf5f298045c32ce3d69033b8f93a41d8;p=cvc5.git

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 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. */