diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9df9da957..852d94fde 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -132,6 +132,7 @@ class QuantifiersEngine; namespace inst{ class Trigger; + class HigherOrderTrigger; } namespace quantifiers { @@ -188,6 +189,7 @@ class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; //TODO: eliminate most of these friend class ::CVC4::theory::inst::Trigger; + friend class ::CVC4::theory::inst::HigherOrderTrigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; friend class ::CVC4::theory::quantifiers::QuantConflictFind; friend class ::CVC4::theory::quantifiers::RelevantDomain; @@ -251,6 +253,17 @@ private: Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ); TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); + /** compute uf eqc terms */ + void computeUfEqcTerms( TNode f ); + /** compute uf terms */ + void computeUfTerms( TNode f ); +private: // for higher-order term indexing + /** a map from matchable operators to their representative */ + std::map< TNode, TNode > d_ho_op_rep; + /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ + std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves; + /** get operator representative */ + Node getOperatorRepresentative( TNode op ) const; public: /** ground terms for operator */ unsigned getNumGroundTerms( Node f ); @@ -272,10 +285,6 @@ public: TNode getCongruentTerm( Node f, std::vector< TNode >& args ); /** compute arg reps */ void computeArgReps( TNode n ); - /** compute uf eqc terms */ - void computeUfEqcTerms( TNode f ); - /** compute uf terms */ - void computeUfTerms( TNode f ); /** in relevant domain */ bool inRelevantDomain( TNode f, unsigned i, TNode r ); /** evaluate a term under a substitution. Return representative in EE if possible. @@ -520,6 +529,19 @@ public: /** is bool connective term */ static bool isBoolConnectiveTerm( TNode n ); +//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 ); + //for sygus private: TermDbSygus * d_sygus_tdb; |