Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)

This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.

1 files changed, 6 insertions, 4 deletions

diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index 8e52c8cd1..f64b88daa 100644
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -21,10 +21,11 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-SimpleTheoryLemma::SimpleTheoryLemma(Node n,
+SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id, 
+                                     Node n,
                                      LemmaProperty p,
                                      ProofGenerator* pg)
-    : d_node(n), d_property(p), d_pg(pg)
+    : TheoryInference(id), d_node(n), d_property(p), d_pg(pg)
 {
 }
 
@@ -36,10 +37,11 @@ bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma)
   return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property);
 }
 
-SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc,
+SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
+                                                   Node conc,
                                                    Node exp,
                                                    ProofGenerator* pg)
-    : d_conc(conc), d_exp(exp), d_pg(pg)
+    : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg)
 {
 }