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.

8 files changed, 71 insertions, 63 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 09e3a8370..820c317c5 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -74,9 +74,9 @@ class NlLemma;
  * which is called by TheoryArithPrivate either:
  * (1) at full effort with no conflicts or lemmas emitted, or
  * (2) at last call effort.
- * In this method, this class calls d_out->lemma(...)
+ * In this method, this class calls d_im.lemma(...)
  * for valid arithmetic theory lemmas, based on the current set of assertions,
- * where d_out is the output channel of TheoryArith.
+ * where d_im is the inference manager of TheoryArith.
  */
 class NonlinearExtension
 {
@@ -94,8 +94,8 @@ class NonlinearExtension
   void preRegisterTerm(TNode n);
   /** Check at effort level e.
    *
-   * This call may result in (possibly multiple) calls to d_out->lemma(...)
-   * where d_out is the output channel of TheoryArith.
+   * This call may result in (possibly multiple) calls to d_im.lemma(...)
+   * where d_im is the inference manager of TheoryArith.
    *
    * If e is FULL, then we add lemmas based on context-depedent
    * simplification (see Reynolds et al FroCoS 2017).
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 53680530d..7f57d5942 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -327,7 +327,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     nb << test << test.notNode();
                     Node lemma = nb;
                     d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT);
-                    d_out->requirePhase( test, true );
+                    d_im.requirePhase(test, true);
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                     Node lemma = utils::mkSplit(n, dt);
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
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index e53ba35f8..c786117f3 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -174,6 +174,17 @@ const char* toString(InferenceId i)
 
     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
+    case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
+    case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
+    case InferenceId::SEP_EMP: return "SEP_EMP";
+    case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
+    case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
+    case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";
+    case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP";
+    case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK";
+    case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA";
+    case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF";
+    case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND";
 
     case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
     case InferenceId::SETS_DEQ: return "SETS_DEQ";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 4af7761a0..380b5eca6 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -294,6 +294,29 @@ enum class InferenceId
   SEP_PTO_NEG_PROP,
   // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
   SEP_PTO_PROP,
+  // introduces a label for a heap, of the form U => L, where U is an
+  // unlabelled separation logic predicate and L is its labelled form
+  SEP_LABEL_INTRO,
+  // introduces the set constraints for a label
+  SEP_LABEL_DEF,
+  // lemma for sep.emp
+  SEP_EMP,
+  // positive reduction for sep constraint
+  SEP_POS_REDUCTION,
+  // negative reduction for sep constraint
+  SEP_NEG_REDUCTION,
+  // model-based refinement for negated star/wand
+  SEP_REFINEMENT,
+  // sep.nil is not in the heap
+  SEP_NIL_NOT_IN_HEAP,
+  // a symmetry breaking lemma
+  SEP_SYM_BREAK,
+  // finite witness data lemma
+  SEP_WITNESS_FINITE_DATA,
+  // element distinctness lemma
+  SEP_DISTINCT_REF,
+  // reference bound lemma
+  SEP_REF_BOUND,
   // ---------------------------------- end sep theory
 
   // ---------------------------------- sets theory
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 47eac5359..52e89159b 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -128,19 +128,7 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
 
 bool TheorySep::propagateLit(TNode literal)
 {
-  Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl;
-  // If already in conflict, no more propagation
-  if (d_state.isInConflict())
-  {
-    Debug("sep") << "TheorySep::propagateLit(" << literal
-                 << "): already in conflict" << std::endl;
-    return false;
-  }
-  bool ok = d_out->propagate(literal);
-  if (!ok) {
-    d_state.notifyInConflict();
-  }
-  return ok;
+  return d_im.propagateLit(literal);
 }
 
 TrustNode TheorySep::explain(TNode literal)
@@ -345,7 +333,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     }
     Trace("sep-lemma-debug")
         << "Sep::Lemma : base reduction : " << lem << std::endl;
-    d_out->lemma(lem);
+    d_im.lemma(lem, InferenceId::SEP_LABEL_INTRO);
     return;
   }
   Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl;
@@ -414,13 +402,13 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
         Trace("sep-lemma")
             << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem
             << std::endl;
-        d_out->lemma(nrlem);
+        d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP);
       }
       // send out definitional lemmas for introduced sets
       for (const Node& clem : c_lems)
       {
         Trace("sep-lemma") << "Sep::Lemma : definition : " << clem << std::endl;
-        d_out->lemma(clem);
+        d_im.lemma(clem, InferenceId::SEP_LABEL_DEF);
       }
       conc = nm->mkNode(AND, children);
     }
@@ -454,7 +442,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
         lem = nm->mkNode(OR, fact.negate(), econc);
       }
       Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
-      d_out->lemma(lem);
+      d_im.lemma(lem, InferenceId::SEP_EMP);
     }
     else
     {
@@ -492,14 +480,14 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     // Node lem = nm->mkNode( EQUAL, lit, conc );
     Node lem = nm->mkNode(OR, lit.negate(), conc);
     Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
-    d_out->lemma(lem);
+    d_im.lemma(lem, InferenceId::SEP_NEG_REDUCTION);
   }
   else
   {
     // reduce based on implication
     Node lem = nm->mkNode(OR, fact.negate(), conc);
     Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl;
-    d_out->lemma(lem);
+    d_im.lemma(lem, InferenceId::SEP_POS_REDUCTION);
   }
 }
 
@@ -799,7 +787,7 @@ void TheorySep::postCheck(Effort level)
                              << ") : " << lem << std::endl;
         Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : "
                            << lem << std::endl;
-        d_out->lemma(lem);
+        d_im.lemma(lem, InferenceId::SEP_REFINEMENT);
         addedLemma = true;
       }
       else
@@ -868,7 +856,7 @@ void TheorySep::postCheck(Effort level)
             nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, ll, dsk), d_true));
         Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem
                            << std::endl;
-        d_out->lemma(lem);
+        d_im.lemma(lem, InferenceId::SEP_WITNESS_FINITE_DATA);
         addedLemma = true;
       }
       else
@@ -906,7 +894,7 @@ void TheorySep::postCheck(Effort level)
 
   if (needAddLemma)
   {
-    d_out->setIncomplete();
+    d_im.setIncomplete();
   }
   Trace("sep-check") << "Sep::check(): " << level
                      << " done, conflict=" << d_state.isInConflict()
@@ -1219,7 +1207,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
         //ensure that it is distinct from all other references so far
         for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
           Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] );
-          d_out->lemma( eq.negate() );
+          d_im.lemma(eq.negate(), InferenceId::SEP_DISTINCT_REF);
         }
         d_type_references_all[tn].push_back( e );
       }
@@ -1237,11 +1225,8 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
 
       Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
       Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
-      d_out->lemma( slem );
-      //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
-      //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
-      //d_out->lemma( slem );
-      
+      d_im.lemma(slem, InferenceId::SEP_REF_BOUND);
+
       //symmetry breaking
       if( d_type_references_card[tn].size()>1 ){
         std::map< unsigned, Node > lit_mem_map;
@@ -1257,7 +1242,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
             Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children );
             sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem );
             Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl;
-            d_out->lemma( sym_lem );
+            d_im.lemma(sym_lem, InferenceId::SEP_SYM_BREAK);
           }
         }
       }
@@ -1267,8 +1252,8 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
     Node nr = getNilRef( tn );
     Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate();
     Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::endl;
-    d_out->lemma( nrlem );
-    
+    d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP);
+
     return n_lbl;
   }else{
     return it->second;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 32524b562..ac25ede14 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -181,7 +181,7 @@ bool TheoryUF::preNotifyFact(
       else
       {
         // support for cardinality constraints is not enabled, set incomplete
-        d_out->setIncomplete();
+        d_im.setIncomplete();
       }
     }
     // don't need to assert cardinality constraints if not producing models