From: Gereon Kremer Date: Wed, 17 Feb 2021 15:10:43 +0000 (+0100) Subject: TheoryIds for UF theory. (#5901) X-Git-Tag: cvc5-1.0.0~2272 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f52cd17ba0f9c455db1d45341ba39f04b319e621;p=cvc5.git TheoryIds for UF theory. (#5901) This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN. --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 5a2158d00..81c34cf3f 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -141,6 +141,13 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_REDUCTION: return "REDUCTION"; case InferenceId::STRINGS_PREFIX_CONFLICT: return "PREFIX_CONFLICT"; + case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE"; + case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM"; + case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY"; + case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE"; + case InferenceId::UF_HO_MODEL_EXTENSIONALITY: + return "UF_HO_MODEL_EXTENSIONALITY"; + default: return "?"; } } diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f28faa037..a48a8c366 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -404,7 +404,40 @@ enum class InferenceId STRINGS_PREFIX_CONFLICT, //-------------------------------------- end prefix conflict - UNKNOWN, + // Clause from the uf symmetry breaker + UF_BREAK_SYMMETRY, + UF_CARD_CLIQUE, + UF_CARD_COMBINED, + UF_CARD_ENFORCE_NEGATIVE, + UF_CARD_EQUIV, + UF_CARD_MONOTONE_COMBINED, + UF_CARD_SIMPLE_CONFLICT, + UF_CARD_SPLIT, + //-------------------------------------- begin HO extension to UF + // Encodes an n-ary application as a chain of binary HO_APPLY applications + // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn)) + UF_HO_APP_ENCODE, + UF_HO_APP_CONV_SKOLEM, + // Adds an extensionality lemma to witness that disequal functions have + // different applications + // (not (= (f sk1 .. skn) (g sk1 .. skn)) + UF_HO_EXTENSIONALITY, + //-------------------------------------- begin model-construction specific part + // These rules are necessary to ensure that we build models properly. For more + // details see Section 3.3 of Barbosa et al. CADE'19. + // + // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY + // equivalent by adding the equality as a lemma + // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn)) + UF_HO_MODEL_APP_ENCODE, + // Adds an extensionality lemma to witness that disequal functions have + // different applications + // (not (= (f sk1 .. skn) (g sk1 .. skn)) + UF_HO_MODEL_EXTENSIONALITY, + //-------------------------------------- end model-construction specific part + //-------------------------------------- end HO extension to UF + + UNKNOWN }; /** diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 697a828a4..861da3558 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r) //split on the equality s Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); // send lemma, with caching - if (d_im.lemma(lem, InferenceId::UNKNOWN)) + if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT)) { Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; //tell the sat solver to explore the equals branch first @@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector& clique) eqs.push_back(d_cardinality_literal[d_cardinality].notNode()); Node lem = NodeManager::currentNM()->mkNode(OR, eqs); // send lemma, with caching - if (d_im.lemma(lem, InferenceId::UNKNOWN)) + if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE)) { Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; ++(d_thss->d_statistics.d_clique_lemmas); @@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() { Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ), getCardinalityLiteral( d_maxNegCard.get() ).negate() ); Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl; - d_im.conflict(lem, InferenceId::UNKNOWN); + d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT); } } @@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall() Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkAnd(force_cl)); Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE, LemmaProperty::NONE, false); return false; } } @@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); eqv_lit = lit.eqNode( eqv_lit ); Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; - d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV, LemmaProperty::NONE, false); d_card_assertions_eqv_lemma[lit] = true; } } @@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level) Node eq = Rewriter::rewrite( a.eqNode( b ) ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() ); Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UF_CARD_SPLIT, LemmaProperty::NONE, false); d_im.requirePhase(eq, true); type_proc[tn] = true; break; @@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality() << " : " << cf << std::endl; Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict" << " : " << cf << std::endl; - d_im.conflict(cf, InferenceId::UNKNOWN); + d_im.conflict(cf, InferenceId::UF_CARD_MONOTONE_COMBINED); return; } } @@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality() << std::endl; Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf << std::endl; - d_im.conflict(cf, InferenceId::UNKNOWN); + d_im.conflict(cf, InferenceId::UF_CARD_COMBINED); } } } diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 55e2500af..a9e48d7ca 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq) Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc); Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN); + d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY); return 1; } return 0; @@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN); + d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM); d_uf_std_skolem[f] = new_f; } else @@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) Node lem = nm->mkNode(OR, deq.negate(), eq); Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN); + d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY); return 1; } } @@ -284,7 +284,12 @@ unsigned HoExtension::applyAppCompletion(TNode n) Node eq = n.eqNode(ret); Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl; - d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n}); + d_im.assertInternalFact(eq, + true, + InferenceId::UF_HO_APP_ENCODE, + PfRule::HO_APP_ENCODE, + {}, + {n}); return 1; } Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." @@ -441,7 +446,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) Node eq = n.eqNode(hn); Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq << std::endl; - d_im.lemma(eq, InferenceId::UNKNOWN); + d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE); return false; } } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index c8cfe295e..3ad94c571 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -315,7 +315,7 @@ void TheoryUF::presolve() { ++i) { Debug("uf") << "uf: generating a lemma: " << *i << std::endl; // no proof generator provided - d_im.lemma(*i, InferenceId::UNKNOWN); + d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY); } } if( d_thss ){