Add the buffered inference manager (#4954)

This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class.

This PR adds basic calls to add lemmas on the output channel from InferenceManager.

It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from.

This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination.

5 files changed, 301 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e86f3e491..06bc9917f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -510,6 +510,8 @@ libcvc4_add_sources(
   theory/fp/theory_fp_type_rules.h
   theory/fp/type_enumerator.h
   theory/interrupted.h
+  theory/inference_manager_buffered.cpp
+  theory/inference_manager_buffered.h
   theory/logic_info.cpp
   theory/logic_info.h
   theory/model_manager.cpp
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
new file mode 100644
index 000000000..adbcc3033
--- /dev/null
+++ b/src/theory/inference_manager_buffered.cpp
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file inference_manager_buffered.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 A buffered inference manager
+ **/
+
+#include "theory/inference_manager_buffered.h"
+
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
+                                                   TheoryState& state,
+                                                   ProofNodeManager* pnm)
+    : TheoryInferenceManager(t, state, pnm)
+{
+}
+
+bool InferenceManagerBuffered::hasProcessed() const
+{
+  return d_theoryState.isInConflict() || !d_pendingLem.empty()
+         || !d_pendingFact.empty();
+}
+
+bool InferenceManagerBuffered::hasPendingFact() const
+{
+  return !d_pendingFact.empty();
+}
+
+bool InferenceManagerBuffered::hasPendingLemma() const
+{
+  return !d_pendingLem.empty();
+}
+
+void InferenceManagerBuffered::addPendingLemma(Node lem,
+                                               LemmaProperty p,
+                                               ProofGenerator* pg)
+{
+  d_pendingLem.push_back(std::make_shared<Lemma>(lem, p, pg));
+}
+
+void InferenceManagerBuffered::addPendingLemma(std::shared_ptr<Lemma> lemma)
+{
+  d_pendingLem.emplace_back(std::move(lemma));
+}
+
+void InferenceManagerBuffered::addPendingFact(Node fact, Node exp)
+{
+  Assert(fact.getKind() != AND && fact.getKind() != OR);
+  d_pendingFact.push_back(std::pair<Node, Node>(fact, exp));
+}
+
+void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
+{
+  // must ensure rewritten
+  lit = Rewriter::rewrite(lit);
+  d_pendingReqPhase[lit] = pol;
+}
+
+void InferenceManagerBuffered::doPendingFacts()
+{
+  size_t i = 0;
+  while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
+  {
+    std::pair<Node, Node>& pfact = d_pendingFact[i];
+    Node fact = pfact.first;
+    Node exp = pfact.second;
+    bool polarity = fact.getKind() != NOT;
+    TNode atom = polarity ? fact : fact[0];
+    // no double negation or conjunctive conclusions
+    Assert(atom.getKind() != NOT && atom.getKind() != AND);
+    assertInternalFact(atom, polarity, exp);
+    i++;
+  }
+  d_pendingFact.clear();
+}
+
+void InferenceManagerBuffered::doPendingLemmas()
+{
+  // process all the pending lemmas
+  for (const std::shared_ptr<Lemma>& plem : d_pendingLem)
+  {
+    if (!plem->notifySend())
+    {
+      // the lemma indicated that it should not be sent after all
+      continue;
+    }
+    Node lem = plem->d_node;
+    LemmaProperty p = plem->d_property;
+    ProofGenerator* pg = plem->d_pg;
+    Assert(!lem.isNull());
+    // send (trusted) lemma on the output channel with property p
+    trustedLemma(TrustNode::mkTrustLemma(lem, pg), p);
+  }
+  d_pendingLem.clear();
+}
+
+void InferenceManagerBuffered::doPendingPhaseRequirements()
+{
+  // process the pending require phase calls
+  for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+  {
+    d_out.requirePhase(prp.first, prp.second);
+  }
+  d_pendingReqPhase.clear();
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
new file mode 100644
index 000000000..bb46ef566
--- /dev/null
+++ b/src/theory/inference_manager_buffered.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file inference_manager_buffered.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 A buffered inference manager
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
+#define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "theory/theory_inference_manager.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * A lemma base class. This class is an abstract data structure for storing
+ * pending lemmas in the inference manager below.
+ */
+class Lemma
+{
+ public:
+  Lemma(Node n, LemmaProperty p, ProofGenerator* pg)
+      : d_node(n), d_property(p), d_pg(pg)
+  {
+  }
+  virtual ~Lemma() {}
+  /**
+   * Called just before this lemma is sent on the output channel. The purpose
+   * of this callback is to do any specific process of the lemma, e.g. take
+   * debug statistics, cache, etc.
+   *
+   * @return true if the lemma should be sent on the output channel.
+   */
+  virtual bool notifySend() { return true; }
+  /** 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;
+};
+
+/**
+ * The buffered inference manager.  This class implements standard methods
+ * for buffering facts, lemmas and phase requirements.
+ */
+class InferenceManagerBuffered : public TheoryInferenceManager
+{
+ public:
+  InferenceManagerBuffered(Theory& t,
+                           TheoryState& state,
+                           ProofNodeManager* pnm);
+  ~InferenceManagerBuffered() {}
+  /**
+   * Have we processed an inference during this call to check? In particular,
+   * this returns true if we have a pending fact or lemma, or have encountered
+   * a conflict.
+   */
+  bool hasProcessed() const;
+  /**
+   * Do we have a pending fact to add as an internal fact to the equality
+   * engine?
+   */
+  bool hasPendingFact() const;
+  /** Do we have a pending lemma to send on the output channel? */
+  bool hasPendingLemma() const;
+  /**
+   * Add pending lemma lem with property p, with proof generator pg. If
+   * non-null, pg must be able to provide a proof for lem for the remainder
+   * of the user context. Pending lemmas are sent to the output channel using
+   * doPendingLemmas.
+   */
+  void addPendingLemma(Node lem,
+                       LemmaProperty p = LemmaProperty::NONE,
+                       ProofGenerator* pg = nullptr);
+  /**
+   * Add pending lemma, where lemma can be a (derived) class of the
+   * above one. Pending lemmas are sent to the output channel using
+   * doPendingLemmas.
+   */
+  void addPendingLemma(std::shared_ptr<Lemma> lemma);
+  /**
+   * Add pending fact, which adds a fact on the pending fact queue. It must
+   * be the case that:
+   * (1) exp => fact is valid,
+   * (2) exp is a literal (or conjunction of literals) that holds in the
+   * equality engine of the theory.
+   *
+   * Pending facts are sent to the equality engine of this class using
+   * doPendingFacts.
+   */
+  void addPendingFact(Node fact, Node exp);
+  /** Add pending phase requirement
+   *
+   * This method is called to indicate this class should send a phase
+   * requirement request to the output channel for literal lit to be
+   * decided with polarity pol. The literal lit should be a SAT literal
+   * by the time that doPendingPhaseRequirements is called. Typically,
+   * lit is a literal that is a subformula of a pending lemma that is processed
+   * prior to sending the phase requirement.
+   */
+  void addPendingPhaseRequirement(Node lit, bool pol);
+  /** Do pending facts
+   *
+   * This method asserts pending facts (d_pendingFact) with explanations
+   * to the equality engine of the theory via calls
+   * to assertInternalFact.
+   *
+   * It terminates early if a conflict is encountered, for instance, by
+   * equality reasoning within the equality engine.
+   *
+   * Regardless of whether a conflict is encountered, the vector d_pendingFact
+   * is cleared after this call.
+   */
+  void doPendingFacts();
+  /** Do pending lemmas
+   *
+   * This method send all pending lemmas (d_pendingLem) on the output
+   * channel of the theory.
+   *
+   * Unlike doPendingFacts, this function will not terminate early if a conflict
+   * has already been encountered by the theory. The vector d_pendingLem is
+   * cleared after this call.
+   */
+  void doPendingLemmas();
+  /**
+   * Do pending phase requirements. Calls the output channel for all pending
+   * phase requirements and clears d_pendingReqPhase.
+   */
+  void doPendingPhaseRequirements();
+
+ protected:
+  /** A set of pending lemmas */
+  std::vector<std::shared_ptr<Lemma>> d_pendingLem;
+  /** A set of pending facts, paired with their explanations */
+  std::vector<std::pair<Node, Node>> d_pendingFact;
+  /** A map from literals to their pending phase requirement */
+  std::map<Node, bool> d_pendingReqPhase;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 54f33f6e7..b2da91e16 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -111,6 +111,17 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
                   << " mkTrustedConflictEqConstantMerge";
 }
 
+LemmaStatus TheoryInferenceManager::lemma(TNode lem, LemmaProperty p)
+{
+  return d_out.lemma(lem, p);
+}
+
+LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
+                                                 LemmaProperty p)
+{
+  return d_out.trustedLemma(tlem, p);
+}
+
 void TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
                                                 TNode fact)
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 914c87d19..e52afe124 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -105,6 +105,11 @@ class TheoryInferenceManager
    * been provided in a custom way.
    */
   void trustedConflict(TrustNode tconf);
+  /** Send lemma lem with property p on the output channel. */
+  LemmaStatus lemma(TNode lem, LemmaProperty p = LemmaProperty::NONE);
+  /** Send (trusted) lemma lem with property p on the output channel. */
+  LemmaStatus trustedLemma(const TrustNode& tlem,
+                           LemmaProperty p = LemmaProperty::NONE);
   /**
    * Assert internal fact. This is recommended method for asserting "internal"
    * facts into the equality engine of the theory. In particular, this method