summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-09-14 14:12:22 -0500
committerGitHub <noreply@github.com>2017-09-14 14:12:22 -0500
commitab2924e8a6cc34f29167b1ff50273d59dd7a6707 (patch)
treed9902a389ae70a21f2d5a3f7acde2ce658fb534d /src/theory
parente4fc6c7b57668f18ce087c45e001c101375c20ea (diff)
Remove unhandled subtypes (#1098)
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception). * Update unit test for parametric datatypes to reflect new subtyping relation. * Remove deprecated test. * Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp26
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.h2
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h67
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h3
4 files changed, 63 insertions, 35 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 57249e181..4948216e5 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -150,7 +150,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl
}
}
-Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){
+Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ){
Assert( n.getKind()==kind::LAMBDA );
Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl;
@@ -165,7 +165,6 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
}
Trace("builtin-rewrite-debug2") << " process body..." << std::endl;
- TypeNode retType;
std::vector< Node > conds;
std::vector< Node > vals;
Node curr = n[1];
@@ -214,7 +213,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
if( !curr_index.isNull() ){
if( !rec_bvl.isNull() ){
curr_val = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr_val );
- curr_val = getArrayRepresentationForLambda( curr_val, reqConst );
+ curr_val = getArrayRepresentationForLambdaRec( curr_val, reqConst, retType );
if( curr_val.isNull() ){
Trace("builtin-rewrite-debug2") << " ...non-constant value." << std::endl;
return Node::null();
@@ -228,18 +227,22 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
conds.push_back( curr_index );
vals.push_back( curr_val );
TypeNode vtype = curr_val.getType();
- retType = retType.isNull() ? vtype : TypeNode::leastCommonTypeNode( retType, vtype );
//recurse
curr = next;
}
if( !rec_bvl.isNull() ){
curr = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr );
- curr = getArrayRepresentationForLambda( curr );
+ curr = getArrayRepresentationForLambdaRec( curr, reqConst, retType );
}
if( !curr.isNull() && curr.isConst() ){
- TypeNode ctype = curr.getType();
- retType = retType.isNull() ? ctype : TypeNode::leastCommonTypeNode( retType, ctype );
- TypeNode array_type = NodeManager::currentNM()->mkArrayType( first_arg.getType(), retType );
+ // compute the return type
+ TypeNode array_type = retType;
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ unsigned index = (n[0].getNumChildren()-1)-i;
+ array_type = NodeManager::currentNM()->mkArrayType( n[0][index].getType(), array_type );
+ }
+ Trace("builtin-rewrite-debug2") << " make array store all " << curr.getType() << " annotated : " << array_type << std::endl;
+ Assert( curr.getType().isSubtypeOf( array_type.getArrayConstituentType() ) );
curr = NodeManager::currentNM()->mkConst(ArrayStoreAll(((ArrayType)array_type.toType()), curr.toExpr()));
Trace("builtin-rewrite-debug2") << " build array..." << std::endl;
// can only build if default value is constant (since array store all must be constant)
@@ -257,6 +260,13 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
}
}
+Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){
+ 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() );
+}
+
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index d9ae5b447..3667cf159 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -59,6 +59,8 @@ private:
/** recursive helper for getLambdaForArrayRepresentation */
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:
/**
* Given an array constant a, returns a lambda expression that it corresponds to, with bound variable list bvl.
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 025fe0349..49e8a6888 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -36,29 +36,11 @@ public:
Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
+ /*
TypeNode tn = in.getType();
Type t = tn.toType();
DatatypeType dt = DatatypeType(t);
- //check for parametric datatype constructors
- // to ensure a normal form, all parameteric datatype constructors must have a type ascription
- if( dt.isParametric() ){
- if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
- Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
- Node op = in.getOperator();
- //get the constructor object
- const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
- //create ascribed constructor type
- Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t)));
- Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op );
- //make new node
- std::vector< Node > children;
- children.push_back( op_new );
- children.insert( children.end(), in.begin(), in.end() );
- Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
- Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
- return RewriteResponse(REWRITE_DONE, inr);
- }
- }
+ // enable this rewrite if we support subtypes of tuples
if( tn.isTuple() ){
Node nn = normalizeTupleConstructorApp( in );
if( nn!=in ){
@@ -66,6 +48,7 @@ public:
return RewriteResponse(REWRITE_AGAIN_FULL, nn);
}
}
+ */
if( in.isConst() ){
Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl;
Node inn = normalizeConstant( in );
@@ -241,6 +224,33 @@ public:
static RewriteResponse preRewrite(TNode in) {
Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
+ //must prewrite to apply type ascriptions since rewriting does not preserve types
+ if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
+ TypeNode tn = in.getType();
+ Type t = tn.toType();
+ DatatypeType dt = DatatypeType(t);
+
+ //check for parametric datatype constructors
+ // to ensure a normal form, all parameteric datatype constructors must have a type ascription
+ if( dt.isParametric() ){
+ if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
+ Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
+ Node op = in.getOperator();
+ //get the constructor object
+ const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
+ //create ascribed constructor type
+ Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t)));
+ Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op );
+ //make new node
+ std::vector< Node > children;
+ children.push_back( op_new );
+ children.insert( children.end(), in.begin(), in.end() );
+ Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+ Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
+ return RewriteResponse(REWRITE_DONE, inr);
+ }
+ }
+ }
return RewriteResponse(REWRITE_DONE, in);
}
@@ -251,10 +261,11 @@ public:
Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
if( n1.getOperator() != n2.getOperator()) {
- if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
- Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
- return true;
- }
+ //enable this check if we support subtypes with tuples
+ //if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
+ Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
+ return true;
+ //}
}
Assert( n1.getNumChildren() == n2.getNumChildren() );
for( unsigned i=0; i<n1.getNumChildren(); i++ ) {
@@ -649,9 +660,11 @@ public:
static Node normalizeConstant( Node n ){
TypeNode tn = n.getType();
if( tn.isDatatype() ){
- if( tn.isTuple() ){
- return normalizeTupleConstructorApp( n );
- }else if( tn.isCodatatype() ){
+ // enable this if we support subtyping with tuples
+ //if( tn.isTuple() ){
+ // return normalizeTupleConstructorApp( n );
+ //}
+ if( tn.isCodatatype() ){
return normalizeCodatatypeConstant( n );
}else{
std::vector< Node > children;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index e787ebc49..d6045404d 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -101,6 +101,8 @@ struct DatatypeConstructorTypeRule {
return false;
}
}
+ //if we support subtyping for tuples, enable this
+ /*
//check whether it is in normal form?
TypeNode tn = n.getType();
if( tn.isTuple() ){
@@ -114,6 +116,7 @@ struct DatatypeConstructorTypeRule {
}else if( tn.isCodatatype() ){
//TODO?
}
+ */
return true;
}
}; /* struct DatatypeConstructorTypeRule */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback