From 57919ba7271a6c2b36173f2ba0f580b84f962b1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Feb 2021 12:29:58 -0600 Subject: [PATCH] Remove support for inst closure (#5874) This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database. It also simplifies the TermDatabase::addTerm method (which changed indentation). --- src/api/cvc4cpp.cpp | 2 - src/api/cvc4cppkind.h | 8 -- src/options/quantifiers_options.toml | 11 -- src/parser/smt2/smt2.cpp | 4 - .../ematching/candidate_generator.cpp | 3 +- src/theory/quantifiers/equality_query.cpp | 5 - src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers/kinds | 5 +- src/theory/quantifiers/term_database.cpp | 105 +++++------------- src/theory/quantifiers/term_database.h | 27 +---- src/theory/quantifiers/theory_quantifiers.cpp | 12 -- .../theory_quantifiers_type_rules.h | 14 --- src/theory/quantifiers_engine.cpp | 30 +++-- src/theory/quantifiers_engine.h | 6 +- 14 files changed, 54 insertions(+), 180 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 541c5f5a5..10f39cb38 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -333,7 +333,6 @@ const static std::unordered_map s_kinds{ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST}, - {INST_CLOSURE, CVC4::Kind::INST_CLOSURE}, {INST_PATTERN, CVC4::Kind::INST_PATTERN}, {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN}, {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE}, @@ -629,7 +628,6 @@ const static std::unordered_map {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, - {CVC4::Kind::INST_CLOSURE, INST_CLOSURE}, {CVC4::Kind::INST_PATTERN, INST_PATTERN}, {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 0bd4117dc..3fb16abcb 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2742,14 +2742,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ BOUND_VAR_LIST, - /* - * A predicate for specifying term in instantiation closure. - * Parameters: 1 - * -[1]: Term - * Create with: - * mkTerm(Kind kind, Term child) - */ - INST_CLOSURE, /* * An instantiation pattern. * Specifies a (list of) terms to be used as a pattern for quantifier diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4b98cb84d..fd781ab2b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1762,17 +1762,6 @@ header = "options/quantifiers_options.h" default = "true" help = "compute inverse for concat over equalities rather than producing an invertibility condition" -### Local theory extensions options - -[[option]] - name = "lteRestrictInstClosure" - category = "regular" - long = "lte-restrict-inst-closure" - type = "bool" - default = "false" - read_only = true - help = "treat arguments of inst closure as restricted terms for instantiation" - ### Reduction options [[option]] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9c5474a47..4d75a982b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -82,10 +82,6 @@ void Smt2::addTranscendentalOperators() void Smt2::addQuantifiersOperators() { - if (!strictModeEnabled()) - { - addOperator(api::INST_CLOSURE, "inst-closure"); - } } void Smt2::addBitvectorOperators() { diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 97693fae0..eb02eb19e 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -189,7 +189,8 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( n.getType().isComparableTo( d_match_pattern_type ) ){ TNode nh = tdb->getEligibleTermInEqc(n); if( !nh.isNull() ){ - if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ + if (options::instMaxLevel() != -1) + { nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); //don't consider this if already the instantiation is ineligible if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f)) diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index c60c98d70..def27fe5a 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -172,11 +172,6 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; - } - else if (options::lteRestrictInstClosure() - && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false))) - { - return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 3bbe15b8c..49f1fe116 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -217,7 +217,7 @@ bool Instantiate::addInstantiation( } // check based on instantiation level - if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure()) + if (options::instMaxLevel() != -1) { for (Node& t : terms) { diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 1534d2d4d..3f15ef916 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -44,15 +44,12 @@ sort INST_PATTERN_LIST_TYPE \ # a list of instantiation patterns operator INST_PATTERN_LIST 1: "a list of instantiation patterns" -operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure." - typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule -typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule -typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule +typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule endtheory diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5a6e38b78..1498c29b7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -198,60 +198,45 @@ Node TermDb::getMatchOperator( Node n ) { } } -void TermDb::addTerm(Node n, - std::set& added, - bool withinQuant, - bool withinInstClosure) +void TermDb::addTerm(Node n) { - //don't add terms in quantifier bodies - if( withinQuant && !options::registerQuantBodyTerms() ){ + if (d_processed.find(n) != d_processed.end()) + { return; } - bool rec = false; - if (d_processed.find(n) == d_processed.end()) + d_processed.insert(n); + if (!TermUtil::hasInstConstAttr(n)) { - d_processed.insert(n); - if (!TermUtil::hasInstConstAttr(n)) + Trace("term-db-debug") << "register term : " << n << std::endl; + d_type_map[n.getType()].push_back(n); + // if this is an atomic trigger, consider adding it + if (inst::TriggerTermInfo::isAtomicTrigger(n)) { - Trace("term-db-debug") << "register term : " << n << std::endl; - d_type_map[n.getType()].push_back(n); - // if this is an atomic trigger, consider adding it - if (inst::TriggerTermInfo::isAtomicTrigger(n)) - { - Trace("term-db") << "register term in db " << n << std::endl; + Trace("term-db") << "register term in db " << n << std::endl; - Node op = getMatchOperator(n); - Trace("term-db-debug") << " match operator is : " << op << std::endl; - if (d_op_map.find(op) == d_op_map.end()) - { - d_ops.push_back(op); - } - d_op_map[op].push_back(n); - added.insert(n); - // If we are higher-order, we may need to register more terms. - if (options::ufHo()) - { - addTermHo(n, added, withinQuant, withinInstClosure); - } + Node op = getMatchOperator(n); + Trace("term-db-debug") << " match operator is : " << op << std::endl; + if (d_op_map.find(op) == d_op_map.end()) + { + d_ops.push_back(op); + } + d_op_map[op].push_back(n); + // If we are higher-order, we may need to register more terms. + if (options::ufHo()) + { + addTermHo(n); } } - else - { - setTermInactive(n); - } - rec = true; } - if (withinInstClosure - && d_iclosure_processed.find(n) == d_iclosure_processed.end()) + else { - d_iclosure_processed.insert(n); - rec = true; + setTermInactive(n); } - if (rec && !n.isClosure()) + if (!n.isClosure()) { for (const Node& nc : n) { - addTerm(nc, added, withinQuant, withinInstClosure); + addTerm(nc); } } } @@ -442,10 +427,7 @@ void TermDb::computeUfTerms( TNode f ) { } } -void TermDb::addTermHo(Node n, - std::set& added, - bool withinQuant, - bool withinInstClosure) +void TermDb::addTermHo(Node n) { Assert(options::ufHo()); if (n.getType().isFunction()) @@ -494,7 +476,7 @@ void TermDb::addTermHo(Node n, // also add standard application version args.insert(args.begin(), curr); Node uf_n = nm->mkNode(APPLY_UF, args); - addTerm(uf_n, added, withinQuant, withinInstClosure); + addTerm(uf_n); } } @@ -918,18 +900,6 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) { - if( options::lteRestrictInstClosure() ){ - //has to be both in inst closure and in ground assertions - if( !isInstClosure( n ) ){ - Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; - return false; - } - // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this - if( !hasTermCurrent( n, false ) ){ - Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; - return false; - } - } if( options::instMaxLevel()!=-1 ){ if( n.hasAttribute(InstLevelAttribute()) ){ int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f ); @@ -979,10 +949,6 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { } } -bool TermDb::isInstClosure( Node r ) { - return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); -} - void TermDb::setHasTerm( Node n ) { Trace("term-db-debug2") << "hasTerm : " << n << std::endl; if( d_has_map.find( n )==d_has_map.end() ){ @@ -1001,7 +967,6 @@ void TermDb::presolve() { d_op_map.clear(); d_type_map.clear(); d_processed.clear(); - d_iclosure_processed.clear(); } } @@ -1060,8 +1025,7 @@ bool TermDb::reset( Theory::Effort effort ){ } //compute has map - if (options::termDbMode() == options::TermDbMode::RELEVANT - || options::lteRestrictInstClosure()) + if (options::termDbMode() == options::TermDbMode::RELEVANT) { d_has_map.clear(); d_term_elig_eqc.clear(); @@ -1103,21 +1067,10 @@ bool TermDb::reset( Theory::Effort effort ){ it != it_end; ++it) { - if ((*it).d_assertion.getKind() != INST_CLOSURE) - { - setHasTerm((*it).d_assertion); - } + setHasTerm((*it).d_assertion); } } } - //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed - for (const Node& n : d_iclosure_processed) - { - if (!ee->hasTerm(n)) - { - ee->addTerm(n); - } - } if( options::ufHo() && options::hoMergeTermDb() ){ Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 244762d24..6a695e70e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -108,15 +108,11 @@ class TermDb : public QuantifiersUtil { * variable per type. */ Node getOrMakeTypeFreshVariable(TypeNode tn); - /** add a term to the database - * withinQuant is whether n is within the body of a quantified formula - * withinInstClosure is whether n is within an inst-closure operator (see - * Bansal et al CAV 2015). - */ - void addTerm(Node n, - std::set& added, - bool withinQuant = false, - bool withinInstClosure = false); + /** + * Add a term to the database, which registers it as a term that may be + * matched with via E-matching, and can be used in entailment tests below. + */ + void addTerm(Node n); /** get match operator for term n * * If n has a kind that we index, this function will @@ -268,12 +264,6 @@ class TermDb : public QuantifiersUtil { bool isTermEligibleForInstantiation(TNode n, TNode f); /** get eligible term in equivalence class of r */ Node getEligibleTermInEqc(TNode r); - /** is r a inst closure node? - * This terminology was used for specifying - * a particular status of nodes for - * Bansal et al., CAV 2015. - */ - bool isInstClosure(Node r); /** get higher-order type match predicate * * This predicate is used to force certain functions f of type tn to appear as @@ -292,8 +282,6 @@ class TermDb : public QuantifiersUtil { QuantifiersInferenceManager& d_qim; /** terms processed */ std::unordered_set< Node, NodeHashFunction > d_processed; - /** terms processed */ - std::unordered_set< Node, NodeHashFunction > d_iclosure_processed; /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ @@ -407,10 +395,7 @@ class TermDb : public QuantifiersUtil { * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and * d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1). */ - void addTermHo(Node n, - std::set& added, - bool withinQuant, - bool withinInstClosure); + void addTermHo(Node n); /** get operator representative */ Node getOperatorRepresentative( TNode op ) const; //------------------------------end higher-order term indexing diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 1cbb2ce40..7c2bbb019 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -162,18 +162,6 @@ bool TheoryQuantifiers::preNotifyFact( { getQuantifiersEngine()->assertQuantifier(atom, polarity); } - else if (k == INST_CLOSURE) - { - if (!polarity) - { - Unhandled() << "Unexpected inst-closure fact " << fact; - } - getQuantifiersEngine()->addTermToDatabase(atom[0], false, true); - if (!options::lteRestrictInstClosure()) - { - d_qstate.getEqualityEngine()->addTerm(atom[0]); - } - } else { Unhandled() << "Unexpected fact " << fact; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index c7cbb278f..01bea3707 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -127,20 +127,6 @@ struct QuantifierInstPatternListTypeRule { } };/* struct QuantifierInstPatternListTypeRule */ -struct QuantifierInstClosureTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::INST_CLOSURE); - if( check ){ - TypeNode tn = n[0].getType(check); - if( tn.isBoolean() ){ - throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean"); - } - } - return nodeManager->booleanType(); - } -};/* struct QuantifierInstClosureTypeRule */ - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a1d3f0ac7..0e28cab76 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -58,9 +58,7 @@ QuantifiersEngine::QuantifiersEngine( d_ierCounter_c(qstate.getSatContext()), d_presolve(qstate.getUserContext(), true), d_presolve_in(qstate.getUserContext()), - d_presolve_cache(qstate.getUserContext()), - d_presolve_cache_wq(qstate.getUserContext()), - d_presolve_cache_wic(qstate.getUserContext()) + d_presolve_cache(qstate.getUserContext()) { //---- utilities // term util must come before the other utilities @@ -273,8 +271,9 @@ void QuantifiersEngine::presolve() { //add all terms to database if( options::incrementalSolving() ){ Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl; - for( unsigned i=0; igetInstConstantBody(f), true); } -void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ +void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant) +{ + // don't add terms in quantifier bodies + if (withinQuant && !options::registerQuantBodyTerms()) + { + return; + } if( options::incrementalSolving() ){ if( d_presolve_in.find( n )==d_presolve_in.end() ){ d_presolve_in.insert( n ); d_presolve_cache.push_back( n ); - d_presolve_cache_wq.push_back( withinQuant ); - d_presolve_cache_wic.push_back( withinInstClosure ); } } //only wait if we are doing incremental solving if( !d_presolve || !options::incrementalSolving() ){ - std::set< Node > added; - d_term_db->addTerm(n, added, withinQuant, withinInstClosure); - - if (!withinQuant) + d_term_db->addTerm(n); + if (d_sygus_tdb && options::sygusEvalUnfold()) { - if (d_sygus_tdb && options::sygusEvalUnfold()) - { - d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); - } + d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d8f94f864..83e01e9e6 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -210,9 +210,7 @@ public: public: /** add term to database */ - void addTermToDatabase(Node n, - bool withinQuant = false, - bool withinInstClosure = false); + void addTermToDatabase(Node n, bool withinQuant = false); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); /** debug print equality engine */ @@ -379,8 +377,6 @@ public: /** presolve cache */ NodeSet d_presolve_in; NodeList d_presolve_cache; - BoolList d_presolve_cache_wq; - BoolList d_presolve_cache_wic; };/* class QuantifiersEngine */ }/* CVC4::theory namespace */ -- 2.30.2