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{
}
}
-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;
// 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();
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();
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();
}
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
}
}
-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 */
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 */
projects / cvc5.git / commitdiff