(new theory) Update TheoryFP to the new interface (#4953)

This updates the theory of floating points to the new interface (see #4929).

Notice that TheoryFP was not adding trigger terms to its equality engine (which should be done during notifySharedTerm), and thus was not propagating equalities between shared terms in combined theories. This PR updates its notifySharedTerm method to the default one.

FYI @martin-cs

1 files changed, 26 insertions, 6 deletions

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 79ece7bce..2ef3b3f35 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -58,15 +58,28 @@ class TheoryFp : public Theory {
   TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode node) override;
-  void notifySharedTerm(TNode node) override;
 
   TrustNode ppRewrite(TNode node) override;
 
-  void check(Effort) override;
-
+  //--------------------------------- standard check
+  /** Do we need a check call at last call effort? */
   bool needsCheckLastEffort() override { return true; }
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  /** Pre-notify fact, return true if processed. */
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+  //--------------------------------- end standard check
+
   Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m) override;
+  /** Collect model values in m based on the relevant terms given by
+   * relevantTerms */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& relevantTerms) override;
 
   std::string identify() const override { return "THEORY_FP"; }
 
@@ -108,10 +121,17 @@ class TheoryFp : public Theory {
 
   /** Interaction with the rest of the solver **/
   void handleLemma(Node node);
-  bool handlePropagation(TNode node);
-  void handleConflict(TNode node);
+  /**
+   * Called when literal node is inferred by the equality engine. This
+   * propagates node on the output channel.
+   */
+  bool propagateLit(TNode node);
+  /**
+   * Called when two constants t1 and t2 merge in the equality engine. This
+   * sends a conflict on the output channel.
+   */
+  void conflictEqConstantMerge(TNode t1, TNode t2);
 
-  context::CDO<bool> d_conflict;
   context::CDO<Node> d_conflictNode;
 
   typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>