From: Andrew Reynolds Date: Thu, 14 Sep 2017 02:08:28 +0000 (-0500) Subject: Add new kinds required for higher-order. (#1083) X-Git-Tag: cvc5-1.0.0~5640 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=daf1d6bf1176834fa697dd57c6fe28142e715585;p=cvc5.git 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 e2d740e20..500295a0c 100644 --- 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 0bd502205..db2f735c6 100644 --- 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 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; imkNode( 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& 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 c31de403c..e0e199288 100644 --- 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 */