Ho quant util (#1119)

Quantifiers utilities for higher-order.

This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.

Also adds required options and a minor utility for implementing app completion.

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;