Clean up remaining raw uses of output channel (#6161)

After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.

This is work towards standardizing the statistics for theories.

2 files changed, 15 insertions, 26 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index d17e2999e..3099d9aab 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -114,7 +114,6 @@ TheoryFp::TheoryFp(context::Context* c,
       d_registeredTerms(u),
       d_conv(new FpConverter(u)),
       d_expansionRequested(false),
-      d_conflictNode(c, Node::null()),
       d_minMap(u),
       d_maxMap(u),
       d_toUBVMap(u),
@@ -123,10 +122,12 @@ TheoryFp::TheoryFp(context::Context* c,
       d_realToFloatMap(u),
       d_floatToRealMap(u),
       d_abstractionMap(u),
-      d_state(c, u, valuation)
+      d_state(c, u, valuation),
+      d_im(*this, d_state, pnm, "theory::fp", false)
 {
-  // indicate we are using the default theory state object
+  // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
+  d_inferManager = &d_im;
 } /* TheoryFp::TheoryFp() */
 
 TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
@@ -917,39 +918,25 @@ void TheoryFp::preRegisterTerm(TNode node)
   return;
 }
 
-void TheoryFp::handleLemma(Node node) {
+void TheoryFp::handleLemma(Node node, InferenceId id)
+{
   Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
   // will be preprocessed when sent, which is important because it contains
   // embedded ITEs
-  d_out->lemma(node);
+  d_im.lemma(node, id);
 }
 
 bool TheoryFp::propagateLit(TNode node)
 {
   Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl;
-
-  bool stat = d_out->propagate(node);
-
-  if (!stat)
-  {
-    d_state.notifyInConflict();
-  }
-  return stat;
+  return d_im.propagateLit(node);
 }
 
 void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2)
 {
-  std::vector<TNode> assumptions;
-  d_equalityEngine->explainEquality(t1, t2, true, assumptions);
-
-  Node conflict = helper::buildConjunct(assumptions);
-  Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected "
-              << conflict << std::endl;
-
-  d_conflictNode = conflict;
-  d_state.notifyInConflict();
-  d_out->conflict(conflict);
-  return;
+  Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected"
+              << std::endl;
+  d_im.conflictEqConstantMerge(t1, t2);
 }
 
 
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 1660d5799..b15b5c2dd 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -27,6 +27,7 @@
 #include "context/cdo.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_inference_manager.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
@@ -142,7 +143,7 @@ class TheoryFp : public Theory
   void convertAndEquateTerm(TNode node);
 
   /** Interaction with the rest of the solver **/
-  void handleLemma(Node node);
+  void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN);
   /**
    * Called when literal node is inferred by the equality engine. This
    * propagates node on the output channel.
@@ -168,7 +169,6 @@ class TheoryFp : public Theory
   Node abstractFloatToReal(Node);
 
  private:
-  context::CDO<Node> d_conflictNode;
 
   ComparisonUFMap d_minMap;
   ComparisonUFMap d_maxMap;
@@ -183,6 +183,8 @@ class TheoryFp : public Theory
   TheoryFpRewriter d_rewriter;
   /** A (default) theory state object */
   TheoryState d_state;
+  /** A (default) inference manager */
+  TheoryInferenceManager d_im;
 }; /* class TheoryFp */
 
 }  // namespace fp