Make linear arithmetic use its inference manager (#5934)

This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.

14 files changed, 89 insertions, 273 deletions

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index ee412483b..81f48ad00 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -64,9 +64,9 @@ RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
   : d_ta(ta)
 {}
 
-void RaiseConflict::raiseConflict(ConstraintCP c) const{
+void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
   Assert(c->inConflict());
-  d_ta.raiseConflict(c);
+  d_ta.raiseConflict(c, id);
 }
 
 FarkasConflictBuilder::FarkasConflictBuilder()
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 574d289b0..9f0ae1017 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -21,6 +21,7 @@
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
+#include "theory/inference_id.h"
 #include "util/rational.h"
 
 namespace CVC4 {
@@ -111,7 +112,7 @@ public:
   RaiseConflict(TheoryArithPrivate& ta);
 
   /** Calls d_ta.raiseConflict(c) */
-  void raiseConflict(ConstraintCP c) const;
+  void raiseConflict(ConstraintCP c, InferenceId id) const;
 };
 
 class FarkasConflictBuilder {
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index bafd4d682..f2de5da6c 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -2236,7 +2236,7 @@ bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
   if(cons->negationHasProof()){
     Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
     cons->impliedByUnate(ant, true);
-    d_raiseConflict.raiseConflict(cons);
+    d_raiseConflict.raiseConflict(cons, InferenceId::UNKNOWN);
     return true;
   }else if(!cons->isTrue()){
     ++d_statistics.d_unatePropagateImplications;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 3f32e7075..671c3f44a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -244,6 +244,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
 
 void NonlinearExtension::check(Theory::Effort e)
 {
+  d_im.reset();
   Trace("nl-ext") << std::endl;
   Trace("nl-ext") << "NonlinearExtension::check, effort = " << e
                   << ", built model = " << d_builtModel.get() << std::endl;
@@ -277,7 +278,6 @@ void NonlinearExtension::check(Theory::Effort e)
       d_im.doPendingFacts();
       d_im.doPendingLemmas();
       d_im.doPendingPhaseRequirements();
-      d_im.reset();
       return;
     }
     // Otherwise, we will answer SAT. The values that we approximated are
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index df399d686..d93e42215 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -94,7 +94,7 @@ void SimplexDecisionProcedure::reportConflict(ArithVar basic){
 
   ConstraintCP conflicted = generateConflictForBasic(basic);
   Assert(conflicted != NullConstraint);
-  d_conflictChannel.raiseConflict(conflicted);
+  d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
 
   d_conflictVariables.add(basic);
 }
@@ -117,7 +117,7 @@ ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic)
 bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
   if(checkBasicForConflict(basic)){
     ConstraintCP conflicted = generateConflictForBasic(basic);
-    d_conflictChannel.raiseConflict(conflicted);
+    d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
     return true;
   }else{
     return false;
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 79136e77c..2ea3fd546 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -846,7 +846,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
       d_conflictBuilder->addConstraint(c, coeff);
     }
     ConstraintCP conflicted = d_conflictBuilder->commitConflict();
-    d_conflictChannel.raiseConflict(conflicted);
+    d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
   }
 
   tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e3c4919a3..83337dd90 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -47,15 +47,15 @@ TheoryArith::TheoryArith(context::Context* c,
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
       d_ppPfGen(pnm, c, "Arith::ppRewrite"),
       d_astate(*d_internal, c, u, valuation),
-      d_inferenceManager(*this, d_astate, pnm),
+      d_im(*this, d_astate, pnm),
       d_nonlinearExtension(nullptr),
-      d_arithPreproc(d_astate, d_inferenceManager, pnm, logicInfo)
+      d_arithPreproc(d_astate, d_im, pnm, logicInfo)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
 
   // indicate we are using the theory state object and inference manager
   d_theoryState = &d_astate;
-  d_inferManager = &d_inferenceManager;
+  d_inferManager = &d_im;
 }
 
 TheoryArith::~TheoryArith(){
@@ -199,7 +199,7 @@ void TheoryArith::postCheck(Effort level)
     else if (d_internal->foundNonlinear())
     {
       // set incomplete
-      d_inferenceManager.setIncomplete();
+      d_im.setIncomplete();
     }
   }
 }
@@ -270,7 +270,7 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
     {
       Node eq = p.first.eqNode(p.second);
       Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
-      d_out->lemma(lem);
+      d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
     }
     return false;
   }
@@ -307,7 +307,7 @@ std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
 }
 eq::ProofEqEngine* TheoryArith::getProofEqEngine()
 {
-  return d_inferenceManager.getProofEqEngine();
+  return d_im.getProofEqEngine();
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 41cc9591d..e0fa1b2d0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -135,7 +135,7 @@ class TheoryArith : public Theory {
   /** Return a reference to the arith::InferenceManager. */
   InferenceManager& getInferenceManager()
   {
-    return d_inferenceManager;
+    return d_im;
   }
 
  private:
@@ -149,7 +149,7 @@ class TheoryArith : public Theory {
   /** The state object wrapping TheoryArithPrivate  */
   ArithState d_astate;
   /** The arith::InferenceManager. */
-  InferenceManager d_inferenceManager;
+  InferenceManager d_im;
 
   /**
    * The non-linear extension, responsible for all approaches for non-linear
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 1faad2a7a..74b13aed1 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -535,9 +535,9 @@ bool TheoryArithPrivate::isProofEnabled() const
   return d_pnm != nullptr;
 }
 
-void TheoryArithPrivate::raiseConflict(ConstraintCP a){
+void TheoryArithPrivate::raiseConflict(ConstraintCP a, InferenceId id){
   Assert(a->inConflict());
-  d_conflicts.push_back(a);
+  d_conflicts.push_back(std::make_pair(a, id));
 }
 
 void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
@@ -654,7 +654,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
     ConstraintP negation = constraint->getNegation();
     negation->impliedByUnate(ubc, true);
 
-    raiseConflict(constraint);
+    raiseConflict(constraint, InferenceId::ARITH_CONF_LOWER);
 
     ++(d_statistics.d_statAssertLowerConflicts);
     return true;
@@ -690,7 +690,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
       }
       if(triConflict){
         ++(d_statistics.d_statDisequalityConflicts);
-        raiseConflict(eq);
+        raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
         return true;
       }
     }
@@ -714,7 +714,7 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
           negUb->tryToPropagate();
         }
         if(ubInConflict){
-          raiseConflict(ub);
+          raiseConflict(ub, InferenceId::ARITH_CONF_TRICHOTOMY);
           return true;
         }else if(learnNegUb){
           d_learnedBounds.push_back(negUb);
@@ -795,7 +795,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
     ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
     ConstraintP negConstraint = constraint->getNegation();
     negConstraint->impliedByUnate(lbc, true);
-    raiseConflict(constraint);
+    raiseConflict(constraint, InferenceId::ARITH_CONF_UPPER);
     ++(d_statistics.d_statAssertUpperConflicts);
     return true;
   }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
@@ -829,7 +829,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
       }
       if(triConflict){
         ++(d_statistics.d_statDisequalityConflicts);
-        raiseConflict(eq);
+        raiseConflict(eq, InferenceId::ARITH_CONF_TRICHOTOMY);
         return true;
       }
     }
@@ -853,7 +853,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
           negLb->tryToPropagate();
         }
         if(lbInConflict){
-          raiseConflict(lb);
+          raiseConflict(lb, InferenceId::ARITH_CONF_TRICHOTOMY);
           return true;
         }else if(learnNegLb){
           d_learnedBounds.push_back(negLb);
@@ -935,7 +935,7 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
     ConstraintP diseq = constraint->getNegation();
     Assert(!diseq->isTrue());
     diseq->impliedByUnate(cb, true);
-    raiseConflict(constraint);
+    raiseConflict(constraint, InferenceId::ARITH_CONF_EQ);
     return true;
   }
 
@@ -1027,7 +1027,7 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
     if(lb->isTrue() && ub->isTrue()){
       ConstraintP eq = constraint->getNegation();
       eq->impliedByTrichotomy(lb, ub, true);
-      raiseConflict(constraint);
+      raiseConflict(constraint, InferenceId::ARITH_CONF_TRICHOTOMY);
       //in conflict
       ++(d_statistics.d_statDisequalityConflicts);
       return true;
@@ -1067,7 +1067,7 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
 
   if(!split && c_i == d_partialModel.getAssignment(x_i)){
     Debug("arith::eq") << "lemma now! " << constraint << endl;
-    outputTrustedLemma(constraint->split());
+    outputTrustedLemma(constraint->split(), InferenceId::ARITH_SPLIT_DEQ);
     return false;
   }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
     Debug("arith::eq") << "can drop as less than lb" << constraint << endl;
@@ -1780,7 +1780,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
     Debug("arith::eq") << "negation has proof" << endl;
     Debug("arith::eq") << constraint << endl;
     Debug("arith::eq") << negation << endl;
-    raiseConflict(negation);
+    raiseConflict(negation, InferenceId::UNKNOWN);
     return NullConstraint;
   }else{
     return constraint;
@@ -1806,7 +1806,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
         floorConstraint->impliedByIntTighten(constraint, inConflict);
         floorConstraint->tryToPropagate();
         if(inConflict){
-          raiseConflict(floorConstraint);
+          raiseConflict(floorConstraint, InferenceId::ARITH_TIGHTEN_FLOOR);
           return true;
         }
       }
@@ -1826,7 +1826,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
         ceilingConstraint->impliedByIntTighten(constraint, inConflict);
         ceilingConstraint->tryToPropagate();
         if(inConflict){
-          raiseConflict(ceilingConstraint);
+          raiseConflict(ceilingConstraint, InferenceId::ARITH_TIGHTEN_CEIL);
           return true;
         }
       }
@@ -1932,7 +1932,8 @@ void TheoryArithPrivate::outputConflicts(){
   if(!conflictQueueEmpty()){
     Assert(!d_conflicts.empty());
     for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
-      ConstraintCP confConstraint = d_conflicts[i];
+      const std::pair<ConstraintCP, InferenceId>& conf = d_conflicts[i];
+      const ConstraintCP& confConstraint = conf.first;
       bool hasProof = confConstraint->hasProof();
       Assert(confConstraint->inConflict());
       const ConstraintRule& pf = confConstraint->getConstraintRule();
@@ -1961,11 +1962,11 @@ void TheoryArithPrivate::outputConflicts(){
 
       if (isProofEnabled())
       {
-        outputTrustedConflict(trustedConflict);
+        outputTrustedConflict(trustedConflict, conf.second);
       }
       else
       {
-        outputConflict(conflict);
+        outputConflict(conflict, conf.second);
       }
     }
   }
@@ -1982,41 +1983,41 @@ void TheoryArithPrivate::outputConflicts(){
     if (isProofEnabled() && d_blackBoxConflictPf.get())
     {
       auto confPf = d_blackBoxConflictPf.get();
-      outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true));
+      outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true), InferenceId::ARITH_BLACK_BOX);
     }
     else
     {
-      outputConflict(bb);
+      outputConflict(bb, InferenceId::ARITH_BLACK_BOX);
     }
   }
 }
 
-void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma)
+void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
 {
   Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
-  (d_containing.d_out)->trustedLemma(lemma);
+  d_containing.d_im.trustedLemma(lemma, id);
 }
 
-void TheoryArithPrivate::outputLemma(TNode lem) {
+void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
   Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
-  (d_containing.d_out)->lemma(lem);
+  d_containing.d_im.lemma(lem, id);
 }
 
-void TheoryArithPrivate::outputTrustedConflict(TrustNode conf)
+void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id)
 {
   Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl;
-  (d_containing.d_out)->trustedConflict(conf);
+  d_containing.d_im.trustedConflict(conf, id);
 }
 
-void TheoryArithPrivate::outputConflict(TNode lit) {
+void TheoryArithPrivate::outputConflict(TNode lit, InferenceId id) {
   Debug("arith::channel") << "Arith conflict: " << lit << std::endl;
-  (d_containing.d_out)->conflict(lit);
+  d_containing.d_im.conflict(lit, id);
 }
 
 void TheoryArithPrivate::outputPropagate(TNode lit) {
   Debug("arith::channel") << "Arith propagation: " << lit << std::endl;
   // call the propagate lit method of the
-  (d_containing.d_out)->propagate(lit);
+  d_containing.d_im.propagateLit(lit);
 }
 
 void TheoryArithPrivate::outputRestart() {
@@ -2113,7 +2114,7 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
                                      << "  (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
                                      << "  (" << at_j->isTrue() <<") " << at_j << endl;
           neg_at_j->impliedByIntHole(vec, true);
-          raiseConflict(at_j);
+          raiseConflict(at_j, InferenceId::UNKNOWN);
           break;
         }
       }
@@ -2339,7 +2340,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
     for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
 
       conflicts.push_back(ConstraintCPVec());
-      intHoleConflictToVector(d_conflicts[i], conflicts.back());
+      intHoleConflictToVector(d_conflicts[i].first, conflicts.back());
       Constraint::assertionFringe(conflicts.back());
 
       // ConstraintCP conflicting = d_conflicts[i];
@@ -2371,7 +2372,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
     if(!contains(conf, bcneg)){
       Debug("approx::branch") << "reraise " << conf  << endl;
       ConstraintCP conflicting = vectorToIntHoleConflict(conf);
-      raiseConflict(conflicting);
+      raiseConflict(conflicting, InferenceId::UNKNOWN);
     }else if(!bci.proven()){
       drop(conf, bcneg);
       bci.setExplanation(conf);
@@ -2391,7 +2392,7 @@ void TheoryArithPrivate::replayAssert(ConstraintP c) {
     }
     Debug("approx::replayAssert") << "replayAssertion " << c << endl;
     if(inConflict){
-      raiseConflict(c);
+      raiseConflict(c, InferenceId::UNKNOWN);
     }else{
       assertionCases(c);
     }
@@ -2541,7 +2542,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
             }else {
               con->impliedByIntHole(exp, true);
               Debug("approx::replayLogRec") << "cut into conflict " << con << endl;
-              raiseConflict(con);
+              raiseConflict(con, InferenceId::UNKNOWN);
             }
           }else{
             ++d_statistics.d_cutsProofFailed;
@@ -2579,7 +2580,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
       /* if a conflict has been found stop */
       for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
         res.push_back(ConstraintCPVec());
-        intHoleConflictToVector(d_conflicts[i], res.back());
+        intHoleConflictToVector(d_conflicts[i].first, res.back());
       }
       ++d_statistics.d_replayLogRecEarlyExit;
     }else if(nl.isBranch()){
@@ -3552,7 +3553,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       Debug("arith::approx::cuts") << "approximate cut:" << lem << endl;
       anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode());
       Debug("arith::lemma") << "approximate cut:" << lem << endl;
-      outputTrustedLemma(lem);
+      outputTrustedLemma(lem, InferenceId::ARITH_APPROX_CUT);
     }
     if(anyFresh){
       emmittedConflictOrSplit = true;
@@ -3669,7 +3670,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
           d_hasDoneWorkSinceCut = false;
           d_cutCount = d_cutCount + 1;
           Debug("arith::lemma") << "dio cut   " << possibleLemma << endl;
-          outputTrustedLemma(possibleLemma);
+          outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT);
         }
       }
     }
@@ -3683,7 +3684,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
         emmittedConflictOrSplit = true;
         Debug("arith::lemma") << "rrbranch lemma"
                               << possibleLemma << endl;
-        outputTrustedLemma(possibleLemma);
+        outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA);
       }
     }
 
@@ -3693,7 +3694,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
           Node decompositionLemma = d_diosolver.nextDecompositionLemma();
           Debug("arith::lemma") << "dio decomposition lemma "
                                 << decompositionLemma << endl;
-          outputLemma(decompositionLemma);
+          outputLemma(decompositionLemma, InferenceId::ARITH_DIO_DECOMPOSITION);
         }
       }else{
         Debug("arith::restart") << "arith restart!" << endl;
@@ -3909,7 +3910,7 @@ bool TheoryArithPrivate::splitDisequalities(){
 
         Debug("arith::lemma")
             << "Now " << Rewriter::rewrite(lemma.getNode()) << endl;
-        outputTrustedLemma(lemma);
+        outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ);
         //cout << "Now " << Rewriter::rewrite(lemma) << endl;
         splitSomething = true;
       }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
@@ -4398,7 +4399,7 @@ void TheoryArithPrivate::presolve(){
   for(; i != i_end; ++i){
     TrustNode lem = *i;
     Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
-    outputTrustedLemma(lem);
+    outputTrustedLemma(lem, InferenceId::UNKNOWN);
   }
 }
 
@@ -4843,11 +4844,11 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
 
         // Output it
         TrustNode trustedClause = d_pfGen->mkTrustNode(clause, clausePf);
-        outputTrustedLemma(trustedClause);
+        outputTrustedLemma(trustedClause, InferenceId::UNKNOWN);
       }
       else
       {
-        outputLemma(clause);
+        outputLemma(clause, InferenceId::UNKNOWN);
       }
     }else{
       Assert(!implied->negationHasProof());
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 55a2472b3..5cbf95760 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -309,7 +309,7 @@ private:
 
 
   /** This is only used by simplex at the moment. */
-  context::CDList<ConstraintCP> d_conflicts;
+  context::CDList<std::pair<ConstraintCP, InferenceId>> d_conflicts;
 
   /** This is only used by simplex at the moment. */
   context::CDO<Node> d_blackBoxConflict;
@@ -323,7 +323,7 @@ private:
    * This adds the constraint a to the queue of conflicts in d_conflicts.
    * Both a and ~a must have a proof.
    */
-  void raiseConflict(ConstraintCP a);
+  void raiseConflict(ConstraintCP a, InferenceId id);
 
   // inline void raiseConflict(const ConstraintCPVec& cv){
   //   d_conflicts.push_back(cv);
@@ -693,10 +693,10 @@ private:
   inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); }
   inline void debugPrintFacts() const { d_containing.debugPrintFacts(); }
   inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
-  void outputTrustedLemma(TrustNode lem);
-  void outputLemma(TNode lem);
-  void outputTrustedConflict(TrustNode conf);
-  void outputConflict(TNode lit);
+  void outputTrustedLemma(TrustNode lem, InferenceId id);
+  void outputLemma(TNode lem, InferenceId id);
+  void outputTrustedConflict(TrustNode conf, InferenceId id);
+  void outputConflict(TNode lit, InferenceId id);
   void outputPropagate(TNode lit);
   void outputRestart();
 
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f5fda1747..b6d0d3c25 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -38,6 +38,28 @@ namespace theory {
 enum class InferenceId
 {
   // ---------------------------------- arith theory
+  //-------------------- linear core
+  // black box conflicts. It's magic.
+  ARITH_BLACK_BOX,
+  // conflicting equality
+  ARITH_CONF_EQ,
+  // conflicting lower bound
+  ARITH_CONF_LOWER,
+  // conflict due to trichotomy
+  ARITH_CONF_TRICHOTOMY,
+  // conflicting upper bound
+  ARITH_CONF_UPPER,
+  // introduces split on a disequality
+  ARITH_SPLIT_DEQ,
+  // tighten integer inequalities to ceiling
+  ARITH_TIGHTEN_CEIL,
+  // tighten integer inequalities to floor
+  ARITH_TIGHTEN_FLOOR,
+  ARITH_APPROX_CUT,
+  ARITH_BB_LEMMA,
+  ARITH_DIO_CUT,
+  ARITH_DIO_DECOMPOSITION,
+  ARITH_SPLIT_FOR_NL_MODEL,
   //-------------------- preprocessing
   // equivalence of term and its preprocessed form
   ARITH_PP_ELIM_OPERATORS,
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1c23d9041..3a90a8ace 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -458,13 +458,6 @@ class Theory {
   }
 
   /**
-   * Set the output channel associated to this theory.
-   */
-  void setOutputChannel(OutputChannel& out) {
-    d_out = &out;
-  }
-
-  /**
    * Get the output channel associated to this theory.
    */
   OutputChannel& getOutputChannel() {
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index 09757a304..d0ed5718e 100644
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -43,19 +43,9 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit
     TestSmtNoFinishInit::SetUp();
     d_smtEngine->setOption("incremental", "false");
     d_smtEngine->finishInit();
-    d_context = d_smtEngine->getContext();
-    d_user_context = d_smtEngine->getUserContext();
-    d_outputChannel.clear();
-    d_logicInfo.lock();
-    d_smtEngine->getTheoryEngine()
-        ->d_theoryTable[THEORY_ARITH]
-        ->setOutputChannel(d_outputChannel);
     d_arith = static_cast<TheoryArith*>(
         d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
 
-    d_preregistered.reset(new std::set<Node>());
-
-    d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
     d_realType.reset(new TypeNode(d_nodeManager->realType()));
     d_intType.reset(new TypeNode(d_nodeManager->integerType()));
   }
@@ -63,57 +53,15 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit
   void fakeTheoryEnginePreprocess(TNode input)
   {
     Assert(input == Rewriter::rewrite(input));
-    Node rewrite = input;
-    if (d_debug)
-    {
-      std::cout << "input " << input << " rewrite " << rewrite << std::endl;
-    }
-
-    std::list<Node> toPreregister;
-
-    toPreregister.push_back(rewrite);
-    for (std::list<Node>::iterator i = toPreregister.begin();
-         i != toPreregister.end();
-         ++i)
-    {
-      Node n = *i;
-      d_preregistered->insert(n);
-
-      for (Node::iterator citer = n.begin(); citer != n.end(); ++citer)
-      {
-        Node c = *citer;
-        if (d_preregistered->find(c) == d_preregistered->end())
-        {
-          toPreregister.push_back(c);
-        }
-      }
-    }
-    for (std::list<Node>::reverse_iterator i = toPreregister.rbegin();
-         i != toPreregister.rend();
-         ++i)
-    {
-      Node n = *i;
-      if (d_debug)
-      {
-        std::cout << "id " << n.getId() << " " << n << std::endl;
-      }
-      d_arith->preRegisterTerm(n);
-    }
+    d_smtEngine->getTheoryEngine()->preRegister(input);
   }
 
-  Context* d_context;
-  UserContext* d_user_context;
-  DummyOutputChannel d_outputChannel;
-  LogicInfo d_logicInfo;
   Theory::Effort d_level = Theory::EFFORT_FULL;
   TheoryArith* d_arith;
-  std::unique_ptr<std::set<Node>> d_preregistered;
-  std::unique_ptr<TypeNode> d_booleanType;
   std::unique_ptr<TypeNode> d_realType;
   std::unique_ptr<TypeNode> d_intType;
   const Rational d_zero = 0;
   const Rational d_one = 1;
-  bool d_debug = false;
 };
 
 TEST_F(TestTheoryWhiteArith, assert)
@@ -128,137 +76,6 @@ TEST_F(TestTheoryWhiteArith, assert)
   d_arith->assertFact(leq, true);
 
   d_arith->check(d_level);
-
-  ASSERT_EQ(d_outputChannel.getNumCalls(), 0u);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLt1)
-{
-  Node x = d_nodeManager->mkVar(*d_realType);
-  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
-  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
-  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
-  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
-  Node leq0 = Rewriter::rewrite(gt0.notNode());
-  Node leq1 = Rewriter::rewrite(gt1.notNode());
-  Node lt1 = Rewriter::rewrite(geq1.notNode());
-
-  fakeTheoryEnginePreprocess(leq0);
-  fakeTheoryEnginePreprocess(leq1);
-  fakeTheoryEnginePreprocess(geq1);
-
-  d_arith->presolve();
-  d_arith->assertFact(lt1, true);
-  d_arith->check(d_level);
-  d_arith->propagate(d_level);
-
-  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
-  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
-  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
-  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
-  std::cout << d_outputChannel.getIthNode(0) << std::endl << std::endl;
-  std::cout << d_outputChannel.getIthNode(1) << std::endl << std::endl;
-  std::cout << d_outputChannel.getIthNode(2) << std::endl << std::endl;
-
-  ASSERT_EQ(d_outputChannel.getNumCalls(), 3u);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
-  ASSERT_TRUE(d_outputChannel.getIthNode(0) == gt0OrLt1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
-  ASSERT_TRUE(d_outputChannel.getIthNode(1) == geq0OrLeq1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
-  ASSERT_EQ(d_outputChannel.getIthNode(2), leq1);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLeq0)
-{
-  Node x = d_nodeManager->mkVar(*d_realType);
-  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
-  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
-  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
-  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
-  Node leq0 = Rewriter::rewrite(gt0.notNode());
-  Node leq1 = Rewriter::rewrite(gt1.notNode());
-  Node lt1 = Rewriter::rewrite(geq1.notNode());
-
-  fakeTheoryEnginePreprocess(leq0);
-  fakeTheoryEnginePreprocess(leq1);
-  fakeTheoryEnginePreprocess(geq1);
-
-  d_arith->presolve();
-  d_arith->assertFact(leq0, true);
-  d_arith->check(d_level);
-  d_arith->propagate(d_level);
-
-  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
-  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
-  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
-  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
-  std::cout << d_outputChannel.getIthNode(0) << std::endl;
-  std::cout << d_outputChannel.getIthNode(1) << std::endl;
-  std::cout << d_outputChannel.getIthNode(2) << std::endl;
-  std::cout << d_outputChannel.getIthNode(3) << std::endl;
-
-  ASSERT_EQ(d_outputChannel.getNumCalls(), 4u);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
-  ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
-  ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
-  ASSERT_EQ(d_outputChannel.getIthNode(2), lt1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(3), PROPAGATE);
-  ASSERT_EQ(d_outputChannel.getIthNode(3), leq1);
-}
-
-TEST_F(TestTheoryWhiteArith, TPLeq1)
-{
-  Node x = d_nodeManager->mkVar(*d_realType);
-  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
-
-  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
-  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
-  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
-  Node leq0 = Rewriter::rewrite(gt0.notNode());
-  Node leq1 = Rewriter::rewrite(gt1.notNode());
-  Node lt1 = Rewriter::rewrite(geq1.notNode());
-
-  fakeTheoryEnginePreprocess(leq0);
-  fakeTheoryEnginePreprocess(leq1);
-  fakeTheoryEnginePreprocess(geq1);
-
-  d_arith->presolve();
-  d_arith->assertFact(leq1, true);
-  d_arith->check(d_level);
-  d_arith->propagate(d_level);
-
-  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
-  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
-  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
-  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
-
-  std::cout << d_outputChannel.getIthNode(0) << std::endl;
-  std::cout << d_outputChannel.getIthNode(1) << std::endl;
-
-  ASSERT_EQ(d_outputChannel.getNumCalls(), 2u);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
-  ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
-
-  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
-  ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
 }
 
 TEST_F(TestTheoryWhiteArith, int_normal_form)
diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp
index f66d81b94..048fac5ac 100644
--- a/test/unit/theory/theory_white.cpp
+++ b/test/unit/theory/theory_white.cpp
@@ -97,24 +97,6 @@ TEST_F(TestTheoryWhite, done)
   ASSERT_TRUE(d_dummy_theory->done());
 }
 
-TEST_F(TestTheoryWhite, outputChannel_accessors)
-{
-  /* void setOutputChannel(OutputChannel& out)  */
-  /* OutputChannel& getOutputChannel() */
-
-  DummyOutputChannel theOtherChannel;
-
-  ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &d_outputChannel);
-
-  d_dummy_theory->setOutputChannel(theOtherChannel);
-
-  ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &theOtherChannel);
-
-  const OutputChannel& oc = d_dummy_theory->getOutputChannel();
-
-  ASSERT_EQ(&oc, &theOtherChannel);
-}
-
 TEST_F(TestTheoryWhite, outputChannel)
 {
   Node n = d_atom0.orNode(d_atom1);