From 53feec296fd26985c4a6d5ead19ff9ef53c5ce7f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Feb 2022 14:09:03 -0600 Subject: [PATCH] Add assertion to require inference ids (#8091) --- src/theory/inference_id.cpp | 2 ++ src/theory/inference_id.h | 2 ++ .../quantifiers/ematching/relational_match_generator.cpp | 3 ++- src/theory/theory_inference_manager.cpp | 6 ++++++ 4 files changed, 12 insertions(+), 1 deletion(-) 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& 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 -- 2.30.2