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.

diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index 58a5528157c7eef60c862482e91a7a0deb695afd..152d4647c3ae3836c494560295a0de3e1147b03e 100644 (file)
--- 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 1c0635f1ffdf90d542eca425ea7debd8be692e13..0d3a6d5478c540145f814bdcc101e29e986c994f 100644 (file)
--- 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 1faf71aa9c379ef47ea4b298dd6e9a19a32e6068..8daa68a27e7a4da0af032663da2a5bf56f955a2a 100644 (file)
--- 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 0dfdfb2814e3e68a4f7b42dc511d2fa187f21cd8..794d26430b54bd127f8e9a1429f9f4e2e10c32a1 100644 (file)
--- 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 3ba41a4318f8d8ed09d3769c1707ea115fcf3cee..b0d092d741e9ecb3c250b3a072ceecdc65608509 100644 (file)
--- 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 618dc640bf27e2a88117b6009f635f1407c431b6..38e01eea5f5ecaadd056b0d9892d75a8df3be6bb 100644 (file)
--- 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 8d98051bf56423cf8208a0c7e09007120cbb8001..6090b5a020de6277117ce90448d51e6f7017a462 100644 (file)
--- 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 801d6a26659d24a4a60b56d8ce20fdff4d6c223a..ff6f0ebc7ec80585f2c28fa8b6673985d27837b6 100644 (file)
--- 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 97baeaa408954502ece653412cd4b79538b04b49..496a7f0f1fb78e0576632d22d99ba57f92769119 100644 (file)
--- 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,