Add new kinds required for higher-order. (#1083)

This consists of a binary apply symbol HO_APPLY that returns the result of applying its first argument to its second argument. Update the UF rewriter to ensure that non-standard APPLY_UF applications are rewritten into curried applications of HO_APPLY.

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index e2d740e20e901f2c00af457d21b8bb0673426d44..500295a0c9e7f62469018fec35c63c7103e56ade 100644 (file)
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -29,4 +29,7 @@ typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule
 operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
 typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
 
+operator HO_APPLY 2 "higher-order (partial) function application"
+typerule HO_APPLY ::CVC4::theory::uf::HoApplyTypeRule
+
 endtheory

diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 0bd50220541a1e9d95a68a938f68064f21cf8184..db2f735c6f21f5e6ba6c7cbb11a30facbae9e186 100644 (file)
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -44,33 +44,55 @@ public:
         return RewriteResponse(REWRITE_DONE, newNode);
       }
     }
-    if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) {
-      // resolve away the lambda
-      context::Context fakeContext;
-      theory::SubstitutionMap substitutions(&fakeContext);
-      TNode lambda = node.getOperator();
-      for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
-        // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
-        Assert(formal != node.end());
-        // This rewrite step is important: if we have (f (f 5)) for
-        // some lambda term f, we want to beta-reduce the inside (f 5)
-        // application first.  Otherwise, we can end up in infinite
-        // recursion, because f's formal (say "x") gives the
-        // substitution "x |-> (f 5)".  Fine, the body of the lambda
-        // gets (f 5) in place for x.  But since the same lambda ("f")
-        // now occurs in the body, it's got the same bound var "x", so
-        // substitution continues and we replace that x by (f 5).  And
-        // then again.  :-(
-        //
-        // We need a better solution for distinguishing bound
-        // variables like this, but for now, handle it by going
-        // inside-out.  (Quantifiers shouldn't ever have this problem,
-        // so long as the bound vars in different quantifiers are kept
-        // different.)
-        Node n = Rewriter::rewrite(*arg);
-        substitutions.addSubstitution(*formal, n);
+    if(node.getKind() == kind::APPLY_UF) {
+      if( node.getOperator().getKind() == kind::LAMBDA ){
+        // resolve away the lambda
+        context::Context fakeContext;
+        theory::SubstitutionMap substitutions(&fakeContext);
+        TNode lambda = node.getOperator();
+        for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
+          // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
+          Assert(formal != node.end());
+          // This rewrite step is important: if we have (f (f 5)) for
+          // some lambda term f, we want to beta-reduce the inside (f 5)
+          // application first.  Otherwise, we can end up in infinite
+          // recursion, because f's formal (say "x") gives the
+          // substitution "x |-> (f 5)".  Fine, the body of the lambda
+          // gets (f 5) in place for x.  But since the same lambda ("f")
+          // now occurs in the body, it's got the same bound var "x", so
+          // substitution continues and we replace that x by (f 5).  And
+          // then again.  :-(
+          //
+          // We need a better solution for distinguishing bound
+          // variables like this, but for now, handle it by going
+          // inside-out.  (Quantifiers shouldn't ever have this problem,
+          // so long as the bound vars in different quantifiers are kept
+          // different.)
+          Node n = Rewriter::rewrite(*arg);
+          substitutions.addSubstitution(*formal, n);
+        }
+        return RewriteResponse(REWRITE_AGAIN_FULL, substitutions.apply(lambda[1]));
+      }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
+        return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
+      }
+    }else if( node.getKind() == kind::HO_APPLY ){
+      if( node[0].getKind() == kind::LAMBDA ){
+        // resolve one argument of the lambda
+        TNode arg = Rewriter::rewrite( node[1] );
+        TNode var = node[0][0][0];
+        Node new_body = node[0][1].substitute( var, arg );
+        if( node[0][0].getNumChildren()>1 ){
+          std::vector< Node > new_vars;
+          for( unsigned i=1; i<node[0][0].getNumChildren(); i++ ){
+            new_vars.push_back( node[0][0][i] );
+          }
+          std::vector< Node > largs;
+          largs.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, new_vars ) );
+          largs.push_back( new_body );
+          new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs );
+        }
+        return RewriteResponse( REWRITE_AGAIN_FULL, new_body );
       }
-      return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1]));
     }
     return RewriteResponse(REWRITE_DONE, node);
   }
@@ -104,6 +126,52 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
+public: //conversion between HO_APPLY AND APPLY_UF
+  // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b)
+  static Node getHoApplyForApplyUf(TNode n) {
+    Assert( n.getKind()==kind::APPLY_UF );
+    Node curr = n.getOperator();
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] );     
+    }
+    return curr;
+  }
+  // converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b)
+  static Node getApplyUfForHoApply(TNode n) {
+    Assert( n.getType().getNumChildren()==2 );
+    std::vector< TNode > children;
+    TNode curr = decomposeHoApply( n, children, true );
+    // if operator is standard
+    if( canUseAsApplyUfOperator( curr ) ){
+      return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+    }
+    // cannot construct APPLY_UF if operator is partially applied or is not standard       
+    return Node::null();
+  }
+  // collects arguments into args, returns operator of a curried HO_APPLY node
+  static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) {
+    TNode curr = n;
+    while( curr.getKind() == kind::HO_APPLY ){
+      args.push_back( curr[1] );
+      curr = curr[0];        
+    }
+    if( opInArgs ){
+      args.push_back( curr );
+    }
+    std::reverse( args.begin(), args.end() );
+    return curr;
+  }
+  /** returns true if this node can be used as an operator of an APPLY_UF node.  In higher-order logic,
+   * terms can have function types and not just variables. 
+   * Currently, we want only free variables to be used as operators of APPLY_UF nodes. This is motivated by
+   * E-matching, ite-lifting among other things.  For example:
+   * f: Int -> Int, g : Int -> Int
+   * forall x : ( Int -> Int ), y : Int. (x y) = (f 0)
+   * Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not.
+   */
+  static inline bool canUseAsApplyUfOperator(TNode n){
+    return n.isVar() && n.getKind()!=kind::BOUND_VARIABLE;
+  }
 };/* class TheoryUfRewriter */
 
 }/* CVC4::theory::uf namespace */

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index c31de403c855764baa81e364d0ddfb8ab97b31c4..e0e199288f95b190bdba22751a30db7917df743b 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -139,6 +139,41 @@ class CardinalityValueTypeRule {
   }
 }; /* class CardinalityValueTypeRule */
 
+// class with the typing rule for HO_APPLY terms
+class HoApplyTypeRule {
+ public:
+  // the typing rule for HO_APPLY terms
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+                                     bool check) {
+    Assert( n.getKind()==kind::HO_APPLY );
+    TypeNode fType = n[0].getType(check);
+    if (!fType.isFunction()) {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument does not have function type");
+    }
+    Assert( fType.getNumChildren()>=2 );
+    if (check) {
+      TypeNode aType = n[1].getType(check);
+      if( !aType.isSubtypeOf( fType[0] ) ){
+        throw TypeCheckingExceptionPrivate(
+            n, "argument does not match function type");
+      }
+    }
+    if( fType.getNumChildren()==2 ){
+      return fType.getRangeType();
+    }else{
+      std::vector< TypeNode > children;
+      TypeNode::iterator argument_type_it = fType.begin();
+      TypeNode::iterator argument_type_it_end = fType.end();
+      ++argument_type_it;
+      for (; argument_type_it != argument_type_it_end; ++argument_type_it) {
+        children.push_back( *argument_type_it );
+      }
+      return nodeManager->mkFunctionType( children );
+    }
+  }
+}; /* class HoApplyTypeRule */
+
 } /* CVC4::theory::uf namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */