From daa163e694d257ffe8ba7ae8ccb240bcbfb1c276 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Jun 2011 19:56:12 +0000 Subject: [PATCH] fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working --- src/parser/cvc/Cvc.g | 2 +- src/theory/datatypes/theory_datatypes.cpp | 38 +++++++++--------- src/theory/datatypes/theory_datatypes.h | 1 - .../datatypes/theory_datatypes_type_rules.h | 39 ++++++++++++------- src/util/datatype.cpp | 31 ++++++++++----- src/util/matcher.h | 26 +++++++------ 6 files changed, 80 insertions(+), 57 deletions(-) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d6165b435..cd4c66664 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1467,7 +1467,7 @@ postfixTerm[CVC4::Expr& f] Expr e = f.getOperator(); const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator()[0] )); + MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() )); v.insert(v.end(), f.begin(), f.end()); f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); } else { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 20668a5ff..6aed9e9fa 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -120,7 +120,7 @@ void TheoryDatatypes::check(Effort e) { while(!done()) { Node assertion = get(); if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") - || Debug.isOn("datatypes-debug-pf") ) { + || Debug.isOn("datatypes-debug-pf") || Debug.isOn("datatypes-conflict") ) { cout << "*** TheoryDatatypes::check(): " << assertion << endl; d_currAsserts.push_back( assertion ); } @@ -211,7 +211,10 @@ void TheoryDatatypes::check(Effort e) { //if there is now a conflict if( hasConflict() ) { Debug("datatypes-conflict") << "Constructing conflict..." << endl; - Debug("datatypes-conflict") << d_cc << std::endl; + for( int i=0; i<(int)d_currAsserts.size(); i++ ) { + Debug("datatypes-conflict") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl; + } + //Debug("datatypes-conflict") << d_cc << std::endl; Node conflict = d_em.getConflict(); if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){ @@ -472,9 +475,19 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) } if( cn.isFinite() || foundSel ) { d_inst_map[ te ] = true; - //instantiate, add equality Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); - val = doTypeAscription( val, te.getType() ); //IDT-param + //instantiate, add equality + if( val.getType()!=te.getType() ){ //IDT-param + Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() ); + Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl; + const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())]; + Debug("datatypes-gt") << "constructor is " << dtc << std::endl; + Type tspec = dtc.getSpecializedConstructorType(te.getType().toType()); + Debug("datatypes-gt") << "tpec is " << tspec << std::endl; + selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), cons); + val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); + } if( find( val ) != find( te ) ) { //build explaination NodeBuilder<> nb(kind::AND); @@ -533,8 +546,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) { retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ]; } else { Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl; - retNode = doTypeAscription( retTyp.mkGroundTerm(), selType[1] ); //IDT-param - //retNode = selType[1].mkGroundTerm(); + retNode = retTyp.mkGroundTerm(); //IDT-param } if( tmp!=t[0] ){ t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp ); @@ -577,8 +589,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) { tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] ); d_em.addNode( tester.notNode(), exp, Reason::idt_tcong ); } - retNode = doTypeAscription( retTyp.mkGroundTerm(), retTyp ); //IDT-param - //retNode = selType[1].mkGroundTerm(); + retNode = retTyp.mkGroundTerm(); //IDT-param Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 ); @@ -1048,14 +1059,3 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, } return false; } - -Node TheoryDatatypes::doTypeAscription( Node t, TypeNode typ ) -{ - TypeNode tt = t.getType(); - if( (tt.isDatatype() || tt.isParametricDatatype()) && !tt.isInstantiatedDatatype() ){ - return NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(typ.toType())), t); - }else{ - return t; - } -} diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 9dfb8c818..1b9e357ed 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -178,7 +178,6 @@ private: bool searchForCycle( Node n, Node on, std::map< Node, bool >& visited, NodeBuilder<>& explanation ); - Node doTypeAscription( Node t, TypeNode typ ); };/* class TheoryDatatypes */ inline bool TheoryDatatypes::hasConflict() { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 5ff01924b..578de69a2 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -163,22 +163,33 @@ struct DatatypeAscriptionTypeRule { TypeNode t = TypeNode::fromType(n.getOperator().getConst().getType()); if(check) { TypeNode childType = n[0].getType(check); - if(!t.getKind() == kind::DATATYPE_TYPE) { - throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription"); + //if(!t.getKind() == kind::DATATYPE_TYPE) { + // throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription"); + //} + //DatatypeType dt = DatatypeType(childType.toType()); + //if( dt.isParametric() ){ + // Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl; + // Matcher m( dt ); + // if( !m.doMatching( childType, t ) ){ + // throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); + // } + //}else{ + // Debug("typecheck-idt") << "typecheck test: " << n << std::endl; + // if(t != childType) { + // throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument"); + // } + //} + + Matcher m; + if( childType.getKind() == kind::CONSTRUCTOR_TYPE ){ + m.addTypesFromDatatype( ConstructorType(childType.toType()).getRangeType() ); + }else if( childType.getKind() == kind::DATATYPE_TYPE ){ + m.addTypesFromDatatype( DatatypeType(childType.toType()) ); } - DatatypeType dt = DatatypeType(childType.toType()); - if( dt.isParametric() ){ - Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl; - Matcher m( dt ); - if( !m.doMatching( childType, t ) ){ - throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); - } - }else{ - Debug("typecheck-idt") << "typecheck test: " << n << std::endl; - if(t != childType) { - throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument"); - } + if( !m.doMatching( childType, t ) ){ + throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); } + } return t; } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index a06a7c2b5..926f31847 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -52,6 +52,7 @@ typedef expr::Attribute Dataty typedef expr::Attribute DatatypeGroundTermAttr; const Datatype& Datatype::datatypeOf(Expr item) { + ExprManagerScope ems(item); TypeNode t = Node::fromExpr(item).getType(); switch(t.getKind()) { case kind::CONSTRUCTOR_TYPE: @@ -65,14 +66,19 @@ const Datatype& Datatype::datatypeOf(Expr item) { } size_t Datatype::indexOf(Expr item) { + ExprManagerScope ems(item); AssertArgument(item.getType().isConstructor() || item.getType().isTester() || item.getType().isSelector(), item, "arg must be a datatype constructor, selector, or tester"); TNode n = Node::fromExpr(item); - Assert(n.hasAttribute(DatatypeIndexAttr())); - return n.getAttribute(DatatypeIndexAttr()); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return indexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeIndexAttr())); + return n.getAttribute(DatatypeIndexAttr()); + } } void Datatype::resolve(ExprManager* em, @@ -201,7 +207,8 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { // prefer the nullary constructor if( groundTerm.isNull() && (*i).getNumArgs() == 0) { - groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor()); + groundTerm = d_constructors[indexOf((*i).getConstructor())].mkGroundTerm( t ); + //groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor()); self.setAttribute(DatatypeGroundTermAttr(), groundTerm); Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl; } @@ -261,10 +268,6 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { // if we get all the way here, we aren't well-founded CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!"); }else{ - if( t!=groundTerm.getType() ){ - groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr(); - } return groundTerm; } } @@ -522,7 +525,7 @@ Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const vector subst; m.getMatches(subst); vector params = dt.getParameters(); - return d_constructor.getType().substitute(subst, params); + return d_constructor.getType().substitute(params, subst); } Expr Datatype::Constructor::getTester() const { @@ -615,7 +618,6 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - Debug("datatypes-gt") << "mkGroundTerm " << t << std::endl; // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -652,8 +654,17 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio } groundTerms.push_back(selType.mkGroundTerm()); } - + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + if( groundTerm.getType()!=t ){ + Assert( Datatype::datatypeOf( d_constructor ).isParametric() ); + //type is ambiguous, must apply type ascription + Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl; + groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))), + groundTerms[0]); + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + } self.setAttribute(DatatypeGroundTermAttr(), groundTerm); return groundTerm; } diff --git a/src/util/matcher.h b/src/util/matcher.h index 2c55309d3..5dc511bc2 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -38,6 +38,11 @@ private: public: Matcher(){} Matcher( DatatypeType dt ){ + addTypesFromDatatype( dt ); + } + ~Matcher(){} + + void addTypesFromDatatype( DatatypeType dt ){ std::vector< Type > argTypes = dt.getParamTypes(); addTypes( argTypes ); Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl; @@ -48,8 +53,6 @@ public: } } } - ~Matcher(){} - void addType( Type t ){ d_types.push_back( TypeNode::fromType( t ) ); d_match.push_back( TypeNode::null() ); @@ -60,25 +63,24 @@ public: } } - bool doMatching( TypeNode base, TypeNode match ){ - Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl; - std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base ); + bool doMatching( TypeNode pattern, TypeNode tn ){ + Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl; + std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern ); if( i!=d_types.end() ){ int index = i - d_types.begin(); - Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl; - if( !d_match[index].isNull() && d_match[index]!=match ){ + if( !d_match[index].isNull() && d_match[index]!=tn ){ return false; }else{ - d_match[ i - d_types.begin() ] = match; + d_match[ i - d_types.begin() ] = tn; return true; } - }else if( base==match ){ + }else if( pattern==tn ){ return true; - }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){ + }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){ return false; }else{ - for( int i=0; i<(int)base.getNumChildren(); i++ ){ - if( !doMatching( base[i], match[i] ) ){ + for( int i=0; i<(int)pattern.getNumChildren(); i++ ){ + if( !doMatching( pattern[i], tn[i] ) ){ return false; } } -- 2.30.2