Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)

This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.

22 files changed, 111 insertions, 89 deletions

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index ecab1b92c..80217195f 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom)
   // tn is of kind REWRITE, turn this into a LEMMA here
   TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
   // must preprocess
-  d_im.trustedLemma(tlem);
+  d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
   // mark the atom as reduced
   d_reduced[atom] = true;
   return true;
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index f2c805d38..be2972444 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -53,9 +53,9 @@ bool InferenceManager::assertInference(TNode atom,
     std::vector<Node> args;
     // convert to proof rule application
     convert(id, fact, reason, children, args);
-    return assertInternalFact(atom, polarity, id, children, args);
+    return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args);
   }
-  return assertInternalFact(atom, polarity, reason);
+  return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason);
 }
 
 bool InferenceManager::arrayLemma(
@@ -72,11 +72,11 @@ bool InferenceManager::arrayLemma(
     convert(id, conc, exp, children, args);
     // make the trusted lemma based on the eager proof generator and send
     TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args);
-    return trustedLemma(tlem, p, doCache);
+    return trustedLemma(tlem, InferenceId::UNKNOWN, p, doCache);
   }
   // send lemma without proofs
   Node lem = nm->mkNode(IMPLIES, exp, conc);
-  return lemma(lem, p, doCache);
+  return lemma(lem, InferenceId::UNKNOWN, p, doCache);
 }
 
 void InferenceManager::convert(PfRule& id,
diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index c4e957087..0655b6bbf 100644
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -37,7 +37,7 @@ bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
   if (asLemma)
   {
     TrustNode trustedLemma = TrustNode::mkTrustLemma(lemma, nullptr);
-    im->trustedLemma(trustedLemma);
+    im->trustedLemma(trustedLemma, getId());
   }
   else
   {
@@ -47,7 +47,7 @@ bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
   {
     Node n = pair.first.eqNode(pair.second);
     TrustNode trustedLemma = TrustNode::mkTrustLemma(n, nullptr);
-    im->trustedLemma(trustedLemma);
+    im->trustedLemma(trustedLemma, getId());
   }
 
   Trace("bags::InferInfo::process") << (*this) << std::endl;
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 7f38c61a2..f3adc4b21 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -416,9 +416,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
       lemmab << d_cnf->getNode(clause[i]);
     }
     Node lemma = lemmab;
-    d_bv->d_inferManager.lemma(lemma);
+    d_bv->d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
   } else {
-    d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]));
+    d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]), InferenceId::UNKNOWN);
   }
 }
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 68192e1d4..ce8bc3645 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -97,7 +97,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     }
 
     NodeManager* nm = NodeManager::currentNM();
-    d_inferManager.conflict(nm->mkAnd(conflict));
+    d_inferManager.conflict(nm->mkAnd(conflict), InferenceId::UNKNOWN);
   }
 }
 
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index a19af44ac..9c44e32f1 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -196,7 +196,7 @@ void BVSolverLazy::sendConflict()
   {
     Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
                        << d_conflictNode << std::endl;
-    d_inferManager.conflict(d_conflictNode);
+    d_inferManager.conflict(d_conflictNode, InferenceId::UNKNOWN);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
   }
@@ -287,11 +287,11 @@ void BVSolverLazy::check(Theory::Effort e)
     {
       if (assertions.size() == 1)
       {
-        d_inferManager.conflict(assertions[0]);
+        d_inferManager.conflict(assertions[0], InferenceId::UNKNOWN);
         return;
       }
       Node conflict = utils::mkAnd(assertions);
-      d_inferManager.conflict(conflict);
+      d_inferManager.conflict(conflict, InferenceId::UNKNOWN);
       return;
     }
     return;
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 6885dbba4..da5f1cbf8 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -203,7 +203,7 @@ class BVSolverLazy : public BVSolver
 
   void lemma(TNode node)
   {
-    d_inferManager.lemma(node);
+    d_inferManager.lemma(node, InferenceId::UNKNOWN);
     d_lemmasAdded = true;
   }
 
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 98fce24be..c4a404041 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -93,12 +93,12 @@ void BVSolverSimple::addBBLemma(TNode fact)
 
   if (d_epg == nullptr)
   {
-    d_inferManager.lemma(lemma);
+    d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
   }
   else
   {
     TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
-    d_inferManager.trustedLemma(tlem);
+    d_inferManager.trustedLemma(tlem, InferenceId::UNKNOWN);
   }
 }
 
@@ -123,13 +123,13 @@ bool BVSolverSimple::preNotifyFact(
 
     if (d_epg == nullptr)
     {
-      d_inferManager.lemma(lemma);
+      d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
     }
     else
     {
       TrustNode tlem =
           d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
-      d_inferManager.trustedLemma(tlem);
+      d_inferManager.trustedLemma(tlem, InferenceId::UNKNOWN);
     }
 
     std::unordered_set<Node, NodeHashFunction> bv_atoms;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index e29553063..87cc0bc4d 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -560,7 +560,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
                               nm->mkNode(kind::LT, n, max));
         Trace("bv-extf-lemma")
             << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->d_inferManager.lemma(lem);
+        d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
         sentLemma = true;
       }
     }
@@ -609,7 +609,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
           Trace("bv-extf-lemma")
               << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->d_inferManager.lemma(lem);
+          d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
           sentLemma = true;
         }
       }
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 7ecac6e3f..affa401d4 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -87,7 +87,7 @@ void InferenceManager::sendDtLemma(Node lem,
     return;
   }
   // otherwise send as a normal lemma
-  if (lemma(lem, p, doCache))
+  if (lemma(lem, id, p, doCache))
   {
     d_inferenceLemmas << id;
   }
@@ -100,7 +100,7 @@ void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId
     Node exp = NodeManager::currentNM()->mkAnd(conf);
     prepareDtInference(d_false, exp, id, d_ipc.get());
   }
-  conflictExp(conf, d_ipc.get());
+  conflictExp(id, conf, d_ipc.get());
   d_inferenceConflicts << id;
 }
 
@@ -109,7 +109,7 @@ bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
   bool ret = false;
   for (const Node& lem : lemmas)
   {
-    if (lemma(lem))
+    if (lemma(lem, InferenceId::UNKNOWN))
     {
       ret = true;
     }
@@ -154,7 +154,7 @@ bool InferenceManager::processDtLemma(
   }
   // use trusted lemma
   TrustNode tlem = TrustNode::mkTrustLemma(lem, d_lemPg.get());
-  if (!trustedLemma(tlem))
+  if (!trustedLemma(tlem, id))
   {
     Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl;
     return false;
@@ -176,12 +176,12 @@ bool InferenceManager::processDtFact(Node conc, Node exp, InferenceId id)
     {
       expv.push_back(exp);
     }
-    assertInternalFact(atom, polarity, expv, d_ipc.get());
+    assertInternalFact(atom, polarity, id, expv, d_ipc.get());
   }
   else
   {
     // use version without proofs
-    assertInternalFact(atom, polarity, exp);
+    assertInternalFact(atom, polarity, id, exp);
   }
   d_inferenceFacts << id;
   return true;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 064a4b2d1..153f7c850 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -252,7 +252,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     assumptions.push_back(assumption);
                     Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
                     Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
-                    d_im.lemma(lemma);
+                    d_im.lemma(lemma, InferenceId::UNKNOWN);
                   }
                 }
               }else{
@@ -318,7 +318,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     NodeBuilder<> nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
-                    d_im.lemma(lemma);
+                    d_im.lemma(lemma, InferenceId::UNKNOWN);
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
@@ -1415,7 +1415,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
       Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
-      d_im.lemma(a);
+      d_im.lemma(a, InferenceId::UNKNOWN);
       Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
     }
     d_singleton_lemma[index][tn] = a;
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 299ef7239..a38a92b6a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1787,7 +1787,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c
                            << std::endl;
-        d_im.conflictExp(ant, nullptr);
+        d_im.conflictExp(InferenceId::UNKNOWN, ant, nullptr);
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
                            << " by " << c << std::endl;
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index fe4a5875a..15b7f64dc 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -57,7 +57,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     if (fact == d_false)
     {
       Trace("sets-lemma") << "Conflict : " << exp << std::endl;
-      conflict(exp);
+      conflict(exp, InferenceId::UNKNOWN);
       return true;
     }
     return false;
@@ -90,7 +90,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
       || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
   {
     // send to equality engine
-    if (assertInternalFact(atom, polarity, exp))
+    if (assertInternalFact(atom, polarity, InferenceId::UNKNOWN, exp))
     {
       // return true if this wasn't redundant
       return true;
@@ -164,7 +164,7 @@ void InferenceManager::split(Node n, int reqPol)
   n = Rewriter::rewrite(n);
   Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
   // send the lemma
-  lemma(lem);
+  lemma(lem, InferenceId::UNKNOWN);
   Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
   if (reqPol != 0)
   {
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index 1e780721d..975581dfa 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -53,13 +53,13 @@ Node TermRegistry::getProxy(Node n)
   d_proxy_to_term[k] = n;
   Node eq = k.eqNode(n);
   Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
-  d_im.lemma(eq, LemmaProperty::NONE, false);
+  d_im.lemma(eq, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
   if (nk == SINGLETON)
   {
     Node slem = nm->mkNode(MEMBER, n[0], k);
     Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
                         << std::endl;
-    d_im.lemma(slem, LemmaProperty::NONE, false);
+    d_im.lemma(slem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
   }
   return k;
 }
@@ -104,7 +104,7 @@ Node TermRegistry::getUnivSet(TypeNode tn)
       Node ulem = nm->mkNode(SUBSET, n1, n2);
       Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
                           << std::endl;
-      d_im.lemma(ulem, LemmaProperty::NONE, false);
+      d_im.lemma(ulem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
     }
   }
   d_univset[tn] = n;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 0d1206dec..867c87c59 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -104,7 +104,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
             // infer equality between elements of singleton
             Node exp = s1.eqNode(s2);
             Node eq = s1[0].eqNode(s2[0]);
-            d_im.assertInternalFact(eq, true, exp);
+            d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, exp);
           }
           else
           {
@@ -137,7 +137,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
       Assert(facts.size() == 1);
       Trace("sets-prop") << "Propagate eq-mem conflict : " << facts[0]
                          << std::endl;
-      d_im.conflict(facts[0]);
+      d_im.conflict(facts[0], InferenceId::UNKNOWN);
       return;
     }
     for (const Node& f : facts)
@@ -145,7 +145,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
       Assert(f.getKind() == kind::IMPLIES);
       Trace("sets-prop") << "Propagate eq-mem eq inference : " << f[0] << " => "
                          << f[1] << std::endl;
-      d_im.assertInternalFact(f[1], true, f[0]);
+      d_im.assertInternalFact(f[1], true, InferenceId::UNKNOWN, f[0]);
     }
   }
 }
@@ -764,7 +764,7 @@ void TheorySetsPrivate::checkReduceComprehensions()
         nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
     Trace("sets-comprehension")
         << "Comprehension reduction: " << lem << std::endl;
-    d_im.lemma(lem);
+    d_im.lemma(lem, InferenceId::UNKNOWN);
   }
 }
 
@@ -818,14 +818,14 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
             Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
             Node eq = s[0].eqNode(atom[0]);
             // triggers an internal inference
-            d_im.assertInternalFact(eq, true, pexp);
+            d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, pexp);
           }
         }
         else
         {
           Trace("sets-prop")
               << "Propagate mem-eq conflict : " << pexp << std::endl;
-          d_im.conflict(pexp);
+          d_im.conflict(pexp, InferenceId::UNKNOWN);
         }
       }
     }
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a348585e7..8c487d7c1 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -299,7 +299,7 @@ void InferenceManager::processConflict(const InferInfo& ii)
   Trace("strings-assert") << "(assert (not " << tconf.getNode()
                           << ")) ; conflict " << ii.getId() << std::endl;
   // send the trusted conflict
-  trustedConflict(tconf);
+  trustedConflict(tconf, ii.getId());
 }
 
 bool InferenceManager::processFact(InferInfo& ii)
@@ -342,13 +342,13 @@ bool InferenceManager::processFact(InferInfo& ii)
       // current SAT context
       d_ipc->notifyFact(ii);
       // now, assert the internal fact with d_ipc as proof generator
-      curRet = assertInternalFact(atom, polarity, exp, d_ipc.get());
+      curRet = assertInternalFact(atom, polarity, ii.getId(), exp, d_ipc.get());
     }
     else
     {
       Node cexp = utils::mkAnd(exp);
       // without proof generator
-      curRet = assertInternalFact(atom, polarity, cexp);
+      curRet = assertInternalFact(atom, polarity, ii.getId(), cexp);
     }
     ret = ret || curRet;
     // may be in conflict
@@ -420,7 +420,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   ++(d_statistics.d_lemmasInfer);
 
   // call the trusted lemma, without caching
-  return trustedLemma(tlem, p, false);
+  return trustedLemma(tlem, ii.getId(), p, false);
 }
 
 }  // namespace strings
diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index f64b88daa..8ccbb7e1f 100644
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -34,7 +34,7 @@ bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma)
   Assert(!d_node.isNull());
   Assert(asLemma);
   // send (trusted) lemma on the output channel with property p
-  return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property);
+  return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), getId(), d_property);
 }
 
 SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
@@ -54,11 +54,11 @@ bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im, bool asLemma)
   Assert(atom.getKind() != NOT && atom.getKind() != AND);
   if (d_pg != nullptr)
   {
-    im->assertInternalFact(atom, polarity, {d_exp}, d_pg);
+    im->assertInternalFact(atom, polarity, getId(), {d_exp}, d_pg);
   }
   else
   {
-    im->assertInternalFact(atom, polarity, d_exp);
+    im->assertInternalFact(atom, polarity, getId(), d_exp);
   }
   return true;
 }
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 58a8b86a4..a56d616d9 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -85,7 +85,7 @@ void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
   }
 }
 
-void TheoryInferenceManager::conflict(TNode conf)
+void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
@@ -95,7 +95,7 @@ void TheoryInferenceManager::conflict(TNode conf)
   }
 }
 
-void TheoryInferenceManager::trustedConflict(TrustNode tconf)
+void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
@@ -104,16 +104,17 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf)
   }
 }
 
-void TheoryInferenceManager::conflictExp(PfRule id,
+void TheoryInferenceManager::conflictExp(InferenceId id,
+                                         PfRule pfr,
                                          const std::vector<Node>& exp,
                                          const std::vector<Node>& args)
 {
   if (!d_theoryState.isInConflict())
   {
     // make the trust node
-    TrustNode tconf = mkConflictExp(id, exp, args);
+    TrustNode tconf = mkConflictExp(pfr, exp, args);
     // send it on the output channel
-    trustedConflict(tconf);
+    trustedConflict(tconf, id);
   }
 }
 
@@ -131,7 +132,8 @@ TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
   return TrustNode::mkTrustConflict(conf, nullptr);
 }
 
-void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
+void TheoryInferenceManager::conflictExp(InferenceId id,
+                                         const std::vector<Node>& exp,
                                          ProofGenerator* pg)
 {
   if (!d_theoryState.isInConflict())
@@ -139,7 +141,7 @@ void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
     // make the trust node
     TrustNode tconf = mkConflictExp(exp, pg);
     // send it on the output channel
-    trustedConflict(tconf);
+    trustedConflict(tconf, id);
   }
 }
 
@@ -207,13 +209,17 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
                   << " mkTrustedConflictEqConstantMerge";
 }
 
-bool TheoryInferenceManager::lemma(TNode lem, LemmaProperty p, bool doCache)
+bool TheoryInferenceManager::lemma(TNode lem,
+                                   InferenceId id,
+                                   LemmaProperty p,
+                                   bool doCache)
 {
   TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
-  return trustedLemma(tlem, p, doCache);
+  return trustedLemma(tlem, id, p, doCache);
 }
 
 bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
+                                          InferenceId id,
                                           LemmaProperty p,
                                           bool doCache)
 {
@@ -230,7 +236,8 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
 }
 
 bool TheoryInferenceManager::lemmaExp(Node conc,
-                                      PfRule id,
+                                      InferenceId id,
+                                      PfRule pfr,
                                       const std::vector<Node>& exp,
                                       const std::vector<Node>& noExplain,
                                       const std::vector<Node>& args,
@@ -238,9 +245,9 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
                                       bool doCache)
 {
   // make the trust node
-  TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args);
+  TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
   // send it on the output channel
-  return trustedLemma(trn, p, doCache);
+  return trustedLemma(trn, id, p, doCache);
 }
 
 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
@@ -261,6 +268,7 @@ TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 }
 
 bool TheoryInferenceManager::lemmaExp(Node conc,
+                                      InferenceId id,
                                       const std::vector<Node>& exp,
                                       const std::vector<Node>& noExplain,
                                       ProofGenerator* pg,
@@ -270,7 +278,7 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
   // make the trust node
   TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
   // send it on the output channel
-  return trustedLemma(trn, p, doCache);
+  return trustedLemma(trn, id, p, doCache);
 }
 
 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
@@ -305,23 +313,28 @@ bool TheoryInferenceManager::hasSentLemma() const
   return d_numCurrentLemmas != 0;
 }
 
-bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
+bool TheoryInferenceManager::assertInternalFact(TNode atom,
+                                                bool pol,
+                                                InferenceId id,
+                                                TNode exp)
 {
   return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 }
 
 bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
-                                                PfRule id,
+                                                InferenceId id,
+                                                PfRule pfr,
                                                 const std::vector<Node>& exp,
                                                 const std::vector<Node>& args)
 {
-  Assert(id != PfRule::UNKNOWN);
-  return processInternalFact(atom, pol, id, exp, args, nullptr);
+  Assert(pfr != PfRule::UNKNOWN);
+  return processInternalFact(atom, pol, pfr, exp, args, nullptr);
 }
 
 bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
+                                                InferenceId id,
                                                 const std::vector<Node>& exp,
                                                 ProofGenerator* pg)
 {
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 324ceb5e1..7a125789b 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -132,12 +132,12 @@ class TheoryInferenceManager
    * Raise conflict conf (of any form), without proofs. This method should
    * only be called if there is not yet proof support in the given theory.
    */
-  void conflict(TNode conf);
+  void conflict(TNode conf, InferenceId id);
   /**
    * Raise trusted conflict tconf (of any form) where a proof generator has
    * been provided (as part of the trust node) in a custom way.
    */
-  void trustedConflict(TrustNode tconf);
+  void trustedConflict(TrustNode tconf, InferenceId id);
   /**
    * Explain and send conflict from contradictory facts. This method is called
    * when the proof rule id with premises exp and arguments args concludes
@@ -145,7 +145,8 @@ class TheoryInferenceManager
    * equality engine's explanation of literals in exp, with the proof equality
    * engine as the proof generator (if it exists).
    */
-  void conflictExp(PfRule id,
+  void conflictExp(InferenceId id,
+                   PfRule pfr,
                    const std::vector<Node>& exp,
                    const std::vector<Node>& args);
   /**
@@ -153,7 +154,7 @@ class TheoryInferenceManager
    * the responsibility of the caller to subsequently call trustedConflict with
    * the returned trust node.
    */
-  TrustNode mkConflictExp(PfRule id,
+  TrustNode mkConflictExp(PfRule pfr,
                           const std::vector<Node>& exp,
                           const std::vector<Node>& args);
   /**
@@ -164,7 +165,9 @@ class TheoryInferenceManager
    * engine as the proof generator (if it exists), where pg provides the
    * final step(s) of this proof during this call.
    */
-  void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+  void conflictExp(InferenceId id,
+                   const std::vector<Node>& exp,
+                   ProofGenerator* pg);
   /**
    * Make the trust node corresponding to the conflict of the above form. It is
    * the responsibility of the caller to subsequently call trustedConflict with
@@ -182,6 +185,7 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool trustedLemma(const TrustNode& tlem,
+                    InferenceId id,
                     LemmaProperty p = LemmaProperty::NONE,
                     bool doCache = true);
   /**
@@ -189,6 +193,7 @@ class TheoryInferenceManager
    * a node instead of a trust node.
    */
   bool lemma(TNode lem,
+             InferenceId id,
              LemmaProperty p = LemmaProperty::NONE,
              bool doCache = true);
   /**
@@ -215,7 +220,8 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool lemmaExp(Node conc,
-                PfRule id,
+                InferenceId id,
+                PfRule pfr,
                 const std::vector<Node>& exp,
                 const std::vector<Node>& noExplain,
                 const std::vector<Node>& args,
@@ -246,6 +252,7 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool lemmaExp(Node conc,
+                InferenceId id,
                 const std::vector<Node>& exp,
                 const std::vector<Node>& noExplain,
                 ProofGenerator* pg = nullptr,
@@ -286,7 +293,7 @@ class TheoryInferenceManager
    * @return true if the fact was processed, i.e. it was asserted to the
    * equality engine or preNotifyFact returned true.
    */
-  bool assertInternalFact(TNode atom, bool pol, TNode exp);
+  bool assertInternalFact(TNode atom, bool pol, InferenceId id, TNode exp);
   /**
    * Assert internal fact, with a proof step justification. Notice that if
    * proofs are not enabled in this inference manager, then this asserts
@@ -302,7 +309,8 @@ class TheoryInferenceManager
    */
   bool assertInternalFact(TNode atom,
                           bool pol,
-                          PfRule id,
+                          InferenceId id,
+                          PfRule pfr,
                           const std::vector<Node>& exp,
                           const std::vector<Node>& args);
   /**
@@ -320,6 +328,7 @@ class TheoryInferenceManager
    */
   bool assertInternalFact(TNode atom,
                           bool pol,
+                          InferenceId id,
                           const std::vector<Node>& exp,
                           ProofGenerator* pg);
   /** The number of internal facts we have added since the last call to reset */
@@ -327,7 +336,7 @@ class TheoryInferenceManager
   /** Have we added a internal fact since the last call to reset? */
   bool hasSentFact() const;
   //--------------------------------------- phase requirements
-  /** 
+  /**
    * Set that literal n has SAT phase requirement pol, that is, it should be
    * decided with polarity pol, for details see OutputChannel::requirePhase.
    */
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index bd69245b8..697a828a4 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r)
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
     // send lemma, with caching
-    if (d_im.lemma(lem))
+    if (d_im.lemma(lem, InferenceId::UNKNOWN))
     {
       Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
       //tell the sat solver to explore the equals branch first
@@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique)
   eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
   Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
   // send lemma, with caching
-  if (d_im.lemma(lem))
+  if (d_im.lemma(lem, InferenceId::UNKNOWN))
   {
     Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
     ++(d_thss->d_statistics.d_clique_lemmas);
@@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() {
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
                                                       getCardinalityLiteral( d_maxNegCard.get() ).negate() );
     Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
-    d_im.conflict(lem);
+    d_im.conflict(lem, InferenceId::UNKNOWN);
   }
 }
 
@@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall()
         Node lem = NodeManager::currentNM()->mkNode(
             OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
         Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
-        d_im.lemma(lem, LemmaProperty::NONE, false);
+        d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
         return false;
       }
     }
@@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
           eqv_lit = lit.eqNode( eqv_lit );
           Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-          d_im.lemma(eqv_lit, LemmaProperty::NONE, false);
+          d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
           d_card_assertions_eqv_lemma[lit] = true;
         }
       }
@@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level)
                     Node eq = Rewriter::rewrite( a.eqNode( b ) );
                     Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                     Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
-                    d_im.lemma(lem, LemmaProperty::NONE, false);
+                    d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
                     d_im.requirePhase(eq, true);
                     type_proc[tn] = true;
                     break;
@@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality()
                              << " : " << cf << std::endl;
         Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
                                 << " : " << cf << std::endl;
-        d_im.conflict(cf);
+        d_im.conflict(cf, InferenceId::UNKNOWN);
         return;
       }
     }
@@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality()
                            << std::endl;
       Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
                               << std::endl;
-      d_im.conflict(cf);
+      d_im.conflict(cf, InferenceId::UNKNOWN);
     }
   }
 }
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 66bcbc76f..55e2500af 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                          << std::endl;
-    d_im.lemma(lem);
+    d_im.lemma(lem, InferenceId::UNKNOWN);
     return 1;
   }
   return 0;
@@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       Trace("uf-ho-lemma")
           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
           << std::endl;
-      d_im.lemma(lem);
+      d_im.lemma(lem, InferenceId::UNKNOWN);
       d_uf_std_skolem[f] = new_f;
     }
     else
@@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
               Node lem = nm->mkNode(OR, deq.negate(), eq);
               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                              << std::endl;
-              d_im.lemma(lem);
+              d_im.lemma(lem, InferenceId::UNKNOWN);
               return 1;
             }
           }
@@ -284,7 +284,7 @@ unsigned HoExtension::applyAppCompletion(TNode n)
     Node eq = n.eqNode(ret);
     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                          << std::endl;
-    d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n});
+    d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n});
     return 1;
   }
   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
@@ -441,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
       Node eq = n.eqNode(hn);
       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                      << std::endl;
-      d_im.lemma(eq);
+      d_im.lemma(eq, InferenceId::UNKNOWN);
       return false;
     }
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6fdc969a4..c8cfe295e 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -315,7 +315,7 @@ void TheoryUF::presolve() {
         ++i) {
       Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
       // no proof generator provided
-      d_im.lemma(*i);
+      d_im.lemma(*i, InferenceId::UNKNOWN);
     }
   }
   if( d_thss ){