From: Andrew Reynolds Date: Mon, 14 Dec 2020 17:38:04 +0000 (-0600) Subject: Properly implement datatype selector triggers (#5624) X-Git-Tag: cvc5-1.0.0~2448 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af7c14503f4600559a104cd97181448a07837dd0;p=cvc5.git Properly implement datatype selector triggers (#5624) This ensures that datatype selectors are properly handled as triggers in E-matching. This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case. It also removes a deprecated option that is no longer used (in part due to our use of shared selectors). This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook. Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter. FYI @barrettcw --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 57bf69162..cb5785e6d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -263,14 +263,6 @@ header = "options/quantifiers_options.h" default = "false" help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1" -[[option]] - name = "purifyDtTriggers" - category = "regular" - long = "purify-dt-triggers" - type = "bool" - default = "false" - help = "purify dt triggers, match all constructors of correct form instead of selectors" - [[option]] name = "pureThTriggers" category = "regular" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b1f56ea37..3bb49b703 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1152,15 +1152,14 @@ Node SmtEngine::simplify(const Node& ex) return d_pp->simplify(ex); } -Node SmtEngine::expandDefinitions(const Node& ex) +Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly) { d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); SmtScope smts(this); finishInit(); d_state->doPendingPops(); - // set expandOnly flag to true - return d_pp->expandDefinitions(ex, true); + return d_pp->expandDefinitions(ex, expandOnly); } // TODO(#1108): Simplify the error reporting of this method. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f8a74597b..6f08359b5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -510,12 +510,15 @@ class CVC4_PUBLIC SmtEngine Node simplify(const Node& e); /** - * Expand the definitions in a term or formula. No other - * simplification or normalization is done. + * Expand the definitions in a term or formula. + * + * @param n The node to expand + * @param expandOnly if true, then the expandDefinitions function of + * TheoryEngine is not called on subterms of n. * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Node expandDefinitions(const Node& e); + Node expandDefinitions(const Node& n, bool expandOnly = true); /** * Get the assigned value of an expr (only if immediately preceded by a SAT diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index a2471c704..beefe4288 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/ematching/candidate_generator.h" #include "expr/dtype.h" #include "options/quantifiers_options.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" @@ -23,12 +25,11 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -using namespace std; -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { +namespace inst { bool CandidateGenerator::isLegalCandidate( Node n ){ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); @@ -48,8 +49,13 @@ void CandidateGeneratorQE::resetInstantiationRound(){ d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); } -void CandidateGeneratorQE::reset( Node eqc ){ +void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); } + +void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) +{ d_term_iter = 0; + d_eqc = eqc; + d_op = op; if( eqc.isNull() ){ d_mode = cand_term_db; }else{ @@ -58,7 +64,7 @@ void CandidateGeneratorQE::reset( Node eqc ){ }else{ eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); if( ee->hasTerm( eqc ) ){ - TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op); + TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op); if( tat ){ //create an equivalence class iterator in eq class eqc Node rep = ee->getRepresentative( eqc ); @@ -69,7 +75,6 @@ void CandidateGeneratorQE::reset( Node eqc ){ } }else{ //the only match is this term itself - d_eqc = eqc; d_mode = cand_term_ident; } } @@ -85,6 +90,11 @@ bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { } Node CandidateGeneratorQE::getNextCandidate(){ + return getNextCandidateInternal(); +} + +Node CandidateGeneratorQE::getNextCandidateInternal() +{ if( d_mode==cand_term_db ){ Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; //get next candidate term in the uf term database @@ -232,7 +242,7 @@ void CandidateGeneratorConsExpand::reset(Node eqc) Node CandidateGeneratorConsExpand::getNextCandidate() { // get the next term from the base class - Node curr = CandidateGeneratorQE::getNextCandidate(); + Node curr = getNextCandidateInternal(); if (curr.isNull() || (curr.hasOperator() && curr.getOperator() == d_op)) { return curr; @@ -256,3 +266,65 @@ bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n) { return isLegalCandidate(n); } + +CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe, + Node mpat) + : CandidateGeneratorQE(qe, mpat) +{ + Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl; + Assert(mpat.getKind() == APPLY_SELECTOR); + Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false); + Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl; + if (mpatExp.getKind() == ITE) + { + Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL); + Assert(mpatExp[2].getKind() == APPLY_UF); + d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]); + d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]); + } + else + { + // corner case of datatype with one constructor + Assert(mpatExp.getKind() == APPLY_SELECTOR_TOTAL); + d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp); + } + Assert(d_selOp != d_ufOp); +} + +void CandidateGeneratorSelector::reset(Node eqc) +{ + Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl; + // start with d_selOp + resetForOperator(eqc, d_selOp); +} + +Node CandidateGeneratorSelector::getNextCandidate() +{ + Node nextc = getNextCandidateInternal(); + if (!nextc.isNull()) + { + Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl; + return nextc; + } + else if (d_op == d_selOp) + { + if (d_ufOp.isNull()) + { + // corner case: selector cannot be wrongly applied (1-cons case) + d_op = Node::null(); + } + else + { + // finished correctly applied selectors, now try incorrectly applied ones + resetForOperator(d_eqc, d_ufOp); + return getNextCandidate(); + } + } + Trace("sel-trigger-debug") << "...finished" << std::endl; + // no more candidates + return Node::null(); +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index d7f61b17b..c1548050a 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -104,6 +104,10 @@ class CandidateGeneratorQE : public CandidateGenerator } protected: + /** reset this class for matching operator op in equivalence class eqc */ + void resetForOperator(Node eqc, Node op); + /** the default implementation of getNextCandidate. */ + Node getNextCandidateInternal(); /** operator you are looking for */ Node d_op; /** the equality class iterator (for cand_term_eqc) */ @@ -112,7 +116,7 @@ class CandidateGeneratorQE : public CandidateGenerator int d_term_iter; /** the TermDb index of the current ground term (for cand_term_db) */ int d_term_iter_limit; - /** the term we are matching (for cand_term_ident) */ + /** the current equivalence class */ Node d_eqc; /** candidate generation modes */ enum { @@ -208,6 +212,30 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE bool isLegalOpCandidate(Node n) override; }; +/** + * Candidate generator for selector applications, which considers both + * internal terms corresponding to correctly and incorrectly applied selectors. + */ +class CandidateGeneratorSelector : public CandidateGeneratorQE +{ + public: + CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat); + /** reset */ + void reset(Node eqc) override; + /** + * Get next candidate, returns matching candidates that are ground terms + * of the selector operator, followed by those that are applications of the + * UF corresponding to an invocation of applying this selector to an + * application of the wrong constructor. + */ + Node getNextCandidate() override; + protected: + /** the selector operator */ + Node d_selOp; + /** the UF operator */ + Node d_ufOp; +}; + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 2099a2cb8..588ec031d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -148,16 +148,14 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< break; } } - }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT && - options::purifyDtTriggers() && !options::dtSharedSelectors() ){ - d_match_pattern = d_match_pattern[0]; } d_match_pattern_type = d_match_pattern.getType(); Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); //now, collect children of d_match_pattern - if (d_match_pattern.getKind() == INST_CONSTANT) + Kind mpk = d_match_pattern.getKind(); + if (mpk == INST_CONSTANT) { d_children_types.push_back( d_match_pattern.getAttribute(InstVarNumAttribute())); @@ -198,8 +196,15 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< } //create candidate generator - if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - if (d_match_pattern.getKind() == APPLY_CONSTRUCTOR) + if (mpk == APPLY_SELECTOR) + { + // candidates for apply selector are a union of correctly and incorrectly + // applied selectors + d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern); + } + else if (Trigger::isAtomicTriggerKind(mpk)) + { + if (mpk == APPLY_CONSTRUCTOR) { // 1-constructors have a trivial way of generating candidates in a // given equivalence class @@ -224,7 +229,9 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_eq_class_rel = Node::null(); } } - }else if( d_match_pattern.getKind()==INST_CONSTANT ){ + } + else if (mpk == INST_CONSTANT) + { if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){ Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern); size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr); @@ -237,7 +244,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } } - else if (d_match_pattern.getKind() == EQUAL) + else if (mpk == EQUAL) { //we will be producing candidates via literal matching heuristics if (d_pattern.getKind() == NOT) @@ -272,10 +279,8 @@ int InstMatchGenerator::getMatch( //if t is null Assert(!t.isNull()); Assert(!quantifiers::TermUtil::hasInstConstAttr(t)); - Assert(d_match_pattern.getKind() == INST_CONSTANT - || t.getKind() == d_match_pattern.getKind()); - Assert(!Trigger::isAtomicTrigger(d_match_pattern) - || t.getOperator() == d_match_pattern.getOperator()); + // notice that t may have a different kind or operator from our match + // pattern, e.g. for APPLY_SELECTOR triggers. //first, check if ground arguments are not equal, or a match is in conflict Trace("matching-debug2") << "Setting immediate matches..." << std::endl; for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++) diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 95ab0674f..8d18c62bf 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -404,11 +404,15 @@ bool Trigger::isAtomicTrigger( Node n ){ } bool Trigger::isAtomicTriggerKind( Kind k ) { + // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this + // method is used both for trigger selection and for ground term registration, + // where these two things require those kinds respectively. return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR - || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION - || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER - || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT - || k == INT_TO_BITVECTOR || k == HO_APPLY || k == SEQ_NTH; + || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL + || k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET + || k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO + || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY + || k == SEQ_NTH; } bool Trigger::isRelationalTrigger( Node n ) { @@ -432,17 +436,13 @@ bool Trigger::isSimpleTrigger( Node n ){ return false; } } - if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){ - return false; - } if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT) { return false; } return true; - }else{ - return false; } + return false; } //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a5adf4d9c..b32e0799d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -870,6 +870,7 @@ set(regress_0_tests regress0/quantifiers/qcf-rel-dom-opt.smt2 regress0/quantifiers/quant-model-simplification.smt2 regress0/quantifiers/rew-to-scala.smt2 + regress0/quantifiers/selector-trigger.smt2 regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/sygus-inst-nia-psyco-060.smt2 diff --git a/test/regress/regress0/quantifiers/selector-trigger.smt2 b/test/regress/regress0/quantifiers/selector-trigger.smt2 new file mode 100644 index 000000000..4e5cf0ecf --- /dev/null +++ b/test/regress/regress0/quantifiers/selector-trigger.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T 0)) ( + ((Z) (Y (y Int))))) + +(declare-fun b () T) +(declare-fun a () Int) + +(declare-fun P (Int) Bool) +(assert (P (y b))) + +(assert (forall ((x T)) (not (P (y x))))) + +(check-sat)