Refactoring theory inference process (#5920)

This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.

1 files changed, 8 insertions, 19 deletions

diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index 8ccbb7e1f..1089cdff3 100644
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -29,12 +29,11 @@ SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id,
 {
 }
 
-bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma)
+TrustNode SimpleTheoryLemma::processLemma(LemmaProperty& p)
 {
   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), getId(), d_property);
+  p = d_property;
+  return TrustNode::mkTrustLemma(d_node, d_pg);
 }
 
 SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
@@ -45,22 +44,12 @@ SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
 {
 }
 
-bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im, bool asLemma)
+Node SimpleTheoryInternalFact::processFact(std::vector<Node>& exp,
+                                           ProofGenerator*& pg)
 {
-  Assert(!asLemma);
-  bool polarity = d_conc.getKind() != NOT;
-  TNode atom = polarity ? d_conc : d_conc[0];
-  // no double negation or conjunctive conclusions
-  Assert(atom.getKind() != NOT && atom.getKind() != AND);
-  if (d_pg != nullptr)
-  {
-    im->assertInternalFact(atom, polarity, getId(), {d_exp}, d_pg);
-  }
-  else
-  {
-    im->assertInternalFact(atom, polarity, getId(), d_exp);
-  }
-  return true;
+  exp.push_back(d_exp);
+  pg = d_pg;
+  return d_conc;
 }
 
 }  // namespace theory