diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 114 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 |
3 files changed, 77 insertions, 60 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 3228d55f6..da28b1ffd 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -88,6 +88,7 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { Trace("builtin-rewrite") << " array rep : " << anode << ", constant = " << anode.isConst() << std::endl; Assert( anode.isConst()==retNode.isConst() ); Assert( retNode.getType()==node.getType() ); + Assert(node.hasFreeVar() == retNode.hasFreeVar()); return RewriteResponse(REWRITE_DONE, retNode); } }else{ @@ -192,7 +193,9 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl } } -Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ){ +Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, + TypeNode retType) +{ Assert( n.getKind()==kind::LAMBDA ); Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl; @@ -230,7 +233,9 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool re // non-equality condition Trace("builtin-rewrite-debug2") << " ...non-equality condition." << std::endl; return Node::null(); - }else if( reqConst && Rewriter::rewrite( index_eq )!=index_eq ){ + } + else if (Rewriter::rewrite(index_eq) != index_eq) + { // equality must be oriented correctly based on rewriter Trace("builtin-rewrite-debug2") << " ...equality not oriented properly." << std::endl; return Node::null(); @@ -241,7 +246,8 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool re Node arg = index_eq[r]; Node val = index_eq[1-r]; if( arg==first_arg ){ - if( reqConst && !val.isConst() ){ + if (!val.isConst()) + { // non-constant value Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl; return Node::null(); @@ -255,7 +261,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool re if( !curr_index.isNull() ){ if( !rec_bvl.isNull() ){ curr_val = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr_val ); - curr_val = getArrayRepresentationForLambdaRec( curr_val, reqConst, retType ); + curr_val = getArrayRepresentationForLambdaRec(curr_val, retType); if( curr_val.isNull() ){ Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl; return Node::null(); @@ -274,7 +280,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool re } if( !rec_bvl.isNull() ){ curr = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr ); - curr = getArrayRepresentationForLambdaRec( curr, reqConst, retType ); + curr = getArrayRepresentationForLambdaRec(curr, retType); } if( !curr.isNull() && curr.isConst() ){ // compute the return type @@ -302,11 +308,12 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool re } } -Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){ +Node TheoryBuiltinRewriter::getArrayRepresentationForLambda(TNode n) +{ Assert( n.getKind()==kind::LAMBDA ); // must carry the overall return type to deal with cases like (lambda ((x Int)(y Int)) (ite (= x _) 0.5 0.0)), // where the inner construction for the else case about should be (arraystoreall (Array Int Real) 0.0) - return getArrayRepresentationForLambdaRec( n, reqConst, n[1].getType() ); + return getArrayRepresentationForLambdaRec(n, n[1].getType()); } }/* CVC4::theory::builtin namespace */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 79ae825e9..8f45cc0fd 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -60,60 +60,70 @@ private: static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, std::unordered_map< TNode, Node, TNodeHashFunction >& visited ); /** recursive helper for getArrayRepresentationForLambda */ - static Node getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ); -public: - /** Get function type for array type - * - * This returns the function type of terms returned by the function - * getLambdaForArrayRepresentation( t, bvl ), - * where t.getType()=atn. - * - * bvl should be a bound variable list whose variables correspond in-order - * to the index types of the (curried) Array type. For example, a bound - * variable list bvl whose variables have types (Int, Real) can be given as - * input when paired with atn = (Array Int (Array Real Bool)), or (Array Int - * (Array Real (Array Bool Bool))). This function returns (-> Int Real Bool) - * and (-> Int Real (Array Bool Bool)) respectively in these cases. - * On the other hand, the above bvl is not a proper input for - * atn = (Array Int (Array Bool Bool)) or (Array Int Int). - * If the types of bvl and atn do not match, we throw an assertion failure. - */ - static TypeNode getFunctionTypeForArrayType(TypeNode atn, Node bvl); - /** Get array type for function type - * - * This returns the array type of terms returned by - * getArrayRepresentationForLambda( t ), where t.getType()=ftn. - */ - static TypeNode getArrayTypeForFunctionType(TypeNode ftn); - /** - * Given an array constant a, returns a lambda expression that it corresponds - * to, with bound variable list bvl. - * Examples: - * - * (store (storeall (Array Int Int) 2) 0 1) - * becomes - * ((lambda x. (ite (= x 0) 1 2)) - * - * (store (storeall (Array Int (Array Int Int)) (storeall (Array Int Int) 4)) 0 - * (store (storeall (Array Int Int) 3) 1 2)) - * becomes - * (lambda xy. (ite (= x 0) (ite (= x 1) 2 3) 4)) - * - * (store (store (storeall (Array Int Bool) false) 2 true) 1 true) - * becomes - * (lambda x. (ite (= x 1) true (ite (= x 2) true false))) - * - * Notice that the return body of the lambda is rewritten to ensure that the - * representation is canonical. Hence the last - * example will in fact be returned as: - * (lambda x. (ite (= x 1) true (= x 2))) - */ - static Node getLambdaForArrayRepresentation(TNode a, TNode bvl); - /** given a lambda expression n, returns an array term. reqConst is true if we - * require the return value to be a constant. + static Node getArrayRepresentationForLambdaRec(TNode n, TypeNode retType); + + public: + /** Get function type for array type + * + * This returns the function type of terms returned by the function + * getLambdaForArrayRepresentation( t, bvl ), + * where t.getType()=atn. + * + * bvl should be a bound variable list whose variables correspond in-order + * to the index types of the (curried) Array type. For example, a bound + * variable list bvl whose variables have types (Int, Real) can be given as + * input when paired with atn = (Array Int (Array Real Bool)), or (Array Int + * (Array Real (Array Bool Bool))). This function returns (-> Int Real Bool) + * and (-> Int Real (Array Bool Bool)) respectively in these cases. + * On the other hand, the above bvl is not a proper input for + * atn = (Array Int (Array Bool Bool)) or (Array Int Int). + * If the types of bvl and atn do not match, we throw an assertion failure. + */ + static TypeNode getFunctionTypeForArrayType(TypeNode atn, Node bvl); + /** Get array type for function type + * + * This returns the array type of terms returned by + * getArrayRepresentationForLambda( t ), where t.getType()=ftn. + */ + static TypeNode getArrayTypeForFunctionType(TypeNode ftn); + /** + * Given an array constant a, returns a lambda expression that it corresponds + * to, with bound variable list bvl. + * Examples: + * + * (store (storeall (Array Int Int) 2) 0 1) + * becomes + * ((lambda x. (ite (= x 0) 1 2)) + * + * (store (storeall (Array Int (Array Int Int)) (storeall (Array Int Int) 4)) + * 0 (store (storeall (Array Int Int) 3) 1 2)) becomes (lambda xy. (ite (= x + * 0) (ite (= x 1) 2 3) 4)) + * + * (store (store (storeall (Array Int Bool) false) 2 true) 1 true) + * becomes + * (lambda x. (ite (= x 1) true (ite (= x 2) true false))) + * + * Notice that the return body of the lambda is rewritten to ensure that the + * representation is canonical. Hence the last + * example will in fact be returned as: + * (lambda x. (ite (= x 1) true (= x 2))) + */ + static Node getLambdaForArrayRepresentation(TNode a, TNode bvl); + /** + * Given a lambda expression n, returns an array term that corresponds to n. * This does the opposite direction of the examples described above. + * + * We limit the return values of this method to be almost constant functions, + * that is, arrays of the form: + * (store ... (store (storeall _ b) i1 e1) ... in en) + * where b, i1, e1, ..., in, en are constants. + * Notice however that the return value of this form need not be a (canonical) + * array constant. + * + * If it is not possible to construct an array of this form that corresponds + * to n, this method returns null. */ - static Node getArrayRepresentationForLambda(TNode n, bool reqConst = false); + static Node getArrayRepresentationForLambda(TNode n); };/* class TheoryBuiltinRewriter */ }/* CVC4::theory::builtin namespace */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index bd3e5faa4..c471caf86 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -170,7 +170,7 @@ class LambdaTypeRule { { Assert(n.getKind() == kind::LAMBDA); //get array representation of this function, if possible - Node na = TheoryBuiltinRewriter::getArrayRepresentationForLambda( n, true ); + Node na = TheoryBuiltinRewriter::getArrayRepresentationForLambda(n); if( !na.isNull() ){ Assert( na.getType().isArray() ); Trace("lambda-const") << "Array representation for " << n << " is " << na << " " << na.getType() << std::endl; |