Add asLemma flag to theory inference process (#5030)

This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.

It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.

9 files changed, 39 insertions, 17 deletions

diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index 58a552815..152d4647c 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -22,9 +22,9 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-bool NlLemma::process(TheoryInferenceManager* im)
+bool NlLemma::process(TheoryInferenceManager* im, bool asLemma)
 {
-  bool res = ArithLemma::process(im);
+  bool res = ArithLemma::process(im, asLemma);
   if (d_nlext != nullptr)
   {
     d_nlext->processSideEffect(*this);
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 1c0635f1f..0d3a6d547 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -57,7 +57,7 @@ class NlLemma : public ArithLemma
   }
   ~NlLemma() {}
 
-  bool process(TheoryInferenceManager* im) override;
+  bool process(TheoryInferenceManager* im, bool asLemma) override;
 
   /** secant points to add
    *
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 1faf71aa9..8daa68a27 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -66,7 +66,7 @@ bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
   return false;
 }
 
-bool DatatypesInference::process(TheoryInferenceManager* im)
+bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma)
 {
   // check to see if we have to communicate it to the rest of the system
   if (mustCommunicateFact(d_conc, d_exp))
@@ -89,7 +89,7 @@ bool DatatypesInference::process(TheoryInferenceManager* im)
 InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm)
+    : InferenceManagerBuffered(t, state, nullptr)
 {
 }
 
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 0dfdfb281..794d26430 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -55,7 +55,7 @@ class DatatypesInference : public SimpleTheoryInternalFact
    * Process this fact, possibly as a fact or as a lemma, depending on the
    * above method.
    */
-  bool process(TheoryInferenceManager* im) override;
+  bool process(TheoryInferenceManager* im, bool asLemma) override;
 };
 
 /**
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 3ba41a431..b0d092d74 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -86,7 +86,7 @@ void InferenceManagerBuffered::doPendingFacts()
   {
     // process this fact, which notice may enqueue more pending facts in this
     // loop.
-    d_pendingFact[i]->process(this);
+    d_pendingFact[i]->process(this, false);
     i++;
   }
   d_pendingFact.clear();
@@ -97,7 +97,7 @@ void InferenceManagerBuffered::doPendingLemmas()
   for (const std::unique_ptr<TheoryInference>& plem : d_pendingLem)
   {
     // process this lemma
-    plem->process(this);
+    plem->process(this, true);
   }
   d_pendingLem.clear();
 }
diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index 618dc640b..38e01eea5 100644
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -28,9 +28,10 @@ SimpleTheoryLemma::SimpleTheoryLemma(Node n,
 {
 }
 
-bool SimpleTheoryLemma::process(TheoryInferenceManager* im)
+bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma)
 {
   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), d_property);
 }
@@ -42,8 +43,9 @@ SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc,
 {
 }
 
-bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im)
+bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im, bool asLemma)
 {
+  Assert(!asLemma);
   bool polarity = d_conc.getKind() != NOT;
   TNode atom = polarity ? d_conc : d_conc[0];
   // no double negation or conjunctive conclusions
diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h
index 8d98051bf..6090b5a02 100644
--- a/src/theory/theory_inference.h
+++ b/src/theory/theory_inference.h
@@ -40,15 +40,26 @@ class TheoryInference
    * 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
+   * d_im->trustedLemma or d_im->assertInternalFact. 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.
    *
+   * @param im The inference manager to use
+   * @param asLemma Whether this inference is being processed as a lemma
+   * during doPendingLemmas (otherwise it is being processed in doPendingFacts).
+   * Typically, this method calls lemma or conflict when asLemma is
+   * true, and assertInternalFact when this flag is false, although this
+   * behavior is (intentionally) not strictly enforced. In particular, the
+   * choice to send a conflict, lemma or fact may depend on local state of the
+   * theory, which may change while the inference is pending. Hence the
+   * implementation of this method may choose to implement any call to the
+   * inference manager. This flag simply serves to track whether the inference
+   * initially was added a pending lemma or not.
    * @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;
+  virtual bool process(TheoryInferenceManager* im, bool asLemma) = 0;
 };
 
 /**
@@ -62,9 +73,10 @@ class SimpleTheoryLemma : public TheoryInference
   virtual ~SimpleTheoryLemma() {}
   /**
    * Send the lemma using inference manager im, return true if the lemma was
-   * sent.
+   * sent. It should be the case that asLemma = true or an assertion failure
+   * is thrown.
    */
-  virtual bool process(TheoryInferenceManager* im) override;
+  virtual bool process(TheoryInferenceManager* im, bool asLemma) override;
   /** The lemma to send */
   Node d_node;
   /** The lemma property (see OutputChannel::lemma) */
@@ -80,7 +92,7 @@ class SimpleTheoryLemma : public TheoryInference
 
 /**
  * A simple internal fact with no side effects. Makes a single call to
- * assertFactInternal in its process method.
+ * assertInternalFact in its process method.
  */
 class SimpleTheoryInternalFact : public TheoryInference
 {
@@ -89,9 +101,10 @@ class SimpleTheoryInternalFact : public TheoryInference
   virtual ~SimpleTheoryInternalFact() {}
   /**
    * Send the lemma using inference manager im, return true if the lemma was
-   * sent.
+   * sent. It should be the case that asLemma = false or an assertion failure
+   * is thrown.
    */
-  virtual bool process(TheoryInferenceManager* im) override;
+  virtual bool process(TheoryInferenceManager* im, bool asLemma) override;
   /** The lemma to send */
   Node d_conc;
   /** The explanation */
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 801d6a266..ff6f0ebc7 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -64,6 +64,11 @@ bool TheoryInferenceManager::hasSent() const
          || d_numCurrentFacts > 0;
 }
 
+eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
+{
+  return d_pfee.get();
+}
+
 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
 {
   if (!d_theoryState.isInConflict())
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 97baeaa40..496a7f0f1 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -97,6 +97,8 @@ class TheoryInferenceManager
    * since the last call to reset.
    */
   bool hasSent() const;
+  /** Get the underlying proof equality engine */
+  eq::ProofEqEngine* getProofEqEngine();
   //--------------------------------------- propagations
   /**
    * T-propagate literal lit, possibly encountered by equality engine,