Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)

This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index ecab1b92c7e45bf7dd2c2728a6271548c766ad1f..80217195f8256902785320ffc26c0f42d2ec56ad 100644 (file)
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom)
   // tn is of kind REWRITE, turn this into a LEMMA here
   TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
   // must preprocess
-  d_im.trustedLemma(tlem);
+  d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
   // mark the atom as reduced
   d_reduced[atom] = true;
   return true;

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index f2c805d38dab5566166020ffb96ace7d1c5b8c68..be29724447d07d05f156a2e25310c34bbd35f55a 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -53,9 +53,9 @@ bool InferenceManager::assertInference(TNode atom,
     std::vector<Node> args;
     // convert to proof rule application
     convert(id, fact, reason, children, args);
-    return assertInternalFact(atom, polarity, id, children, args);
+    return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args);
   }
-  return assertInternalFact(atom, polarity, reason);
+  return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason);
 }
 
 bool InferenceManager::arrayLemma(
@@ -72,11 +72,11 @@ bool InferenceManager::arrayLemma(
     convert(id, conc, exp, children, args);
     // make the trusted lemma based on the eager proof generator and send
     TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args);
-    return trustedLemma(tlem, p, doCache);
+    return trustedLemma(tlem, InferenceId::UNKNOWN, p, doCache);
   }
   // send lemma without proofs
   Node lem = nm->mkNode(IMPLIES, exp, conc);
-  return lemma(lem, p, doCache);
+  return lemma(lem, InferenceId::UNKNOWN, p, doCache);
 }
 
 void InferenceManager::convert(PfRule& id,

diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index c4e9570876749c54c88931a39fb7361d52186ed0..0655b6bbfd7f272e924ef16628fb27abbd6908ce 100644 (file)
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -37,7 +37,7 @@ bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
   if (asLemma)
   {
     TrustNode trustedLemma = TrustNode::mkTrustLemma(lemma, nullptr);
-    im->trustedLemma(trustedLemma);
+    im->trustedLemma(trustedLemma, getId());
   }
   else
   {
@@ -47,7 +47,7 @@ bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
   {
     Node n = pair.first.eqNode(pair.second);
     TrustNode trustedLemma = TrustNode::mkTrustLemma(n, nullptr);
-    im->trustedLemma(trustedLemma);
+    im->trustedLemma(trustedLemma, getId());
   }
 
   Trace("bags::InferInfo::process") << (*this) << std::endl;

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 7f38c61a2a6cb4ce0db47a518179fc7dd50235fd..f3adc4b21ff8dfd92680e1bc88d2bbf09305f9ba 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -416,9 +416,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
       lemmab << d_cnf->getNode(clause[i]);
     }
     Node lemma = lemmab;
-    d_bv->d_inferManager.lemma(lemma);
+    d_bv->d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
   } else {
-    d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]));
+    d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]), InferenceId::UNKNOWN);
   }
 }
 

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 68192e1d4daea2dea3bd24d75c62338d5a263fe2..ce8bc3645ac6df72deab795dc34ddf7eae75d156 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -97,7 +97,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     }
 
     NodeManager* nm = NodeManager::currentNM();
-    d_inferManager.conflict(nm->mkAnd(conflict));
+    d_inferManager.conflict(nm->mkAnd(conflict), InferenceId::UNKNOWN);
   }
 }
 

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index a19af44ac37871822eda93b6b0065963355cde4f..9c44e32f12c584c9c4e5eb56a1e1169fa9ec9d52 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -196,7 +196,7 @@ void BVSolverLazy::sendConflict()
   {
     Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
                        << d_conflictNode << std::endl;
-    d_inferManager.conflict(d_conflictNode);
+    d_inferManager.conflict(d_conflictNode, InferenceId::UNKNOWN);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
   }
@@ -287,11 +287,11 @@ void BVSolverLazy::check(Theory::Effort e)
     {
       if (assertions.size() == 1)
       {
-        d_inferManager.conflict(assertions[0]);
+        d_inferManager.conflict(assertions[0], InferenceId::UNKNOWN);
         return;
       }
       Node conflict = utils::mkAnd(assertions);
-      d_inferManager.conflict(conflict);
+      d_inferManager.conflict(conflict, InferenceId::UNKNOWN);
       return;
     }
     return;

diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 6885dbba4736e7e4ceac5a7d9fae7e1f7a1dd9b8..da5f1cbf88fa5cc51c48bc89bd950c99ffc867b8 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -203,7 +203,7 @@ class BVSolverLazy : public BVSolver
 
   void lemma(TNode node)
   {
-    d_inferManager.lemma(node);
+    d_inferManager.lemma(node, InferenceId::UNKNOWN);
     d_lemmasAdded = true;
   }
 

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 98fce24be86bab04ce0b0f90da7e97949423f5b4..c4a40404105e9f83e28040750e499d7e3dd25c47 100644 (file)
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -93,12 +93,12 @@ void BVSolverSimple::addBBLemma(TNode fact)
 
   if (d_epg == nullptr)
   {
-    d_inferManager.lemma(lemma);
+    d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
   }
   else
   {
     TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
-    d_inferManager.trustedLemma(tlem);
+    d_inferManager.trustedLemma(tlem, InferenceId::UNKNOWN);
   }
 }
 
@@ -123,13 +123,13 @@ bool BVSolverSimple::preNotifyFact(
 
     if (d_epg == nullptr)
     {
-      d_inferManager.lemma(lemma);
+      d_inferManager.lemma(lemma, InferenceId::UNKNOWN);
     }
     else
     {
       TrustNode tlem =
           d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
-      d_inferManager.trustedLemma(tlem);
+      d_inferManager.trustedLemma(tlem, InferenceId::UNKNOWN);
     }
 
     std::unordered_set<Node, NodeHashFunction> bv_atoms;

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index e2955306372841dab7a9f3083eba150f30191318..87cc0bc4de76d7b31b537924d02ae009e4602ef0 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -560,7 +560,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
                               nm->mkNode(kind::LT, n, max));
         Trace("bv-extf-lemma")
             << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->d_inferManager.lemma(lem);
+        d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
         sentLemma = true;
       }
     }
@@ -609,7 +609,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
           Trace("bv-extf-lemma")
               << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->d_inferManager.lemma(lem);
+          d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
           sentLemma = true;
         }
       }

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 7ecac6e3f58c4ce84dc0aebe791f5832db50d7b0..affa401d4497db93d624baf529179b97c4e108b7 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -87,7 +87,7 @@ void InferenceManager::sendDtLemma(Node lem,
     return;
   }
   // otherwise send as a normal lemma
-  if (lemma(lem, p, doCache))
+  if (lemma(lem, id, p, doCache))
   {
     d_inferenceLemmas << id;
   }
@@ -100,7 +100,7 @@ void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId
     Node exp = NodeManager::currentNM()->mkAnd(conf);
     prepareDtInference(d_false, exp, id, d_ipc.get());
   }
-  conflictExp(conf, d_ipc.get());
+  conflictExp(id, conf, d_ipc.get());
   d_inferenceConflicts << id;
 }
 
@@ -109,7 +109,7 @@ bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
   bool ret = false;
   for (const Node& lem : lemmas)
   {
-    if (lemma(lem))
+    if (lemma(lem, InferenceId::UNKNOWN))
     {
       ret = true;
     }
@@ -154,7 +154,7 @@ bool InferenceManager::processDtLemma(
   }
   // use trusted lemma
   TrustNode tlem = TrustNode::mkTrustLemma(lem, d_lemPg.get());
-  if (!trustedLemma(tlem))
+  if (!trustedLemma(tlem, id))
   {
     Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl;
     return false;
@@ -176,12 +176,12 @@ bool InferenceManager::processDtFact(Node conc, Node exp, InferenceId id)
     {
       expv.push_back(exp);
     }
-    assertInternalFact(atom, polarity, expv, d_ipc.get());
+    assertInternalFact(atom, polarity, id, expv, d_ipc.get());
   }
   else
   {
     // use version without proofs
-    assertInternalFact(atom, polarity, exp);
+    assertInternalFact(atom, polarity, id, exp);
   }
   d_inferenceFacts << id;
   return true;

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 064a4b2d16a29d0e6fab5b51aec93dded49b9494..153f7c85060cb1a5f3c58a02facbe4b4f713a67e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -252,7 +252,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     assumptions.push_back(assumption);
                     Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
                     Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
-                    d_im.lemma(lemma);
+                    d_im.lemma(lemma, InferenceId::UNKNOWN);
                   }
                 }
               }else{
@@ -318,7 +318,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     NodeBuilder<> nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
-                    d_im.lemma(lemma);
+                    d_im.lemma(lemma, InferenceId::UNKNOWN);
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
@@ -1415,7 +1415,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
       Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
-      d_im.lemma(a);
+      d_im.lemma(a, InferenceId::UNKNOWN);
       Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
     }
     d_singleton_lemma[index][tn] = a;

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 299ef7239306fe7e99fc0899c148194d8844a75e..a38a92b6a68d40a826a55f4b39cbe7883af88c29 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1787,7 +1787,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c
                            << std::endl;
-        d_im.conflictExp(ant, nullptr);
+        d_im.conflictExp(InferenceId::UNKNOWN, ant, nullptr);
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
                            << " by " << c << std::endl;

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index fe4a5875a358d72a96cd847d3bd94e2f27748e7e..15b7f64dcbf9b6adb7953cdd2b56d284f3896a0d 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -57,7 +57,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     if (fact == d_false)
     {
       Trace("sets-lemma") << "Conflict : " << exp << std::endl;
-      conflict(exp);
+      conflict(exp, InferenceId::UNKNOWN);
       return true;
     }
     return false;
@@ -90,7 +90,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
       || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
   {
     // send to equality engine
-    if (assertInternalFact(atom, polarity, exp))
+    if (assertInternalFact(atom, polarity, InferenceId::UNKNOWN, exp))
     {
       // return true if this wasn't redundant
       return true;
@@ -164,7 +164,7 @@ void InferenceManager::split(Node n, int reqPol)
   n = Rewriter::rewrite(n);
   Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
   // send the lemma
-  lemma(lem);
+  lemma(lem, InferenceId::UNKNOWN);
   Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
   if (reqPol != 0)
   {

diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index 1e780721d7497ac6a1f8ac69096d75b0dc859494..975581dfa908964f0a96baf52499e714f736b349 100644 (file)
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -53,13 +53,13 @@ Node TermRegistry::getProxy(Node n)
   d_proxy_to_term[k] = n;
   Node eq = k.eqNode(n);
   Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
-  d_im.lemma(eq, LemmaProperty::NONE, false);
+  d_im.lemma(eq, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
   if (nk == SINGLETON)
   {
     Node slem = nm->mkNode(MEMBER, n[0], k);
     Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
                         << std::endl;
-    d_im.lemma(slem, LemmaProperty::NONE, false);
+    d_im.lemma(slem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
   }
   return k;
 }
@@ -104,7 +104,7 @@ Node TermRegistry::getUnivSet(TypeNode tn)
       Node ulem = nm->mkNode(SUBSET, n1, n2);
       Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
                           << std::endl;
-      d_im.lemma(ulem, LemmaProperty::NONE, false);
+      d_im.lemma(ulem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
     }
   }
   d_univset[tn] = n;

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 0d1206dec9087ff48015f10eec17b5ed4a081528..867c87c5978e2dca0922658113f971564e6b85db 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -104,7 +104,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
             // infer equality between elements of singleton
             Node exp = s1.eqNode(s2);
             Node eq = s1[0].eqNode(s2[0]);
-            d_im.assertInternalFact(eq, true, exp);
+            d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, exp);
           }
           else
           {
@@ -137,7 +137,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
       Assert(facts.size() == 1);
       Trace("sets-prop") << "Propagate eq-mem conflict : " << facts[0]
                          << std::endl;
-      d_im.conflict(facts[0]);
+      d_im.conflict(facts[0], InferenceId::UNKNOWN);
       return;
     }
     for (const Node& f : facts)
@@ -145,7 +145,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
       Assert(f.getKind() == kind::IMPLIES);
       Trace("sets-prop") << "Propagate eq-mem eq inference : " << f[0] << " => "
                          << f[1] << std::endl;
-      d_im.assertInternalFact(f[1], true, f[0]);
+      d_im.assertInternalFact(f[1], true, InferenceId::UNKNOWN, f[0]);
     }
   }
 }
@@ -764,7 +764,7 @@ void TheorySetsPrivate::checkReduceComprehensions()
         nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
     Trace("sets-comprehension")
         << "Comprehension reduction: " << lem << std::endl;
-    d_im.lemma(lem);
+    d_im.lemma(lem, InferenceId::UNKNOWN);
   }
 }
 
@@ -818,14 +818,14 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
             Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
             Node eq = s[0].eqNode(atom[0]);
             // triggers an internal inference
-            d_im.assertInternalFact(eq, true, pexp);
+            d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, pexp);
           }
         }
         else
         {
           Trace("sets-prop")
               << "Propagate mem-eq conflict : " << pexp << std::endl;
-          d_im.conflict(pexp);
+          d_im.conflict(pexp, InferenceId::UNKNOWN);
         }
       }
     }

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a348585e74ac38fecccc13eab98815a6a7633bbb..8c487d7c1c4aad20bad0b1d753e522a530c031e4 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -299,7 +299,7 @@ void InferenceManager::processConflict(const InferInfo& ii)
   Trace("strings-assert") << "(assert (not " << tconf.getNode()
                           << ")) ; conflict " << ii.getId() << std::endl;
   // send the trusted conflict
-  trustedConflict(tconf);
+  trustedConflict(tconf, ii.getId());
 }
 
 bool InferenceManager::processFact(InferInfo& ii)
@@ -342,13 +342,13 @@ bool InferenceManager::processFact(InferInfo& ii)
       // current SAT context
       d_ipc->notifyFact(ii);
       // now, assert the internal fact with d_ipc as proof generator
-      curRet = assertInternalFact(atom, polarity, exp, d_ipc.get());
+      curRet = assertInternalFact(atom, polarity, ii.getId(), exp, d_ipc.get());
     }
     else
     {
       Node cexp = utils::mkAnd(exp);
       // without proof generator
-      curRet = assertInternalFact(atom, polarity, cexp);
+      curRet = assertInternalFact(atom, polarity, ii.getId(), cexp);
     }
     ret = ret || curRet;
     // may be in conflict
@@ -420,7 +420,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   ++(d_statistics.d_lemmasInfer);
 
   // call the trusted lemma, without caching
-  return trustedLemma(tlem, p, false);
+  return trustedLemma(tlem, ii.getId(), p, false);
 }
 
 }  // namespace strings

diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp
index f64b88daa6cdde851690ef3c9cef62797b3f9846..8ccbb7e1f416e995820c18a6783741b3a475b47f 100644 (file)
--- a/src/theory/theory_inference.cpp
+++ b/src/theory/theory_inference.cpp
@@ -34,7 +34,7 @@ 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);
+  return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), getId(), d_property);
 }
 
 SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
@@ -54,11 +54,11 @@ bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im, bool asLemma)
   Assert(atom.getKind() != NOT && atom.getKind() != AND);
   if (d_pg != nullptr)
   {
-    im->assertInternalFact(atom, polarity, {d_exp}, d_pg);
+    im->assertInternalFact(atom, polarity, getId(), {d_exp}, d_pg);
   }
   else
   {
-    im->assertInternalFact(atom, polarity, d_exp);
+    im->assertInternalFact(atom, polarity, getId(), d_exp);
   }
   return true;
 }

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 58a8b86a47b6504225317c235255a3e3cf830ea9..a56d616d9253eb2aec05472deca43a8b95893026 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -85,7 +85,7 @@ void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
   }
 }
 
-void TheoryInferenceManager::conflict(TNode conf)
+void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
@@ -95,7 +95,7 @@ void TheoryInferenceManager::conflict(TNode conf)
   }
 }
 
-void TheoryInferenceManager::trustedConflict(TrustNode tconf)
+void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
@@ -104,16 +104,17 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf)
   }
 }
 
-void TheoryInferenceManager::conflictExp(PfRule id,
+void TheoryInferenceManager::conflictExp(InferenceId id,
+                                         PfRule pfr,
                                          const std::vector<Node>& exp,
                                          const std::vector<Node>& args)
 {
   if (!d_theoryState.isInConflict())
   {
     // make the trust node
-    TrustNode tconf = mkConflictExp(id, exp, args);
+    TrustNode tconf = mkConflictExp(pfr, exp, args);
     // send it on the output channel
-    trustedConflict(tconf);
+    trustedConflict(tconf, id);
   }
 }
 
@@ -131,7 +132,8 @@ TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
   return TrustNode::mkTrustConflict(conf, nullptr);
 }
 
-void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
+void TheoryInferenceManager::conflictExp(InferenceId id,
+                                         const std::vector<Node>& exp,
                                          ProofGenerator* pg)
 {
   if (!d_theoryState.isInConflict())
@@ -139,7 +141,7 @@ void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
     // make the trust node
     TrustNode tconf = mkConflictExp(exp, pg);
     // send it on the output channel
-    trustedConflict(tconf);
+    trustedConflict(tconf, id);
   }
 }
 
@@ -207,13 +209,17 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
                   << " mkTrustedConflictEqConstantMerge";
 }
 
-bool TheoryInferenceManager::lemma(TNode lem, LemmaProperty p, bool doCache)
+bool TheoryInferenceManager::lemma(TNode lem,
+                                   InferenceId id,
+                                   LemmaProperty p,
+                                   bool doCache)
 {
   TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
-  return trustedLemma(tlem, p, doCache);
+  return trustedLemma(tlem, id, p, doCache);
 }
 
 bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
+                                          InferenceId id,
                                           LemmaProperty p,
                                           bool doCache)
 {
@@ -230,7 +236,8 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
 }
 
 bool TheoryInferenceManager::lemmaExp(Node conc,
-                                      PfRule id,
+                                      InferenceId id,
+                                      PfRule pfr,
                                       const std::vector<Node>& exp,
                                       const std::vector<Node>& noExplain,
                                       const std::vector<Node>& args,
@@ -238,9 +245,9 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
                                       bool doCache)
 {
   // make the trust node
-  TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args);
+  TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
   // send it on the output channel
-  return trustedLemma(trn, p, doCache);
+  return trustedLemma(trn, id, p, doCache);
 }
 
 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
@@ -261,6 +268,7 @@ TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 }
 
 bool TheoryInferenceManager::lemmaExp(Node conc,
+                                      InferenceId id,
                                       const std::vector<Node>& exp,
                                       const std::vector<Node>& noExplain,
                                       ProofGenerator* pg,
@@ -270,7 +278,7 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
   // make the trust node
   TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
   // send it on the output channel
-  return trustedLemma(trn, p, doCache);
+  return trustedLemma(trn, id, p, doCache);
 }
 
 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
@@ -305,23 +313,28 @@ bool TheoryInferenceManager::hasSentLemma() const
   return d_numCurrentLemmas != 0;
 }
 
-bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
+bool TheoryInferenceManager::assertInternalFact(TNode atom,
+                                                bool pol,
+                                                InferenceId id,
+                                                TNode exp)
 {
   return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 }
 
 bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
-                                                PfRule id,
+                                                InferenceId id,
+                                                PfRule pfr,
                                                 const std::vector<Node>& exp,
                                                 const std::vector<Node>& args)
 {
-  Assert(id != PfRule::UNKNOWN);
-  return processInternalFact(atom, pol, id, exp, args, nullptr);
+  Assert(pfr != PfRule::UNKNOWN);
+  return processInternalFact(atom, pol, pfr, exp, args, nullptr);
 }
 
 bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
+                                                InferenceId id,
                                                 const std::vector<Node>& exp,
                                                 ProofGenerator* pg)
 {

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 324ceb5e1c39e62bee2a46edbb86f34de43ba761..7a125789b9176d7e91f64662fe270ea4fd9d57fe 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -132,12 +132,12 @@ class TheoryInferenceManager
    * Raise conflict conf (of any form), without proofs. This method should
    * only be called if there is not yet proof support in the given theory.
    */
-  void conflict(TNode conf);
+  void conflict(TNode conf, InferenceId id);
   /**
    * Raise trusted conflict tconf (of any form) where a proof generator has
    * been provided (as part of the trust node) in a custom way.
    */
-  void trustedConflict(TrustNode tconf);
+  void trustedConflict(TrustNode tconf, InferenceId id);
   /**
    * Explain and send conflict from contradictory facts. This method is called
    * when the proof rule id with premises exp and arguments args concludes
@@ -145,7 +145,8 @@ class TheoryInferenceManager
    * equality engine's explanation of literals in exp, with the proof equality
    * engine as the proof generator (if it exists).
    */
-  void conflictExp(PfRule id,
+  void conflictExp(InferenceId id,
+                   PfRule pfr,
                    const std::vector<Node>& exp,
                    const std::vector<Node>& args);
   /**
@@ -153,7 +154,7 @@ class TheoryInferenceManager
    * the responsibility of the caller to subsequently call trustedConflict with
    * the returned trust node.
    */
-  TrustNode mkConflictExp(PfRule id,
+  TrustNode mkConflictExp(PfRule pfr,
                           const std::vector<Node>& exp,
                           const std::vector<Node>& args);
   /**
@@ -164,7 +165,9 @@ class TheoryInferenceManager
    * engine as the proof generator (if it exists), where pg provides the
    * final step(s) of this proof during this call.
    */
-  void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+  void conflictExp(InferenceId id,
+                   const std::vector<Node>& exp,
+                   ProofGenerator* pg);
   /**
    * Make the trust node corresponding to the conflict of the above form. It is
    * the responsibility of the caller to subsequently call trustedConflict with
@@ -182,6 +185,7 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool trustedLemma(const TrustNode& tlem,
+                    InferenceId id,
                     LemmaProperty p = LemmaProperty::NONE,
                     bool doCache = true);
   /**
@@ -189,6 +193,7 @@ class TheoryInferenceManager
    * a node instead of a trust node.
    */
   bool lemma(TNode lem,
+             InferenceId id,
              LemmaProperty p = LemmaProperty::NONE,
              bool doCache = true);
   /**
@@ -215,7 +220,8 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool lemmaExp(Node conc,
-                PfRule id,
+                InferenceId id,
+                PfRule pfr,
                 const std::vector<Node>& exp,
                 const std::vector<Node>& noExplain,
                 const std::vector<Node>& args,
@@ -246,6 +252,7 @@ class TheoryInferenceManager
    * @return true if the lemma was sent on the output channel.
    */
   bool lemmaExp(Node conc,
+                InferenceId id,
                 const std::vector<Node>& exp,
                 const std::vector<Node>& noExplain,
                 ProofGenerator* pg = nullptr,
@@ -286,7 +293,7 @@ class TheoryInferenceManager
    * @return true if the fact was processed, i.e. it was asserted to the
    * equality engine or preNotifyFact returned true.
    */
-  bool assertInternalFact(TNode atom, bool pol, TNode exp);
+  bool assertInternalFact(TNode atom, bool pol, InferenceId id, TNode exp);
   /**
    * Assert internal fact, with a proof step justification. Notice that if
    * proofs are not enabled in this inference manager, then this asserts
@@ -302,7 +309,8 @@ class TheoryInferenceManager
    */
   bool assertInternalFact(TNode atom,
                           bool pol,
-                          PfRule id,
+                          InferenceId id,
+                          PfRule pfr,
                           const std::vector<Node>& exp,
                           const std::vector<Node>& args);
   /**
@@ -320,6 +328,7 @@ class TheoryInferenceManager
    */
   bool assertInternalFact(TNode atom,
                           bool pol,
+                          InferenceId id,
                           const std::vector<Node>& exp,
                           ProofGenerator* pg);
   /** The number of internal facts we have added since the last call to reset */
@@ -327,7 +336,7 @@ class TheoryInferenceManager
   /** Have we added a internal fact since the last call to reset? */
   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.
    */

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index bd69245b8cc25928e76ba2bef96c0f4592839b5d..697a828a4dfe7a1b2d922b53d41c5208577055dd 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r)
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
     // send lemma, with caching
-    if (d_im.lemma(lem))
+    if (d_im.lemma(lem, InferenceId::UNKNOWN))
     {
       Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
       //tell the sat solver to explore the equals branch first
@@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique)
   eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
   Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
   // send lemma, with caching
-  if (d_im.lemma(lem))
+  if (d_im.lemma(lem, InferenceId::UNKNOWN))
   {
     Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
     ++(d_thss->d_statistics.d_clique_lemmas);
@@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() {
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
                                                       getCardinalityLiteral( d_maxNegCard.get() ).negate() );
     Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
-    d_im.conflict(lem);
+    d_im.conflict(lem, InferenceId::UNKNOWN);
   }
 }
 
@@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall()
         Node lem = NodeManager::currentNM()->mkNode(
             OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
         Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
-        d_im.lemma(lem, LemmaProperty::NONE, false);
+        d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
         return false;
       }
     }
@@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
           eqv_lit = lit.eqNode( eqv_lit );
           Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-          d_im.lemma(eqv_lit, LemmaProperty::NONE, false);
+          d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
           d_card_assertions_eqv_lemma[lit] = true;
         }
       }
@@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level)
                     Node eq = Rewriter::rewrite( a.eqNode( b ) );
                     Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                     Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
-                    d_im.lemma(lem, LemmaProperty::NONE, false);
+                    d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
                     d_im.requirePhase(eq, true);
                     type_proc[tn] = true;
                     break;
@@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality()
                              << " : " << cf << std::endl;
         Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
                                 << " : " << cf << std::endl;
-        d_im.conflict(cf);
+        d_im.conflict(cf, InferenceId::UNKNOWN);
         return;
       }
     }
@@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality()
                            << std::endl;
       Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
                               << std::endl;
-      d_im.conflict(cf);
+      d_im.conflict(cf, InferenceId::UNKNOWN);
     }
   }
 }

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 66bcbc76f41bc2bccd13a63fcf5956c79c5c011b..55e2500af0b626f8493a953484e52e2b139846b8 100644 (file)
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                          << std::endl;
-    d_im.lemma(lem);
+    d_im.lemma(lem, InferenceId::UNKNOWN);
     return 1;
   }
   return 0;
@@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       Trace("uf-ho-lemma")
           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
           << std::endl;
-      d_im.lemma(lem);
+      d_im.lemma(lem, InferenceId::UNKNOWN);
       d_uf_std_skolem[f] = new_f;
     }
     else
@@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
               Node lem = nm->mkNode(OR, deq.negate(), eq);
               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                              << std::endl;
-              d_im.lemma(lem);
+              d_im.lemma(lem, InferenceId::UNKNOWN);
               return 1;
             }
           }
@@ -284,7 +284,7 @@ unsigned HoExtension::applyAppCompletion(TNode n)
     Node eq = n.eqNode(ret);
     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                          << std::endl;
-    d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n});
+    d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n});
     return 1;
   }
   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
@@ -441,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
       Node eq = n.eqNode(hn);
       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                      << std::endl;
-      d_im.lemma(eq);
+      d_im.lemma(eq, InferenceId::UNKNOWN);
       return false;
     }
   }

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6fdc969a4cce7aea94fd6172471e1bedde3a3a47..c8cfe295e3a2ea1a7230d61d9759d86ed8bb398a 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -315,7 +315,7 @@ void TheoryUF::presolve() {
         ++i) {
       Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
       // no proof generator provided
-      d_im.lemma(*i);
+      d_im.lemma(*i, InferenceId::UNKNOWN);
     }
   }
   if( d_thss ){