diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 14:42:50 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 07:42:50 -0600 |
commit | 2d6de44a51fed47a625ae73181efbcc3dac0c751 (patch) | |
tree | 50ebd370468514d15b71a1d5f7d8993c24116fc0 /src/theory/quantifiers/ematching | |
parent | a1a2d9389730ed46ab246865e320108db07c30ff (diff) |
Add InferenceId to buffered inference manager (#5911)
This PR collects the InferenceId in the InferenceManagerBuffered class.
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 7cc1074aa..0ab2988d2 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -498,7 +498,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); - if (d_qim.addPendingLemma(au)) + if (d_qim.addPendingLemma(au, InferenceId::UNKNOWN)) { // this forces f to be a first-class member of the quantifier-free // equality engine, which in turn forces the quantifier-free diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 881133432..90d8de128 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -632,7 +632,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { << "Make partially specified user pattern: " << std::endl; Trace("auto-gen-trigger-partial") << " " << qq << std::endl; Node lem = nm->mkNode(OR, q.negate(), qq); - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); return; } unsigned tindex; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 58d94a11d..3bc5ded16 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -123,7 +123,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); + d_qim.addPendingLemma(eq, InferenceId::UNKNOWN); gtAddedLemmas++; } } |