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, 106 insertions, 0 deletions

diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h
new file mode 100644
index 000000000..8d98051bf
--- /dev/null
+++ b/src/theory/theory_inference.h
@@ -0,0 +1,106 @@
+/*********************                                                        */
+/*! \file theory_inference.h
+ ** \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 "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_INFERENCE_H
+#define CVC4__THEORY__THEORY_INFERENCE_H
+
+#include "expr/node.h"
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TheoryInferenceManager;
+
+/**
+ * A theory inference base class. This class is an abstract data structure for
+ * storing pending lemmas or facts in the buffered inference manager. It can
+ * be seen a single use object capturing instructions for making a single
+ * call to TheoryInferenceManager for lemmas or facts.
+ */
+class TheoryInference
+{
+ public:
+  virtual ~TheoryInference() {}
+  /**
+   * Called by the provided inference manager to process this inference. This
+   * method should make call(s) to inference manager to process this
+   * inference, as well as processing any specific side effects. This method
+   * typically makes a single call to the provided inference manager e.g.
+   * d_im->trustedLemma or d_im->assertFactInternal. Notice it is the sole
+   * responsibility of this class to make this call; the inference manager
+   * does not call itself otherwise when processing pending inferences.
+   *
+   * @return true if the inference was successfully processed by the inference
+   * manager. This method for instance returns false if it corresponds to a
+   * lemma that was already cached by im and hence was discarded.
+   */
+  virtual bool process(TheoryInferenceManager* im) = 0;
+};
+
+/**
+ * A simple theory lemma with no side effects. Makes a single call to
+ * trustedLemma in its process method.
+ */
+class SimpleTheoryLemma : public TheoryInference
+{
+ public:
+  SimpleTheoryLemma(Node n, LemmaProperty p, ProofGenerator* pg);
+  virtual ~SimpleTheoryLemma() {}
+  /**
+   * Send the lemma using inference manager im, return true if the lemma was
+   * sent.
+   */
+  virtual bool process(TheoryInferenceManager* im) override;
+  /** The lemma to send */
+  Node d_node;
+  /** The lemma property (see OutputChannel::lemma) */
+  LemmaProperty d_property;
+  /**
+   * The proof generator for this lemma, which if non-null, is wrapped in a
+   * TrustNode to be set on the output channel via trustedLemma at the time
+   * the lemma is sent. This proof generator must be able to provide a proof
+   * for d_node in the remainder of the user context.
+   */
+  ProofGenerator* d_pg;
+};
+
+/**
+ * A simple internal fact with no side effects. Makes a single call to
+ * assertFactInternal in its process method.
+ */
+class SimpleTheoryInternalFact : public TheoryInference
+{
+ public:
+  SimpleTheoryInternalFact(Node conc, Node exp, ProofGenerator* pg);
+  virtual ~SimpleTheoryInternalFact() {}
+  /**
+   * Send the lemma using inference manager im, return true if the lemma was
+   * sent.
+   */
+  virtual bool process(TheoryInferenceManager* im) override;
+  /** The lemma to send */
+  Node d_conc;
+  /** The explanation */
+  Node d_exp;
+  /** The proof generator */
+  ProofGenerator* d_pg;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif