Add assertion to require inference ids (#8091)

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 791819f381b94697b1484f710887aac3efdd25e7..e1a5260e33c13d3cb5b2b46c716aa8809e96e4fc 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -196,6 +196,8 @@ const char* toString(InferenceId i)
       return "QUANTIFIERS_INST_E_MATCHING_HO";
     case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
       return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
+    case InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL:
+      return "QUANTIFIERS_INST_E_MATCHING_RELATIONAL";
     case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
       return "QUANTIFIERS_INST_CBQI_CONFLICT";
     case InferenceId::QUANTIFIERS_INST_CBQI_PROP:

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 4301e0d165db1a01e694aa7f475a048f9436bbc9..19dd1d3eac9710b77237d0340fbdb346f8e828e3 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -293,6 +293,8 @@ enum class InferenceId
   QUANTIFIERS_INST_E_MATCHING_HO,
   // E-matching based on variable triggers
   QUANTIFIERS_INST_E_MATCHING_VAR_GEN,
+  // E-matching based on relational triggers
+  QUANTIFIERS_INST_E_MATCHING_RELATIONAL,
   // conflicting instantiation from conflict-based instantiation
   QUANTIFIERS_INST_CBQI_CONFLICT,
   // propagating instantiation from conflict-based instantiation

diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
index db523683cd7efd92e09b09119dccd3b2a46af076..d415157ae881ced30cdc85648268dcc2e958b724 100644 (file)
--- a/src/theory/quantifiers/ematching/relational_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp
@@ -103,7 +103,8 @@ int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
     if (m.set(d_qstate, d_vindex, s))
     {
       Trace("relational-match-gen") << "...success" << std::endl;
-      int ret = continueNextMatch(q, m, InferenceId::UNKNOWN);
+      int ret = continueNextMatch(
+          q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL);
       if (ret > 0)
       {
         Trace("relational-match-gen") << "...returned " << ret << std::endl;

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index fda6d08812286a7c7aa2b702938b52b06da6af8c..b4add920ae27e496b8e39517dc76d3ab675ce1a2 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -143,6 +143,8 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 
 void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
+  Assert(id != InferenceId::UNKNOWN)
+      << "Must provide an inference id for conflict";
   d_conflictIdStats << id;
   resourceManager()->spendResource(id);
   Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
@@ -280,6 +282,8 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
       return false;
     }
   }
+  Assert(id != InferenceId::UNKNOWN)
+      << "Must provide an inference id for lemma";
   d_lemmaIdStats << id;
   resourceManager()->spendResource(id);
   Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
@@ -412,6 +416,8 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
                                                  const std::vector<Node>& args,
                                                  ProofGenerator* pg)
 {
+  Assert(iid != InferenceId::UNKNOWN)
+      << "Must provide an inference id for fact";
   d_factIdStats << iid;
   resourceManager()->spendResource(iid);
   // make the node corresponding to the explanation