From d78327addb22d1bb31836281235e988e45878fda Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Aug 2021 11:32:48 -0500 Subject: [PATCH] Add missing inference identifiers (#6962) The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR. --- src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 54 ++++++++++++++----- src/theory/inference_id.cpp | 25 +++++++++ src/theory/inference_id.h | 32 +++++++++++ .../quantifiers/conjecture_generator.cpp | 5 +- src/theory/quantifiers/ematching/trigger.cpp | 2 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 14 ++--- src/theory/quantifiers/term_database.cpp | 4 +- src/theory/sets/cardinality_extension.cpp | 5 +- src/theory/sets/theory_sets_rels.cpp | 2 +- 10 files changed, 117 insertions(+), 28 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 053b91d90..c85376e6b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1613,7 +1613,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion) Debug("arith::eq") << "negation has proof" << endl; Debug("arith::eq") << constraint << endl; Debug("arith::eq") << negation << endl; - raiseConflict(negation, InferenceId::UNKNOWN); + raiseConflict(negation, InferenceId::ARITH_CONF_FACT_QUEUE); return NullConstraint; }else{ return constraint; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 7a764feba..6c9c162ab 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1676,7 +1676,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) } d_im.assertInference(selConst.eqNode(defValue), true, - InferenceId::UNKNOWN, + InferenceId::ARRAYS_CONST_ARRAY_DEFAULT, d_true, PfRule::ARRAYS_TRUST); } @@ -1892,8 +1892,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(aj2); } - d_im.assertInference( - aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(aj.eqNode(aj2), + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -1904,8 +1907,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(bj2); } - d_im.assertInference( - bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(bj.eqNode(bj2), + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { return; @@ -1923,14 +1929,22 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) { preRegisterTermInternal(bj2); } - d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq1, + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); return; } Node eq2 = i.eqNode(j); Node eq2_r = Rewriter::rewrite(eq2); if (eq2_r == d_true) { - d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq2, + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); return; } @@ -2009,8 +2023,11 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(aj2); } - d_im.assertInference( - aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(aj.eqNode(aj2), + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { @@ -2021,8 +2038,11 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(bj2); } - d_im.assertInference( - bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(bj.eqNode(bj2), + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); } if (aj2 == bj2) { continue; @@ -2040,14 +2060,22 @@ bool TheoryArrays::dischargeLemmas() { preRegisterTermInternal(bj2); } - d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq1, + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); continue; } Node eq2 = i.eqNode(j); Node eq2_r = Rewriter::rewrite(eq2); if (eq2_r == d_true) { - d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO); + d_im.assertInference(eq2, + true, + InferenceId::ARRAYS_EQ_TAUTOLOGY, + d_true, + PfRule::MACRO_SR_PRED_INTRO); continue; } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c0700c06e..8ed30ea98 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -34,6 +34,7 @@ const char* toString(InferenceId i) case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER"; case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX"; case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX"; + case InferenceId::ARITH_CONF_FACT_QUEUE: return "ARITH_CONF_FACT_QUEUE"; case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ"; case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL"; case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR"; @@ -96,6 +97,9 @@ const char* toString(InferenceId i) case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA"; + case InferenceId::ARRAYS_CONST_ARRAY_DEFAULT: + return "ARRAYS_CONST_ARRAY_DEFAULT"; + case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY"; case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT"; case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT"; @@ -221,14 +225,34 @@ const char* toString(InferenceId i) return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT"; case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA: return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB: + return "QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION: + return "QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE: + return "QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS: + return "QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB: + return "QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB"; + case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN: + return "QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN"; case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT"; + case InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT: + return "QUANTIFIERS_CONJ_GEN_SPLIT"; + case InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM: + return "QUANTIFIERS_CONJ_GEN_GT_ENUM"; case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE"; case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ: return "QUANTIFIERS_REDUCE_ALPHA_EQ"; case InferenceId::QUANTIFIERS_HO_MATCH_PRED: return "QUANTIFIERS_HO_MATCH_PRED"; + case InferenceId::QUANTIFIERS_HO_PURIFY: return "QUANTIFIERS_HO_PURIFY"; case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE: return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE"; + case InferenceId::QUANTIFIERS_GT_PURIFY: return "QUANTIFIERS_GT_PURIFY"; + case InferenceId::QUANTIFIERS_TDB_DEQ_CONG: + return "QUANTIFIERS_TDB_DEQ_CONG"; case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; @@ -283,6 +307,7 @@ const char* toString(InferenceId i) case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE"; case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN: return "SETS_RELS_JOIN_IMAGE_DOWN"; + case InferenceId::SETS_RELS_JOIN_IMAGE_UP: return "SETS_RELS_JOIN_IMAGE_UP"; case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1"; case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2"; case InferenceId::SETS_RELS_PRODUCE_COMPOSE: diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index b3be59c5c..b2bfe3657 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -61,6 +61,8 @@ enum class InferenceId ARITH_CONF_SIMPLEX, // conflict from sum-of-infeasibility simplex ARITH_CONF_SOI_SIMPLEX, + // conflict when getting constraint from fact queue + ARITH_CONF_FACT_QUEUE, // introduces split on a disequality ARITH_SPLIT_DEQ, // tighten integer inequalities to ceiling @@ -156,6 +158,10 @@ enum class InferenceId ARRAYS_READ_OVER_WRITE, ARRAYS_READ_OVER_WRITE_1, ARRAYS_READ_OVER_WRITE_CONTRA, + // (= (select (as const (Array T1 T2) x) y) x) + ARRAYS_CONST_ARRAY_DEFAULT, + // an internally inferred tautological equality + ARRAYS_EQ_TAUTOLOGY, // ---------------------------------- end arrays theory // ---------------------------------- bags theory @@ -334,9 +340,26 @@ enum class InferenceId QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT, // ~Q where Q is a PBE conjecture with conflicting examples QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA, + // unif+pi symmetry breaking between multiple enumerators + QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB, + // unif+pi separation lemma + QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION, + // unif+pi lemma for fairness of size of enumerators + QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE, + // unif+pi lemma for removing redundant operators + QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS, + // symmetry breaking for enumerators + QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB, + // constraining terms to be in the domain of output + QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN, //-------------------- dynamic splitting // a dynamic split from quantifiers QUANTIFIERS_DSPLIT, + //-------------------- induction / conjecture generation + // a split on a conjecture for inductive theorem proving + QUANTIFIERS_CONJ_GEN_SPLIT, + // enumeration of ground terms for inductive theorem proving + QUANTIFIERS_CONJ_GEN_GT_ENUM, //-------------------- miscellaneous // skolemization QUANTIFIERS_SKOLEMIZE, @@ -344,8 +367,16 @@ enum class InferenceId QUANTIFIERS_REDUCE_ALPHA_EQ, // a higher-order match predicate lemma QUANTIFIERS_HO_MATCH_PRED, + // purification of non-variable higher-order function + QUANTIFIERS_HO_PURIFY, // reduction of quantifiers that don't have triggers that cover all variables QUANTIFIERS_PARTIAL_TRIGGER_REDUCE, + // a purification lemma for a ground term appearing in a quantified formula, + // used to ensure E-matching has equality information for that term + QUANTIFIERS_GT_PURIFY, + // when term indexing discovers disequal congruent terms in the master + // equality engine + QUANTIFIERS_TDB_DEQ_CONG, //-------------------------------------- end quantifiers theory // ---------------------------------- sep theory @@ -425,6 +456,7 @@ enum class InferenceId SETS_RELS_IDENTITY_UP, SETS_RELS_JOIN_COMPOSE, SETS_RELS_JOIN_IMAGE_DOWN, + SETS_RELS_JOIN_IMAGE_UP, SETS_RELS_JOIN_SPLIT_1, SETS_RELS_JOIN_SPLIT_2, SETS_RELS_PRODUCE_COMPOSE, 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() ){ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 529125978..3e3249629 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -145,7 +145,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, InferenceId::UNKNOWN); + d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY); gtAddedLemmas++; } } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 544bdcc5c..1e77087b7 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -219,7 +219,8 @@ bool CegisUnif::getEnumValues(const std::vector& enums, << "CegisUnif::lemma, inter-unif-enumerator " "symmetry breaking lemma : " << slem << "\n"; - d_qim.lemma(slem, InferenceId::UNKNOWN); + d_qim.lemma( + slem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB); addedUnifEnumSymBreakLemma = true; break; } @@ -367,7 +368,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, { Trace("cegis-unif-lemma") << "CegisUnif::lemma, separation lemma : " << lem << "\n"; - d_qim.lemma(lem, InferenceId::UNKNOWN); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION); } Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n"; return false; @@ -510,7 +511,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) // G_uq_i => size(ve) >= log_2( i-1 ) // In other words, if we use i conditions, then we allow terms in our // solution whose size is at most log_2(i-1). - d_qim.lemma(fair_lemma, InferenceId::UNKNOWN); + d_qim.lemma(fair_lemma, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE); } } @@ -619,7 +620,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : " << sym_break_red_ops << "\n"; - d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN); + d_qim.lemma(sym_break_red_ops, + InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS); } // symmetry breaking between enumerators if (!si.d_enums[index].empty() && index == 0) @@ -630,7 +632,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; - d_qim.lemma(sym_break, InferenceId::UNKNOWN); + d_qim.lemma(sym_break, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB); } // register the enumerator si.d_enums[index].push_back(e); @@ -686,7 +688,7 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, Node lem = NodeManager::currentNM()->mkNode(OR, disj); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem << "\n"; - d_qim.lemma(lem, InferenceId::UNKNOWN); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN); } } // namespace quantifiers diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 523b84e65..655fd2df7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -434,7 +434,7 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_qim->addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); d_qstate.notifyInConflict(); d_consistent_ee = false; return; @@ -1047,7 +1047,7 @@ bool TermDb::reset( Theory::Effort effort ){ // equality is sent out as a lemma here. Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; - d_qim->addPendingLemma(eq, InferenceId::UNKNOWN); + d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY); d_qstate.notifyInConflict(); d_consistent_ee = false; return false; 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; } -- 2.30.2