Add TheoryInference base class (#4990)

This introduces a TheoryInference base class, which is a generalization and cleaner version of the former Lemma object. This changes the name of Lemma -> SimpleTheoryLemma, and makes the callback responsible for calling the inference manager.

This PR also updates the datatypes inference manager to use the new style. This required adding some additional interfaces to TheoryInferenceManager.

1 files changed, 63 insertions, 0 deletions

diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
new file mode 100644
index 000000000..618dc640b
--- /dev/null
+++ b/src/theory/theory_inference.cpp
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file theory_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory inference utility
+ **/
+
+#include "theory/theory_inference.h"
+
+#include "theory/theory_inference_manager.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+SimpleTheoryLemma::SimpleTheoryLemma(Node n,
+                                     LemmaProperty p,
+                                     ProofGenerator* pg)
+    : d_node(n), d_property(p), d_pg(pg)
+{
+}
+
+bool SimpleTheoryLemma::process(TheoryInferenceManager* im)
+{
+  Assert(!d_node.isNull());
+  // send (trusted) lemma on the output channel with property p
+  return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property);
+}
+
+SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc,
+                                                   Node exp,
+                                                   ProofGenerator* pg)
+    : d_conc(conc), d_exp(exp), d_pg(pg)
+{
+}
+
+bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im)
+{
+  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, {d_exp}, d_pg);
+  }
+  else
+  {
+    im->assertInternalFact(atom, polarity, d_exp);
+  }
+  return true;
+}
+
+}  // namespace theory
+}  // namespace CVC4