From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Feb 2022 20:09:03 +0000 (-0600)
Subject: Add assertion to require inference ids (#8091)
X-Git-Tag: cvc5-1.0.0~428
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53feec296fd26985c4a6d5ead19ff9ef53c5ce7f;p=cvc5.git

Add assertion to require inference ids (#8091)
---

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 791819f38..e1a5260e3 100644
--- 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 4301e0d16..19dd1d3ea 100644
--- 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 db523683c..d415157ae 100644
--- 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 fda6d0881..b4add920a 100644
--- 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