Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)

* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.

* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.

* Remove unused NodeList

3 files changed, 346 insertions, 36 deletions

diff --git a/src/options/uf_options b/src/options/uf_options
index cbac04b18..7e1cbdb17 100644
--- a/src/options/uf_options
+++ b/src/options/uf_options
@@ -41,4 +41,9 @@ option ufssFairness --uf-ss-fair bool :default true
 option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false
  group monotone sorts when enforcing fairness for finite model finding
 
+option ufHo --uf-ho bool :read-write :default false
+ enable support for higher-order reasoning
+option ufHoExt --uf-ho-ext bool :read-write :default true
+ apply extensionality on function symbols
+
 endmodule
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 981e3e2ac..e8cc3b385 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -28,6 +28,7 @@
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/quantifiers/term_database.h"
 #include "options/theory_options.h"
+#include "theory/uf/theory_uf_rewriter.h"
 
 using namespace std;
 
@@ -47,13 +48,18 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
       d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF",
                        true),
       d_conflict(c, false),
-      d_literalsToPropagate(c),
-      d_literalsToPropagateIndex(c, 0),
+      d_extensionality_deq(u),
+      d_uf_std_skolem(u),
       d_functionsTerms(c),
       d_symb(u, instanceName)
 {
+  d_true = NodeManager::currentNM()->mkConst( true );
+
   // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+  d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
+  if( options::ufHo() ){
+    d_equalityEngine.addFunctionKind(kind::HO_APPLY);
+  }
 }
 
 TheoryUF::~TheoryUF() {
@@ -123,6 +129,11 @@ void TheoryUF::check(Effort level) {
     TNode atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
+      if( options::ufHo() && options::ufHoExt() ){
+        if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
+          applyExtensionality( fact );
+        }
+      }
     } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
       if( d_thss == NULL ){
         if( !getLogicInfo().hasCardinalityConstraints() ){
@@ -151,9 +162,71 @@ void TheoryUF::check(Effort level) {
         d_conflict = true;
       }
     }
+    if(! d_conflict && fullEffort(level) ){
+      if( options::ufHo() ){
+        checkHigherOrder();
+      }
+    }
   }
 }/* TheoryUF::check() */
 
+Node TheoryUF::getApplyUfForHoApply( Node node ) {
+  Assert( node[0].getType().getNumChildren()==2 );
+  std::vector< TNode > args;
+  Node f = TheoryUfRewriter::decomposeHoApply( node, args, true );
+  Node new_f = f;
+  if( !TheoryUfRewriter::canUseAsApplyUfOperator( f ) ){
+    NodeNodeMap::const_iterator itus = d_uf_std_skolem.find( f );
+    if( itus==d_uf_std_skolem.end() ){
+      // introduce skolem to make a standard APPLY_UF
+      new_f = NodeManager::currentNM()->mkSkolem( "app_uf", f.getType() );
+      Node lem = new_f.eqNode( f );
+      Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl;
+      d_out->lemma( lem );
+      d_uf_std_skolem[f] = new_f;
+    }else{
+      new_f = (*itus).second;
+    }
+  }
+  Assert( TheoryUfRewriter::canUseAsApplyUfOperator( new_f ) );
+  args[0] = new_f;
+  Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, args );
+  return ret;
+}
+
+Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
+  Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
+  if( node.getKind()==kind::APPLY_UF ){
+    return node.getOperator();
+  }else{
+    return d_equalityEngine.getRepresentative( node[0] );
+  }
+}
+
+unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
+  Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
+  return node.getKind()==kind::APPLY_UF ? 0 : 1;
+}
+
+Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) {
+  Trace("uf-ho-debug") << "uf-ho-debug : expanding definition : " << node << std::endl;
+  if( node.getKind()==kind::HO_APPLY ){
+    if( !options::ufHo() ){
+      std::stringstream ss;
+      ss << "Partial function applications are not supported in default mode, try --uf-ho.";
+      throw LogicException(ss.str());
+    }
+    // convert HO_APPLY to APPLY_UF if fully applied
+    if( node[0].getType().getNumChildren()==2 ){
+      Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
+      Node ret = getApplyUfForHoApply( node );
+      Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret << std::endl;
+      return ret;
+    }
+  }
+  return node;
+}
+
 void TheoryUF::preRegisterTerm(TNode node) {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
@@ -161,12 +234,17 @@ void TheoryUF::preRegisterTerm(TNode node) {
     d_thss->preRegisterTerm(node);
   }
 
+  // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
+  //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
+  Assert( node.getKind()!=kind::HO_APPLY || options::ufHo() );
+
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
     d_equalityEngine.addTriggerEquality(node);
     break;
   case kind::APPLY_UF:
+  case kind::HO_APPLY:
     // Maybe it's a predicate
     if (node.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
@@ -251,33 +329,26 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
 }
 
 void TheoryUF::collectModelInfo( TheoryModel* m ){
+  Debug("uf") << "UF : collectModelInfo " << std::endl;
   set<Node> termSet;
 
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
 
   m->assertEqualityEngine( &d_equalityEngine, &termSet );
-  // if( fullModel ){
-  //   std::map< TypeNode, TypeEnumerator* > type_enums;
-  //   //must choose proper representatives
-  //   // for each equivalence class, specify fresh constant as representative
-  //   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  //   while( !eqcs_i.isFinished() ){
-  //     Node eqc = (*eqcs_i);
-  //     TypeNode tn = eqc.getType();
-  //     if( tn.isSort() ){
-  //       if( type_enums.find( tn )==type_enums.end() ){
-  //         type_enums[tn] = new TypeEnumerator( tn );
-  //       }
-  //       Node rep = *(*type_enums[tn]);
-  //       ++(*type_enums[tn]);
-  //       //specify the constant as the representative
-  //       m->assertEquality( eqc, rep, true );
-  //       m->assertRepresentative( rep );
-  //     }
-  //     ++eqcs_i;
-  //   }
-  // }
+
+  if( options::ufHo() ){
+    for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
+      Node n = *it;
+      if( n.getKind()==kind::APPLY_UF ){
+        // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY
+        Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n );
+        m->assertEquality( n, hn, true );
+      }
+    }
+  }
+
+  Debug("uf") << "UF : finish collectModelInfo " << std::endl;
 }
 
 void TheoryUF::presolve() {
@@ -466,7 +537,8 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
       if( !d_equalityEngine.areEqual( f1, f2 ) ){
         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
-        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
+        unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
+        for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
           TNode x = f1[k];
           TNode y = f2[k];
           Assert( d_equalityEngine.hasTerm(x) );
@@ -532,17 +604,18 @@ void TheoryUF::computeCareGraph() {
     unsigned functionTerms = d_functionsTerms.size();
     for (unsigned i = 0; i < functionTerms; ++ i) {
       TNode f1 = d_functionsTerms[i];
-      Node op = f1.getOperator();
+      Node op = getOperatorForApplyTerm( f1 );
+      unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
       std::vector< TNode > reps;
       bool has_trigger_arg = false;
-      for( unsigned j=0; j<f1.getNumChildren(); j++ ){
+      for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
         reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
         if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
           has_trigger_arg = true;
         }
       }
       if( has_trigger_arg ){
-        index[op].addTerm( f1, reps );
+        index[op].addTerm( f1, reps, arg_start_index );
         arity[op] = reps.size();
       }
     }
@@ -551,6 +624,7 @@ void TheoryUF::computeCareGraph() {
       Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
       addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
     }
+    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
   }
 }/* TheoryUF::computeCareGraph() */
 
@@ -586,6 +660,180 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   }
 }
 
+unsigned TheoryUF::applyExtensionality(TNode deq) {
+  Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL );
+  Assert( deq[0][0].getType().isFunction() );
+  // apply extensionality
+  if( d_extensionality_deq.find( deq )==d_extensionality_deq.end() ){
+    d_extensionality_deq.insert( deq );
+    TypeNode tn = deq[0][0].getType();
+    std::vector< Node > skolems;
+    for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
+      Node k = NodeManager::currentNM()->mkSkolem( "k", tn[i], "skolem created for extensionality." );
+      skolems.push_back( k );
+    }
+    Node t[2];
+    for( unsigned i=0; i<2; i++ ){
+      std::vector< Node > children;
+      Node curr = deq[0][i];
+      while( curr.getKind()==kind::HO_APPLY ){
+        children.push_back( curr[1] );
+        curr = curr[0];
+      }
+      children.push_back( curr );
+      std::reverse( children.begin(), children.end() );
+      children.insert( children.end(), skolems.begin(), skolems.end() );
+      t[i] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+    }
+    Node conc = t[0].eqNode( t[1] ).negate();
+    Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc );
+    Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl;
+    d_out->lemma( lem );
+    return 1;
+  }else{
+    return 0;
+  }
+}
+
+unsigned TheoryUF::checkExtensionality() {
+  unsigned num_lemmas = 0;
+  Trace("uf-ho") << "TheoryUF::checkExtensionality..." << std::endl;
+  // This is bit eager: we should allow functions to be neither equal nor disequal during model construction
+  // However, doing so would require a function-type enumerator.
+  std::map< TypeNode, std::vector< Node > > func_eqcs;
+
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    TypeNode tn = eqc.getType();
+    if( tn.isFunction() ){
+      func_eqcs[tn].push_back( eqc );
+      Trace("uf-ho-debug") << "  func eqc : " << tn << " : " << eqc << std::endl;
+    }
+    ++eqcs_i;
+  }
+  
+  for( std::map< TypeNode, std::vector< Node > >::iterator itf = func_eqcs.begin(); 
+       itf != func_eqcs.end(); ++itf ){
+    for( unsigned j=0; j<itf->second.size(); j++ ){
+      for( unsigned k=(j+1); k<itf->second.size(); k++ ){ 
+        // if these equivalence classes are not explicitly disequal, do extensionality to ensure distinctness
+        if( !d_equalityEngine.areDisequal( itf->second[j], itf->second[k], false ) ){
+          Node deq = Rewriter::rewrite( itf->second[j].eqNode( itf->second[k] ).negate() );
+          num_lemmas += applyExtensionality( deq );
+        }
+      }   
+    }
+  }
+  return num_lemmas;
+}
+
+unsigned TheoryUF::applyAppCompletion( TNode n ) {
+  Assert( n.getKind()==kind::APPLY_UF );
+
+  //must expand into APPLY_HO version if not there already
+  Node ret = TheoryUfRewriter::getHoApplyForApplyUf( n );
+  if( !d_equalityEngine.hasTerm( ret ) || !d_equalityEngine.areEqual( ret, n ) ){
+    Node eq = ret.eqNode( n );
+    Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl;
+    d_equalityEngine.assertEquality(eq, true, d_true);
+    return 1;
+  }else{
+    Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "." << std::endl;
+    return 0;
+  }
+}
+
+unsigned TheoryUF::checkAppCompletion() {
+  Trace("uf-ho") << "TheoryUF::checkApplyCompletion..." << std::endl;
+  // compute the operators that are relevant (those for which an HO_APPLY exist)
+  std::set< TNode > rlvOp;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  std::map< TNode, std::vector< Node > > apply_uf;
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    Trace("uf-ho-debug") << "  apply completion : visit eqc " << eqc << std::endl;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      Node n = *eqc_i;
+      if( n.getKind()==kind::APPLY_UF || n.getKind()==kind::HO_APPLY ){
+        int curr_sum = 0;
+        std::map< TNode, bool > curr_rops;
+        if( n.getKind()==kind::APPLY_UF ){
+          TNode rop = d_equalityEngine.getRepresentative( n.getOperator() );
+          if( rlvOp.find( rop )!=rlvOp.end() ){
+            // try if its operator is relevant
+            curr_sum = applyAppCompletion( n );
+            if( curr_sum>0 ){
+              return curr_sum;
+            }
+          }else{
+            // add to pending list
+            apply_uf[rop].push_back( n );
+          }
+          //arguments are also relevant operators  FIXME (github issue #1115)
+          for( unsigned k=0; k<n.getNumChildren(); k++ ){
+            if( n[k].getType().isFunction() ){
+              TNode rop = d_equalityEngine.getRepresentative( n[k] );
+              curr_rops[rop] = true;
+            }
+          }
+        }else{
+          Assert( n.getKind()==kind::HO_APPLY );
+          TNode rop = d_equalityEngine.getRepresentative( n[0] );
+          curr_rops[rop] = true;
+        }
+        for( std::map< TNode, bool >::iterator itc = curr_rops.begin(); itc != curr_rops.end(); ++itc ){
+          TNode rop = itc->first;
+          if( rlvOp.find( rop )==rlvOp.end() ){
+            rlvOp.insert( rop );
+            // now, try each pending APPLY_UF for this operator
+            std::map< TNode, std::vector< Node > >::iterator itu = apply_uf.find( rop );
+            if( itu!=apply_uf.end() ){
+              for( unsigned j=0; j<itu->second.size(); j++ ){
+                curr_sum = applyAppCompletion( itu->second[j] );
+                if( curr_sum>0 ){
+                  return curr_sum;
+                }
+              }
+            }
+          }
+        }
+      }
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+  return 0;
+}
+
+unsigned TheoryUF::checkHigherOrder() {
+  Trace("uf-ho") << "TheoryUF::checkHigherOrder..." << std::endl;
+
+  // infer new facts based on apply completion until fixed point 
+  unsigned num_facts;
+  do{
+    num_facts = checkAppCompletion();
+    if( d_conflict ){
+      Trace("uf-ho") << "...conflict during app-completion." << std::endl;
+      return 1;  
+    }
+  }while( num_facts>0 );
+
+  if( options::ufHoExt() ){
+    unsigned num_lemmas = 0;
+
+    num_lemmas = checkExtensionality();
+    if( num_lemmas>0 ){
+      Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." << std::endl;
+      return num_lemmas;
+    }
+  }
+
+  Trace("uf-ho") << "...finished check higher order." << std::endl;
+
+  return 0;
+}
 
 } /* namespace CVC4::theory::uf */
 } /* namespace CVC4::theory */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index bd10f5961..0665b8272 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -30,6 +30,7 @@
 #include "context/cdo.h"
 #include "context/cdhashset.h"
 
+
 namespace CVC4 {
 namespace theory {
 
@@ -45,7 +46,8 @@ class StrongSolverTheoryUF;
 class TheoryUF : public Theory {
 
   friend class StrongSolverTheoryUF;
-
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 public:
 
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -125,6 +127,15 @@ private:
   /** The conflict node */
   Node d_conflictNode;
 
+  /** extensionality has been applied to these disequalities */
+  NodeSet d_extensionality_deq;
+
+  /** map from non-standard operators to their skolems */
+  NodeNodeMap d_uf_std_skolem;
+
+  /** node for true */
+  Node d_true;
+
   /**
    * Should be called to propagate the literal. We use a node here
    * since some of the propagated literals are not kept anywhere.
@@ -142,12 +153,6 @@ private:
    */
   Node explain(TNode literal, eq::EqProof* pf);
 
-  /** Literals to propagate */
-  context::CDList<Node> d_literalsToPropagate;
-
-  /** Index of the next literal to propagate */
-  context::CDO<unsigned> d_literalsToPropagateIndex;
-
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
 
@@ -169,6 +174,57 @@ private:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
+private: // for higher-order
+  /** applyExtensionality 
+   * Given disequality deq 
+   * If not already cached, this sends a lemma of the form 
+   *   f = g V (f k) != (g k) for fresh constant k.
+   * on the output channel.
+   * Return value is the number of lemmas sent.
+   */
+  unsigned applyExtensionality(TNode deq);
+
+  /** check whether extensionality should be applied for any
+   * pair of terms in the equality engine.
+   */
+  unsigned checkExtensionality();
+  
+  /** applyAppCompletion
+   * This infers a correspondence between APPLY_UF and HO_APPLY 
+   * versions of terms for higher-order.
+   * Given APPLY_UF node e.g. (f a b c), this adds the equality to its 
+   * HO_APPLY equivalent:
+   *   (f a b c) == (@ (@ (@ f a) b) c)
+   * to equality engine, if not already equal.
+   * Return value is the number of equalities added.
+   */
+  unsigned applyAppCompletion( TNode n );
+
+  /** check whether app-completion should be applied for any
+   * pair of terms in the equality engine.
+   */
+  unsigned checkAppCompletion();
+
+  /** check higher order
+   * This is called at full effort and infers facts and sends lemmas
+   * based on higher-order reasoning (specifically, extentionality and
+   * app completion above). It returns the number of lemmas plus facts
+   * added to the equality engine.
+  */
+  unsigned checkHigherOrder();
+
+  /** get apply uf for ho apply 
+   * This returns the APPLY_UF equivalent for the HO_APPLY term node, where
+   * node has non-functional return type (that is, it corresponds to a fully
+   * applied function term).
+   * This call may introduce a skolem for the head operator and send out a lemma
+   * specifying the definition.
+  */
+  Node getApplyUfForHoApply( Node node );
+  /** get the operator for this node (node should be either APPLY_UF or HO_APPLY) */
+  Node getOperatorForApplyTerm( TNode node );
+  /** get the starting index of the arguments for node (node should be either APPLY_UF or HO_APPLY) */
+  unsigned getArgumentStartIndexForApplyTerm( TNode node );
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -181,7 +237,8 @@ public:
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void finishInit();
 
-  void check(Effort);
+  void check(Effort);  
+  Node expandDefinition(LogicRequest &logicRequest, Node node);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);