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/sets | |
| 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/sets')
| -rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 5 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 62dedb35a..39b1fcca9 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -794,7 +794,8 @@ void CardinalityExtension::checkNormalForm(Node eqc, Trace("sets-nf") << "Actual Split : "; d_treg.debugPrintSet(r, "sets-nf"); Trace("sets-nf") << std::endl; - d_im.split(r.eqNode(emp_set), InferenceId::UNKNOWN, 1); + d_im.split( + r.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1); Assert(d_im.hasSent()); return; } @@ -866,7 +867,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, && !d_state.hasMembers(eqc)) { Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl; - d_im.split(eqc.eqNode(emp_set), InferenceId::UNKNOWN); + d_im.split(eqc.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY); success = false; } else diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 0546c7f95..65f5cedf5 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -349,7 +349,7 @@ void TheorySetsRels::check(Theory::Effort level) Assert(reasons.size() >= 1); sendInfer( new_membership, - InferenceId::UNKNOWN, + InferenceId::SETS_RELS_JOIN_IMAGE_UP, reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0]); break; } |