From: Andrew Reynolds Date: Fri, 26 Oct 2012 22:19:20 +0000 (+0000) Subject: bug fix for parametric datatypes, previously datatypes theory/rewriter was not recogn... X-Git-Tag: cvc5-1.0.0~7661 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2333e3bb49f84be01ddcc875dc6b01cc6b29307;p=cvc5.git bug fix for parametric datatypes, previously datatypes theory/rewriter was not recognizing parametric datatype types as being datatype types --- diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 21d4f0d07..42b999561 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -31,12 +31,12 @@ class DatatypesRewriter { public: static RewriteResponse postRewrite(TNode in) { - Debug("datatypes-rewrite") << "post-rewriting " << in << std::endl; + Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl; if(in.getKind() == kind::APPLY_TESTER) { if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) { bool result = Datatype::indexOf(in.getOperator().toExpr()) == Datatype::indexOf(in[0].getOperator().toExpr()); - Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " << "Rewrite trivial tester " << in << " " << result << std::endl; return RewriteResponse(REWRITE_DONE, @@ -45,7 +45,7 @@ public: const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype(); if(dt.getNumConstructors() == 1) { // only one constructor, so it must be - Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " << "only one ctor for " << dt.getName() << " and that is " << dt[0].getName() << std::endl; @@ -69,7 +69,7 @@ public: const DatatypeConstructor& c = dt[constructorIndex]; if(c.getNumArgs() > selectorIndex && c[selectorIndex].getSelector() == selectorExpr) { - Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " << "Rewrite trivial selector " << in << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); @@ -82,7 +82,7 @@ public: gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); } - Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " << "Rewrite trivial selector " << in << " to distinguished ground term " << in.getType().mkGroundTerm() << std::endl; @@ -105,7 +105,7 @@ public: } static RewriteResponse preRewrite(TNode in) { - Debug("datatypes-rewrite") << "pre-rewriting " << in << std::endl; + Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl; return RewriteResponse(REWRITE_DONE, in); } @@ -124,7 +124,7 @@ public: } } } - }else if( !n1.getType().isDatatype() ){ + }else if( !isTermDatatype( n1 ) ){ //also check for clashes between non-datatypes Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); eq = Rewriter::rewrite( eq ); @@ -134,7 +134,11 @@ public: } return false; } - + /** is this term a datatype */ + static bool isTermDatatype( Node n ){ + TypeNode tn = n.getType(); + return tn.isDatatype() || tn.isParametricDatatype(); + } };/* class DatatypesRewriter */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 34e7c6f11..6b576cba8 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -34,54 +34,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -void TheoryDatatypes::printModelDebug( const char* c ){ - Trace( c ) << "Datatypes model : " << std::endl; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - if( eqc.getType().isDatatype()){ - Trace( c ) << "DATATYPE : "; - } - Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; - Trace( c ) << " { "; - //add terms to model - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Trace( c ) << (*eqc_i) << " "; - ++eqc_i; - } - Trace( c ) << "}" << std::endl; - if( eqc.getType().isDatatype() ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; - if( ei->d_constructor.get().isNull() ){ - Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; - Trace( c ) << " Constructor : " << std::endl; - Trace( c ) << " Labels : "; - if( hasLabel( ei, eqc ) ){ - Trace( c ) << getLabel( eqc ); - }else{ - NodeListMap::iterator lbl_i = d_labels.find( eqc ); - if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ - Trace( c ) << *j << " "; - } - } - } - Trace( c ) << std::endl; - }else{ - Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; - } - Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; - } - } - ++eqcs_i; - } -} - TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe), @@ -148,7 +100,7 @@ void TheoryDatatypes::check(Effort e) { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node n = (*eqcs_i); - if( n.getType().isDatatype() ){ + if( DatatypesRewriter::isTermDatatype( n ) ){ EqcInfo* eqc = getOrMakeEqcInfo( n, true ); //if there are more than 1 possible constructors for eqc if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) { @@ -184,6 +136,7 @@ void TheoryDatatypes::check(Effort e) { if( !needSplit && mustSpecifyModel() ){ //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type + //** TODO: this is probably not good enough, actually need fair enumeration strategy Node groundTerm = n.getType().mkGroundTerm(); int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); if( pcons[index] ){ @@ -396,7 +349,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){ /** called when two equivalance classes have merged */ void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){ - if( t1.getType().isDatatype() ){ + if( DatatypesRewriter::isTermDatatype( t1 ) ){ d_pending_merge.push_back( t1.eqNode( t2 ) ); } } @@ -683,7 +636,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); //for all equivalence classes that are datatypes - if( eqc.getType().isDatatype() ){ + if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( ei ){ if( !ei->d_constructor.get().isNull() ){ @@ -928,7 +881,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ addLemma = dt.involvesExternalType(); #else for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ - if( !n[1][j].getType().isDatatype() ){ + if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ addLemma = true; break; } @@ -979,3 +932,52 @@ Node TheoryDatatypes::getRepresentative( Node a ){ return a; } } + + +void TheoryDatatypes::printModelDebug( const char* c ){ + Trace( c ) << "Datatypes model : " << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + Trace( c ) << "DATATYPE : "; + } + Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; + Trace( c ) << " { "; + //add terms to model + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Trace( c ) << (*eqc_i) << " "; + ++eqc_i; + } + Trace( c ) << "}" << std::endl; + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; + if( ei->d_constructor.get().isNull() ){ + Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; + Trace("model-warn") << " Type : " << eqc.getType() << std::endl; + Trace( c ) << " Constructor : " << std::endl; + Trace( c ) << " Labels : "; + if( hasLabel( ei, eqc ) ){ + Trace( c ) << getLabel( eqc ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( eqc ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ + Trace( c ) << *j << " "; + } + } + } + Trace( c ) << std::endl; + }else{ + Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; + } + Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; + } + } + ++eqcs_i; + } +}