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_util.h | |
| parent | bfd8e5426cfa5d8955e62c822d61536e42b3eff9 (diff) | |
Move higher-order matching predicate (#3280)
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 13 |
1 files changed, 0 insertions, 13 deletions
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 */ |