diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-04 11:32:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-04 16:32:48 +0000 |
| commit | d78327addb22d1bb31836281235e988e45878fda (patch) | |
| tree | d336be153c0403d3d2755b7030e31bd4ba26242a /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | 5f89c684f95f16bdb5953fc543a36115093f1982 (diff) | |
Add missing inference identifiers (#6962)
The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 4c767012b..17eaad5c6 100644 --- 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() ){ |