diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-13 15:14:59 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-13 15:14:59 -0500 |
commit | e69f6c3aa94e382d082d23f847709a97d9470f31 (patch) | |
tree | 814080b7c1b473e03928b339b99d653819246185 /src/theory/quantifiers/term_database.h | |
parent | bfd8e5426cfa5d8955e62c822d61536e42b3eff9 (diff) |
Move higher-order matching predicate (#3280)
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 15 |
1 files changed, 14 insertions, 1 deletions
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<Node, Node> d_term_elig_eqc; + /** + * Dummy predicate that states terms should be considered first-class members + * of equality engine (for higher-order). + */ + std::map<TypeNode, Node> d_ho_type_match_pred; /** set has term */ void setHasTerm( Node n ); /** helper for evaluate term */ |