From e69f6c3aa94e382d082d23f847709a97d9470f31 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Sep 2019 15:14:59 -0500 Subject: [PATCH] Move higher-order matching predicate (#3280) --- src/theory/quantifiers/ematching/ho_trigger.cpp | 8 ++++---- src/theory/quantifiers/term_database.cpp | 14 ++++++++++++++ src/theory/quantifiers/term_database.h | 15 ++++++++++++++- src/theory/quantifiers/term_util.cpp | 13 ------------- src/theory/quantifiers/term_util.h | 13 ------------- src/theory/uf/ho_extension.cpp | 3 ++- 6 files changed, 34 insertions(+), 32 deletions(-) diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 7598e6fdc..b01d5e1df 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -469,12 +469,12 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; unsigned numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - unsigned size = d_quantEngine->getTermDatabase()->getNumOperators(); - quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); + quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase(); + unsigned size = tdb->getNumOperators(); NodeManager* nm = NodeManager::currentNM(); for (unsigned j = 0; j < size; j++) { - Node f = d_quantEngine->getTermDatabase()->getOperator(j); + Node f = tdb->getOperator(j); if (f.isVar()) { TypeNode tn = f.getType(); @@ -497,7 +497,7 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // if a variable of this type occurs in this trigger if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { - Node u = tutil->getHoTypeMatchPredicate(tn); + Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); if (d_quantEngine->addLemma(au)) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 84147bf6b..9da9c95b6 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1229,6 +1229,20 @@ TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { return d_func_map_trie[f].existsTerm( args ); } +Node TermDb::getHoTypeMatchPredicate(TypeNode tn) +{ + std::map::iterator ithp = d_ho_type_match_pred.find(tn); + if (ithp != d_ho_type_match_pred.end()) + { + return ithp->second; + } + NodeManager* nm = NodeManager::currentNM(); + TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType()); + Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types"); + d_ho_type_match_pred[tn] = k; + return k; +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f92bce8bd..7caf29d20 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -291,6 +291,14 @@ class TermDb : public QuantifiersUtil { * 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 + * first-class representatives in the quantifier-free UF solver. For a typical + * use case, we call getHoTypeMatchPredicate which returns a fresh predicate + * P of type (tn -> Bool). Then, we add P( f ) as a lemma. + */ + Node getHoTypeMatchPredicate(TypeNode tn); private: /** reference to the quantifiers engine */ @@ -328,7 +336,12 @@ class TermDb : public QuantifiersUtil { /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ - std::map< Node, Node > d_term_elig_eqc; + std::map d_term_elig_eqc; + /** + * Dummy predicate that states terms should be considered first-class members + * of equality engine (for higher-order). + */ + std::map d_ho_type_match_pred; /** set has term */ void setHasTerm( Node n ); /** helper for evaluate term */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 48dc88537..6ffc50c97 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -954,19 +954,6 @@ bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok) return false; } -Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) { - std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn ); - if( ithp==d_ho_type_match_pred.end() ){ - TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); - Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" ); - d_ho_type_match_pred[tn] = k; - return k; - }else{ - return ithp->second; - } -} - - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 99ea483d9..52965d2fa 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -348,19 +348,6 @@ public: * minimum and maximum elements, for example tn is Bool or BitVector. */ static Node mkTypeConst(TypeNode tn, bool pol); - - // for higher-order - private: - /** dummy predicate that states terms should be considered first-class members of equality engine */ - std::map< TypeNode, Node > d_ho_type_match_pred; -public: - /** get higher-order type match predicate - * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the - * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh - * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma. - * TODO: we may eliminate this depending on how github issue #1115 is resolved. - */ - Node getHoTypeMatchPredicate( TypeNode tn ); };/* class TermUtil */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 4d5a879ad..88b2ba8d2 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -316,7 +316,8 @@ unsigned HoExtension::checkAppCompletion() // add to pending list apply_uf[rop].push_back(n); } - // arguments are also relevant operators FIXME (github issue #1115) + // Arguments are also relevant operators. + // It might be possible include fewer terms here, see #1115. for (unsigned k = 0; k < n.getNumChildren(); k++) { if (n[k].getType().isFunction()) -- 2.30.2