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