Minor updates to theory inference manager (#5004)

These updates are inspired by the current inference manager for sets.

4 files changed, 55 insertions, 37 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 78b6d81c2..5253414a9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -170,7 +170,7 @@ void TheoryDatatypes::postCheck(Effort level)
     return;
   }
   else if (level == EFFORT_FULL && !d_state.isInConflict()
-           && !d_im.hasAddedLemma() && !d_valuation.needCheck())
+           && !d_im.hasSentLemma() && !d_valuation.needCheck())
   {
     //check for cycles
     Assert(!d_im.hasPendingFact());
@@ -180,11 +180,11 @@ void TheoryDatatypes::postCheck(Effort level)
       checkCycles();
       Trace("datatypes-proc") << "...finish check cycles" << std::endl;
       d_im.process();
-      if (d_state.isInConflict() || d_im.hasAddedLemma())
+      if (d_state.isInConflict() || d_im.hasSentLemma())
       {
         return;
       }
-    } while (d_im.hasAddedFact());
+    } while (d_im.hasSentFact());
 
     //check for splits
     Trace("datatypes-debug") << "Check for splits " << endl;
@@ -329,7 +329,7 @@ void TheoryDatatypes::postCheck(Effort level)
         }
         ++eqcs_i;
       }
-      if (d_im.hasAddedLemma())
+      if (d_im.hasSentLemma())
       {
         // clear pending facts: we added a lemma, so internal inferences are
         // no longer necessary
@@ -342,11 +342,11 @@ void TheoryDatatypes::postCheck(Effort level)
         Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
         d_im.process();
       }
-    } while (!d_state.isInConflict() && !d_im.hasAddedLemma()
-             && d_im.hasAddedFact());
+    } while (!d_state.isInConflict() && !d_im.hasSentLemma()
+             && d_im.hasSentFact());
     Trace("datatypes-debug")
         << "Finished, conflict=" << d_state.isInConflict()
-        << ", lemmas=" << d_im.hasAddedLemma() << std::endl;
+        << ", lemmas=" << d_im.hasSentLemma() << std::endl;
     if (!d_state.isInConflict())
     {
       Trace("dt-model-debug") << std::endl;
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 8d7dd2abc..8a7713121 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -76,8 +76,7 @@ void InferenceManagerBuffered::addPendingFact(
 
 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
 {
-  // must ensure rewritten
-  lit = Rewriter::rewrite(lit);
+  // it is the responsibility of the caller to ensure lit is rewritten
   d_pendingReqPhase[lit] = pol;
 }
 
@@ -109,7 +108,7 @@ 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);
+    requirePhase(prp.first, prp.second);
   }
   d_pendingReqPhase.clear();
 }
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 3abe530f1..9405a8162 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -221,41 +221,41 @@ bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
   return d_lemmasSent.find(lem) != d_lemmasSent.end();
 }
 
-uint32_t TheoryInferenceManager::numAddedLemmas() const
+uint32_t TheoryInferenceManager::numSentLemmas() const
 {
   return d_numCurrentLemmas;
 }
 
-bool TheoryInferenceManager::hasAddedLemma() const
+bool TheoryInferenceManager::hasSentLemma() const
 {
   return d_numCurrentLemmas != 0;
 }
 
-void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
+bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
 {
-  processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
+  return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 }
 
-void TheoryInferenceManager::assertInternalFact(TNode atom,
+bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
                                                 PfRule id,
                                                 const std::vector<Node>& exp,
                                                 const std::vector<Node>& args)
 {
   Assert(id != PfRule::UNKNOWN);
-  processInternalFact(atom, pol, id, exp, args, nullptr);
+  return processInternalFact(atom, pol, id, exp, args, nullptr);
 }
 
-void TheoryInferenceManager::assertInternalFact(TNode atom,
+bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
                                                 const std::vector<Node>& exp,
                                                 ProofGenerator* pg)
 {
   Assert(pg != nullptr);
-  processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
+  return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
 }
 
-void TheoryInferenceManager::processInternalFact(TNode atom,
+bool TheoryInferenceManager::processInternalFact(TNode atom,
                                                  bool pol,
                                                  PfRule id,
                                                  const std::vector<Node>& exp,
@@ -267,8 +267,9 @@ void TheoryInferenceManager::processInternalFact(TNode atom,
   // call the pre-notify fact method with preReg = false, isInternal = true
   if (d_theory.preNotifyFact(atom, pol, expn, false, true))
   {
-    // handled in a theory-specific way that doesn't require equality engine
-    return;
+    // Handled in a theory-specific way that doesn't require equality engine,
+    // notice we return true, indicating that the fact was processed.
+    return true;
   }
   Assert(d_ee != nullptr);
   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
@@ -276,15 +277,16 @@ void TheoryInferenceManager::processInternalFact(TNode atom,
   d_numCurrentFacts++;
   // Now, assert the fact. How to do so depends on whether proofs are enabled.
   // If no proof production, or no proof rule was given
+  bool ret = false;
   if (d_pfee == nullptr || id == PfRule::UNKNOWN)
   {
     if (atom.getKind() == kind::EQUAL)
     {
-      d_ee->assertEquality(atom, pol, expn);
+      ret = d_ee->assertEquality(atom, pol, expn);
     }
     else
     {
-      d_ee->assertPredicate(atom, pol, expn);
+      ret = d_ee->assertPredicate(atom, pol, expn);
     }
     // Must reference count the equality and its explanation, which is not done
     // by the equality engine. Notice that we do *not* need to do this for
@@ -304,18 +306,19 @@ void TheoryInferenceManager::processInternalFact(TNode atom,
     if (pg != nullptr)
     {
       // use the proof generator interface
-      d_pfee->assertFact(lit, expn, pg);
+      ret = d_pfee->assertFact(lit, expn, pg);
     }
     else
     {
       // use the explict proof step interface
-      d_pfee->assertFact(lit, id, expn, args);
+      ret = d_pfee->assertFact(lit, id, expn, args);
     }
   }
   // call the notify fact method with isInternal = true
   d_theory.notifyFact(atom, pol, expn, true);
   Trace("infer-manager")
       << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
+  return ret;
 }
 
 void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
@@ -361,12 +364,12 @@ Node TheoryInferenceManager::mkExplainPartial(
   return NodeManager::currentNM()->mkAnd(assumps);
 }
 
-uint32_t TheoryInferenceManager::numAddedFacts() const
+uint32_t TheoryInferenceManager::numSentFacts() const
 {
   return d_numCurrentFacts;
 }
 
-bool TheoryInferenceManager::hasAddedFact() const
+bool TheoryInferenceManager::hasSentFact() const
 {
   return d_numCurrentFacts != 0;
 }
@@ -381,5 +384,10 @@ bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
   return true;
 }
 
+void TheoryInferenceManager::requirePhase(TNode n, bool pol)
+{
+  return d_out.requirePhase(n, pol);
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 2ddcd0985..7e5ef6dec 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -214,9 +214,9 @@ class TheoryInferenceManager
    */
   virtual bool hasCachedLemma(TNode lem, LemmaProperty p);
   /** The number of lemmas we have sent since the last call to reset */
-  uint32_t numAddedLemmas() const;
+  uint32_t numSentLemmas() const;
   /** Have we added a lemma since the last call to reset? */
-  bool hasAddedLemma() const;
+  bool hasSentLemma() const;
   //--------------------------------------- internal facts
   /**
    * Assert internal fact. This is recommended method for asserting "internal"
@@ -229,8 +229,10 @@ class TheoryInferenceManager
    * @param atom The atom of the fact to assert
    * @param pol Its polarity
    * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.
+   * @return true if the fact was processed, i.e. it was asserted to the
+   * equality engine or preNotifyFact returned true.
    */
-  void assertInternalFact(TNode atom, bool pol, TNode exp);
+  bool assertInternalFact(TNode atom, bool pol, TNode exp);
   /**
    * Assert internal fact, with a proof step justification. Notice that if
    * proofs are not enabled in this inference manager, then this asserts
@@ -241,8 +243,10 @@ class TheoryInferenceManager
    * @param id The proof rule identifier of the proof step
    * @param exp Its explanation, interpreted as a conjunction
    * @param args The arguments of the proof step
+   * @return true if the fact was processed, i.e. it was asserted to the
+   * equality engine or preNotifyFact returned true.
    */
-  void assertInternalFact(TNode atom,
+  bool assertInternalFact(TNode atom,
                           bool pol,
                           PfRule id,
                           const std::vector<Node>& exp,
@@ -257,22 +261,29 @@ class TheoryInferenceManager
    * @param pg The proof generator for this step. If non-null, pg must be able
    * to provide a proof concluding (~) atom from free asumptions in exp in
    * the remainder of the current SAT context.
+   * @return true if the fact was processed, i.e. it was asserted to the
+   * equality engine or preNotifyFact returned true.
    */
-  void assertInternalFact(TNode atom,
+  bool assertInternalFact(TNode atom,
                           bool pol,
                           const std::vector<Node>& exp,
                           ProofGenerator* pg);
   /** The number of internal facts we have added since the last call to reset */
-  uint32_t numAddedFacts() const;
+  uint32_t numSentFacts() const;
   /** Have we added a internal fact since the last call to reset? */
-  bool hasAddedFact() const;
-
+  bool hasSentFact() const;
+  //--------------------------------------- phase requirements
+  /** 
+   * Set that literal n has SAT phase requirement pol, that is, it should be
+   * decided with polarity pol, for details see OutputChannel::requirePhase.
+   */
+  void requirePhase(TNode n, bool pol);
  protected:
   /**
    * Process internal fact. This is a common helper method for the
-   * assertInternalFact variants above.
+   * assertInternalFact variants above. Returns true if the fact was processed.
    */
-  void processInternalFact(TNode atom,
+  bool processInternalFact(TNode atom,
                            bool pol,
                            PfRule id,
                            const std::vector<Node>& exp,