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.

1 files changed, 3 insertions, 3 deletions

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;