Add InferenceId to buffered inference manager (#5911)

This PR collects the InferenceId in the InferenceManagerBuffered class.

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 153f7c85060cb1a5f3c58a02facbe4b4f713a67e..dc7bdc369aa5bb93f1624a29444a274bc0ce27cb 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -850,7 +850,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
-      d_im.addPendingLemma(eq);
+      d_im.addPendingLemma(eq, InferenceId::UNKNOWN);
       return k;
     }else{
       return (*it).second;
@@ -1473,7 +1473,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
     Node lem = nm->mkNode(LEQ, d_zero, n);
     Trace("datatypes-infer")
         << "DtInfer : size geq zero : " << lem << std::endl;
-    d_im.addPendingLemma(lem);
+    d_im.addPendingLemma(lem, InferenceId::UNKNOWN);
   }
   else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
   {
@@ -1498,7 +1498,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
                                           : nm->mkNode(OR, children));
     }
     Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
-    d_im.addPendingLemma(lem);
+    d_im.addPendingLemma(lem, InferenceId::UNKNOWN);
   }
 }
 

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index e5f6ae4e48849f4b307b929b9dddbd313294cab2..6789043b1b5cd5aed30d0294bd2fd495746bf0a2 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -45,6 +45,7 @@ bool InferenceManagerBuffered::hasPendingLemma() const
 }
 
 bool InferenceManagerBuffered::addPendingLemma(Node lem,
+                                               InferenceId id,
                                                LemmaProperty p,
                                                ProofGenerator* pg,
                                                bool checkCache)
@@ -59,7 +60,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem,
     }
   }
   // make the simple theory lemma
-  d_pendingLem.emplace_back(new SimpleTheoryLemma(InferenceId::UNKNOWN, lem, p, pg));
+  d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
   return true;
 }
 
@@ -70,12 +71,13 @@ void InferenceManagerBuffered::addPendingLemma(
 }
 
 void InferenceManagerBuffered::addPendingFact(Node conc,
+                                              InferenceId id,
                                               Node exp,
                                               ProofGenerator* pg)
 {
   // make a simple theory internal fact
   Assert(conc.getKind() != AND && conc.getKind() != OR);
-  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(InferenceId::UNKNOWN, conc, exp, pg));
+  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
 }
 
 void InferenceManagerBuffered::addPendingFact(

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 28014ce8e9f78ecfb04523a83f166caa0dfe0693..f9cddadd39e1de18dd7428d5e8f61e610598a5e8 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -54,6 +54,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * doPendingLemmas.
    *
    * @param lem The lemma to send
+   * @param id The identifier of the inference
    * @param p The property of the lemma
    * @param pg The proof generator which can provide a proof for lem
    * @param checkCache Whether we want to check that the lemma is already in
@@ -62,6 +63,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * false if the lemma is already cached.
    */
   bool addPendingLemma(Node lem,
+                       InferenceId id,
                        LemmaProperty p = LemmaProperty::NONE,
                        ProofGenerator* pg = nullptr,
                        bool checkCache = true);
@@ -79,8 +81,12 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    *
    * Pending facts are sent to the equality engine of this class using
    * doPendingFacts.
+   * @param conc The conclustion
+   * @param id The identifier of the inference
+   * @param exp The explanation in the equality engine of the theory
+   * @param pg The proof generator which can provide a proof for conc
    */
-  void addPendingFact(Node conc, Node exp, ProofGenerator* pg = nullptr);
+  void addPendingFact(Node conc, InferenceId id, Node exp, ProofGenerator* pg = nullptr);
   /**
    * Add pending fact, where fact can be a (derived) class of the
    * theory inference base class.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 208933456955c08324f272d4e70d7259185e3573..c37054fdd4e6b327ba544d4b2d76ea29eee2e760 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -394,7 +394,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   {
     Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
                          << std::endl;
-    d_qim.addPendingLemma(auxLems[i]);
+    d_qim.addPendingLemma(auxLems[i], InferenceId::UNKNOWN);
   }
 }
 
@@ -495,7 +495,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
 
 bool InstStrategyCegqi::addPendingLemma(Node lem) const
 {
-  return d_qim.addPendingLemma(lem);
+  return d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
 }
 
 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
@@ -536,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
       // add lemmas to process
       for (const Node& lem : lems)
       {
-        d_qim.addPendingLemma(lem);
+        d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
       }
       // don't need to process this, since it has been reduced
       return true;

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 57c5533a994b8823a03a16a6de85be1e2bcd87a3..96bb9a9f7f9a269dcc035616ee28458ab8bf07e9 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -349,7 +349,7 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
       if( !lem.empty() ){
         for (const Node& l : lem)
         {
-          d_qim.addPendingLemma(l);
+          d_qim.addPendingLemma(l, InferenceId::UNKNOWN);
         }
         d_hasAddedLemma = true;
         return false;
@@ -934,7 +934,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
               d_eq_conjectures[rhs].push_back( lhs );
 
               Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );
-              d_qim.addPendingLemma(lem);
+              d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
               d_qim.addPendingPhaseRequirement(rsg, false);
               addedLemmas++;
               if( (int)addedLemmas>=options::conjectureGenPerRound() ){

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 7cc1074aaf61e4bcaae59bb0ad6f00c76e7a6c6f..0ab2988d286b5256af2c0faf2624d00854a35c7f 100644 (file)
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -498,7 +498,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
           {
             Node u = tdb->getHoTypeMatchPredicate(tn);
             Node au = nm->mkNode(kind::APPLY_UF, u, f);
-            if (d_qim.addPendingLemma(au))
+            if (d_qim.addPendingLemma(au, InferenceId::UNKNOWN))
             {
               // this forces f to be a first-class member of the quantifier-free
               // equality engine, which in turn forces the quantifier-free

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 881133432d4686a36268439f027acb1783d413ab..90d8de1282534e9543369a1fd81248e507c5367a 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -632,7 +632,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
         << "Make partially specified user pattern: " << std::endl;
     Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
     Node lem = nm->mkNode(OR, q.negate(), qq);
-    d_qim.addPendingLemma(lem);
+    d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
     return;
   }
   unsigned tindex;

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 58d94a11dad1c8f5939236e1855cdc3b9dfb3850..3bc5ded16f4724515b909f56b20ca05663f65983 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -123,7 +123,7 @@ uint64_t Trigger::addInstantiations()
         Node eq = k.eqNode(gt);
         Trace("trigger-gt-lemma")
             << "Trigger: ground term purify lemma: " << eq << std::endl;
-        d_qim.addPendingLemma(eq);
+        d_qim.addPendingLemma(eq, InferenceId::UNKNOWN);
         gtAddedLemmas++;
       }
     }

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 0a0d155f9e937f3ae48d4c0018023c179ea81fcf..5a0407f1f88095b841cff83c4256d6e91b53ae5a 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -294,7 +294,7 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
     {
       Trace("bound-int-lemma")
           << "*** bound int : proxy lemma : " << prangeLem << std::endl;
-      d_qim.addPendingLemma(prangeLem);
+      d_qim.addPendingLemma(prangeLem, InferenceId::UNKNOWN);
       addedLemma = true;
     }
   }

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 9588bba7fd242e01b80b9ed74c7729efc1abab54..b4fed5b1310f320a9e3a8ab9f0843101033e1e37 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -324,11 +324,11 @@ bool Instantiate::addInstantiation(
   if (hasProof)
   {
     // use proof generator
-    addedLem = d_qim.addPendingLemma(lem, LemmaProperty::NONE, d_pfInst.get());
+    addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, d_pfInst.get());
   }
   else
   {
-    addedLem = d_qim.addPendingLemma(lem);
+    addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
   }
 
   if (!addedLem)

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index f782ae7ef62cd11a221e8c56eebaea86f3ff0dd9..a0b7808363c5e66a7f72a41eaf34f59616da7973 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -198,7 +198,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
   for (const Node& lem : lemmas)
   {
     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
-    d_qim.addPendingLemma(lem);
+    d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
   }
   Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
 }

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 7bae9218447af390eb80f9ec761ea5d65c2cff3d..59edd3070395d50483be6dec7d6d98c6a30a070e 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -723,7 +723,7 @@ bool SynthConjecture::doRefine()
   {
     Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
                          << std::endl;
-    bool res = d_qim.addPendingLemma(lem);
+    bool res = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
     if (res)
     {
       ++(d_stats.d_cegqi_lemmas_refine);

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index c12f387bc0def3199f83cce3940e74ed6b400731..e4c8c6cec2be760904e6551a2e6859e161bd389f 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -224,7 +224,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
-      if (d_qim.addPendingLemma(lem))
+      if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
       {
         ++(d_statistics.d_cegqi_lemmas_ce);
         addedLemma = true;

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index f6827d1c43e4ce1f31c2dbf5799b16e5951da0b4..e59b788b62442c8d6915dcfe65e0a9e43f979108 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -309,7 +309,7 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
   for (const Node& lem : lemmas)
   {
     Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
-    added_lemma |= d_qim.addPendingLemma(lem);
+    added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
   }
   return added_lemma;
 }
@@ -545,7 +545,7 @@ void SygusInst::addCeLemma(Node q)
   if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
 
   Node lem = d_ce_lemmas[q];
-  d_qim.addPendingLemma(lem);
+  d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
   d_ce_lemma_added.insert(q);
   Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
 }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b83cdf3e54d9341459929692d86e67da378d05b0..61a62a820ffd32d028a8f0a027271f0b319337a5 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -435,7 +435,7 @@ void TermDb::computeUfTerms( TNode f ) {
             }
             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
           }
-          d_qim.addPendingLemma(lem);
+          d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return;
@@ -1044,7 +1044,7 @@ bool TermDb::reset( Theory::Effort effort ){
           // equality is sent out as a lemma here.
           Trace("term-db-lemma")
               << "Purify equality lemma: " << eq << std::endl;
-          d_qim.addPendingLemma(eq);
+          d_qim.addPendingLemma(eq, InferenceId::UNKNOWN);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return false;

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index a38a92b6a68d40a826a55f4b39cbe7883af88c29..8782bfe348427995be73c5d0455c397357b70bae 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1782,7 +1782,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
     if( infer && conc!=d_false ){
       Node ant_n = NodeManager::currentNM()->mkAnd(ant);
       Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
-      d_im.addPendingFact(conc, ant_n);
+      d_im.addPendingFact(conc, InferenceId::UNKNOWN, ant_n);
     }else{
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c
@@ -1793,7 +1793,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
                            << " by " << c << std::endl;
         TrustNode trn = d_im.mkLemmaExp(conc, ant, {});
         d_im.addPendingLemma(
-            trn.getNode(), LemmaProperty::NONE, trn.getGenerator());
+            trn.getNode(), InferenceId::UNKNOWN, LemmaProperty::NONE, trn.getGenerator());
       }
     }
   }

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 15b7f64dcbf9b6adb7953cdd2b56d284f3896a0d..2629e2cbd8b8310e3de4783b8c7f232da1b3f285 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -46,7 +46,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     {
       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
     }
-    addPendingLemma(lem);
+    addPendingLemma(lem, InferenceId::UNKNOWN);
     return true;
   }
   Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
@@ -104,7 +104,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     {
       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
     }
-    addPendingLemma(lem);
+    addPendingLemma(lem, InferenceId::UNKNOWN);
     return true;
   }
   return false;