Add missing inference identifiers (#6962)

The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 053b91d906e9f9e398f13decd4ed685880235fbf..c85376e6b3caf008a59af7755684414baed168f8 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1613,7 +1613,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
     Debug("arith::eq") << "negation has proof" << endl;
     Debug("arith::eq") << constraint << endl;
     Debug("arith::eq") << negation << endl;
-    raiseConflict(negation, InferenceId::UNKNOWN);
+    raiseConflict(negation, InferenceId::ARITH_CONF_FACT_QUEUE);
     return NullConstraint;
   }else{
     return constraint;

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 7a764feba503bf11494833ebc606e16e6055d5d0..6c9c162abb0d5edfa2a73b0e4a7df29608948b23 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1676,7 +1676,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     }
     d_im.assertInference(selConst.eqNode(defValue),
                          true,
-                         InferenceId::UNKNOWN,
+                         InferenceId::ARRAYS_CONST_ARRAY_DEFAULT,
                          d_true,
                          PfRule::ARRAYS_TRUST);
   }
@@ -1892,8 +1892,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       {
         preRegisterTermInternal(aj2);
       }
-      d_im.assertInference(
-          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(aj.eqNode(aj2),
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
@@ -1904,8 +1907,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(
-          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(bj.eqNode(bj2),
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
     }
     if (aj2 == bj2) {
       return;
@@ -1923,14 +1929,22 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq1,
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
       return;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq2,
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
       return;
     }
 
@@ -2009,8 +2023,11 @@ bool TheoryArrays::dischargeLemmas()
       {
         preRegisterTermInternal(aj2);
       }
-      d_im.assertInference(
-          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(aj.eqNode(aj2),
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
@@ -2021,8 +2038,11 @@ bool TheoryArrays::dischargeLemmas()
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(
-          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(bj.eqNode(bj2),
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
     }
     if (aj2 == bj2) {
       continue;
@@ -2040,14 +2060,22 @@ bool TheoryArrays::dischargeLemmas()
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq1,
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
       continue;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq2,
+                           true,
+                           InferenceId::ARRAYS_EQ_TAUTOLOGY,
+                           d_true,
+                           PfRule::MACRO_SR_PRED_INTRO);
       continue;
     }
 

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index c0700c06ef1657e421463ffbdcc04e85afbb6e3d..8ed30ea9851a363ff353f8ba0db497f64ad41d03 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -34,6 +34,7 @@ const char* toString(InferenceId i)
     case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER";
     case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX";
     case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX";
+    case InferenceId::ARITH_CONF_FACT_QUEUE: return "ARITH_CONF_FACT_QUEUE";
     case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ";
     case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL";
     case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR";
@@ -96,6 +97,9 @@ const char* toString(InferenceId i)
     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
     case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
     case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA";
+    case InferenceId::ARRAYS_CONST_ARRAY_DEFAULT:
+      return "ARRAYS_CONST_ARRAY_DEFAULT";
+    case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY";
 
     case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
     case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
@@ -221,14 +225,34 @@ const char* toString(InferenceId i)
       return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
     case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
       return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB";
+    case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN:
+      return "QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN";
     case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT";
+    case InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT:
+      return "QUANTIFIERS_CONJ_GEN_SPLIT";
+    case InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM:
+      return "QUANTIFIERS_CONJ_GEN_GT_ENUM";
     case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
     case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
       return "QUANTIFIERS_REDUCE_ALPHA_EQ";
     case InferenceId::QUANTIFIERS_HO_MATCH_PRED:
       return "QUANTIFIERS_HO_MATCH_PRED";
+    case InferenceId::QUANTIFIERS_HO_PURIFY: return "QUANTIFIERS_HO_PURIFY";
     case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE:
       return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE";
+    case InferenceId::QUANTIFIERS_GT_PURIFY: return "QUANTIFIERS_GT_PURIFY";
+    case InferenceId::QUANTIFIERS_TDB_DEQ_CONG:
+      return "QUANTIFIERS_TDB_DEQ_CONG";
 
     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
@@ -283,6 +307,7 @@ const char* toString(InferenceId i)
     case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE";
     case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN:
       return "SETS_RELS_JOIN_IMAGE_DOWN";
+    case InferenceId::SETS_RELS_JOIN_IMAGE_UP: return "SETS_RELS_JOIN_IMAGE_UP";
     case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
     case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
     case InferenceId::SETS_RELS_PRODUCE_COMPOSE:

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index b3be59c5c754c635909c8e94f7aa60ad349701a8..b2bfe36579ae650d76c00aaf98e8ac280f6a6313 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -61,6 +61,8 @@ enum class InferenceId
   ARITH_CONF_SIMPLEX,
   // conflict from sum-of-infeasibility simplex
   ARITH_CONF_SOI_SIMPLEX,
+  // conflict when getting constraint from fact queue
+  ARITH_CONF_FACT_QUEUE,
   // introduces split on a disequality
   ARITH_SPLIT_DEQ,
   // tighten integer inequalities to ceiling
@@ -156,6 +158,10 @@ enum class InferenceId
   ARRAYS_READ_OVER_WRITE,
   ARRAYS_READ_OVER_WRITE_1,
   ARRAYS_READ_OVER_WRITE_CONTRA,
+  // (= (select (as const (Array T1 T2) x) y) x)
+  ARRAYS_CONST_ARRAY_DEFAULT,
+  // an internally inferred tautological equality
+  ARRAYS_EQ_TAUTOLOGY,
   // ---------------------------------- end arrays theory
 
   // ---------------------------------- bags theory
@@ -334,9 +340,26 @@ enum class InferenceId
   QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
   // ~Q where Q is a PBE conjecture with conflicting examples
   QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
+  // unif+pi symmetry breaking between multiple enumerators
+  QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB,
+  // unif+pi separation lemma
+  QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION,
+  // unif+pi lemma for fairness of size of enumerators
+  QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE,
+  // unif+pi lemma for removing redundant operators
+  QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS,
+  // symmetry breaking for enumerators
+  QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB,
+  // constraining terms to be in the domain of output
+  QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN,
   //-------------------- dynamic splitting
   // a dynamic split from quantifiers
   QUANTIFIERS_DSPLIT,
+  //-------------------- induction / conjecture generation
+  // a split on a conjecture for inductive theorem proving
+  QUANTIFIERS_CONJ_GEN_SPLIT,
+  // enumeration of ground terms for inductive theorem proving
+  QUANTIFIERS_CONJ_GEN_GT_ENUM,
   //-------------------- miscellaneous
   // skolemization
   QUANTIFIERS_SKOLEMIZE,
@@ -344,8 +367,16 @@ enum class InferenceId
   QUANTIFIERS_REDUCE_ALPHA_EQ,
   // a higher-order match predicate lemma
   QUANTIFIERS_HO_MATCH_PRED,
+  // purification of non-variable higher-order function
+  QUANTIFIERS_HO_PURIFY,
   // reduction of quantifiers that don't have triggers that cover all variables
   QUANTIFIERS_PARTIAL_TRIGGER_REDUCE,
+  // a purification lemma for a ground term appearing in a quantified formula,
+  // used to ensure E-matching has equality information for that term
+  QUANTIFIERS_GT_PURIFY,
+  // when term indexing discovers disequal congruent terms in the master
+  // equality engine
+  QUANTIFIERS_TDB_DEQ_CONG,
   //-------------------------------------- end quantifiers theory
 
   // ---------------------------------- sep theory
@@ -425,6 +456,7 @@ enum class InferenceId
   SETS_RELS_IDENTITY_UP,
   SETS_RELS_JOIN_COMPOSE,
   SETS_RELS_JOIN_IMAGE_DOWN,
+  SETS_RELS_JOIN_IMAGE_UP,
   SETS_RELS_JOIN_SPLIT_1,
   SETS_RELS_JOIN_SPLIT_2,
   SETS_RELS_PRODUCE_COMPOSE,

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 4c767012b3a24426e45b428cbc8eb69dd60ec318..17eaad5c648b04ec40b1c8e66eee9fad94c133e1 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -351,7 +351,7 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
       if( !lem.empty() ){
         for (const Node& l : lem)
         {
-          d_qim.addPendingLemma(l, InferenceId::UNKNOWN);
+          d_qim.addPendingLemma(l, InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM);
         }
         d_hasAddedLemma = true;
         return false;
@@ -936,7 +936,8 @@ 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, InferenceId::UNKNOWN);
+              d_qim.addPendingLemma(lem,
+                                    InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT);
               d_qim.addPendingPhaseRequirement(rsg, false);
               addedLemmas++;
               if( (int)addedLemmas>=options::conjectureGenPerRound() ){

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 5291259787c0ffb3685fcb0eab4258c39419b23b..3e32496290e47d7f4f229d3f41a8d8534c1df9e6 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -145,7 +145,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, InferenceId::UNKNOWN);
+        d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY);
         gtAddedLemmas++;
       }
     }

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 544bdcc5cddd01226c8cbd1b97aca87a14f04652..1e77087b71c8e57bd87887d220be13c9528e1c21 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -219,7 +219,8 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
                     << "CegisUnif::lemma, inter-unif-enumerator "
                        "symmetry breaking lemma : "
                     << slem << "\n";
-                d_qim.lemma(slem, InferenceId::UNKNOWN);
+                d_qim.lemma(
+                    slem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB);
                 addedUnifEnumSymBreakLemma = true;
                 break;
               }
@@ -367,7 +368,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   {
     Trace("cegis-unif-lemma")
         << "CegisUnif::lemma, separation lemma : " << lem << "\n";
-    d_qim.lemma(lem, InferenceId::UNKNOWN);
+    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION);
   }
   Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
   return false;
@@ -510,7 +511,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       //   G_uq_i => size(ve) >= log_2( i-1 )
       // In other words, if we use i conditions, then we allow terms in our
       // solution whose size is at most log_2(i-1).
-      d_qim.lemma(fair_lemma, InferenceId::UNKNOWN);
+      d_qim.lemma(fair_lemma, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE);
     }
   }
 
@@ -619,7 +620,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
     Trace("cegis-unif-enum-lemma")
         << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
         << sym_break_red_ops << "\n";
-    d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN);
+    d_qim.lemma(sym_break_red_ops,
+                InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS);
   }
   // symmetry breaking between enumerators
   if (!si.d_enums[index].empty() && index == 0)
@@ -630,7 +632,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
     Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
     Trace("cegis-unif-enum-lemma")
         << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
-    d_qim.lemma(sym_break, InferenceId::UNKNOWN);
+    d_qim.lemma(sym_break, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB);
   }
   // register the enumerator
   si.d_enums[index].push_back(e);
@@ -686,7 +688,7 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
   Node lem = NodeManager::currentNM()->mkNode(OR, disj);
   Trace("cegis-unif-enum-lemma")
       << "CegisUnifEnum::lemma, domain:" << lem << "\n";
-  d_qim.lemma(lem, InferenceId::UNKNOWN);
+  d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN);
 }
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 523b84e6590d61ba3690c0035cde205430c923a2..655fd2df7e3cdc2991f773cada807e30f6b9c077 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -434,7 +434,7 @@ void TermDb::computeUfTerms( TNode f ) {
             }
             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
           }
-          d_qim->addPendingLemma(lem, InferenceId::UNKNOWN);
+          d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return;
@@ -1047,7 +1047,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, InferenceId::UNKNOWN);
+          d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return false;

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 62dedb35abca4359ce1802401aff61609effd7a7..39b1fcca9da7189ff334acb1f6420d85fc65ef09 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -794,7 +794,8 @@ void CardinalityExtension::checkNormalForm(Node eqc,
               Trace("sets-nf") << "Actual Split : ";
               d_treg.debugPrintSet(r, "sets-nf");
               Trace("sets-nf") << std::endl;
-              d_im.split(r.eqNode(emp_set), InferenceId::UNKNOWN, 1);
+              d_im.split(
+                  r.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1);
               Assert(d_im.hasSent());
               return;
             }
@@ -866,7 +867,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
         && !d_state.hasMembers(eqc))
     {
       Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
-      d_im.split(eqc.eqNode(emp_set), InferenceId::UNKNOWN);
+      d_im.split(eqc.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY);
       success = false;
     }
     else

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 0546c7f9531fe9146a99b616f62e543888f5bee8..65f5cedf577fc3a05019533e265549638ac80486 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -349,7 +349,7 @@ void TheorySetsRels::check(Theory::Effort level)
               Assert(reasons.size() >= 1);
               sendInfer(
                   new_membership,
-                  InferenceId::UNKNOWN,
+                  InferenceId::SETS_RELS_JOIN_IMAGE_UP,
                   reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0]);
               break;
             }