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

1 files changed, 276 insertions, 28 deletions

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 */