diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-22 23:21:40 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-22 23:21:40 +0100 |
commit | 76da4764db903c503ac339584db667aa50748179 (patch) | |
tree | 1c7f35e8ee0804aaf08679daac8ad2ef9f3b8b09 /src | |
parent | 1eef0f8d079e40cf9eac76e70399908d75dc11bc (diff) |
Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 24 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 22 | ||||
-rw-r--r-- | src/util/datatype.cpp | 1 |
3 files changed, 14 insertions, 33 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 0bbb97076..02339dc26 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -143,20 +143,22 @@ public: if( in.getType().isSort() ){ TypeEnumerator te(in.getType()); gt = *te; - }else{ + }else if( dt.isWellFounded() || in[0].isConst() ){ gt = in.getType().mkGroundTerm(); } - TypeNode gtt = gt.getType(); - //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + if( !gt.isNull() ){ + TypeNode gtt = gt.getType(); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); } } if(in.getKind() == kind::DT_SIZE && in[0].getKind()==kind::APPLY_CONSTRUCTOR ){ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index edb548ca4..0429c3aab 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -802,28 +802,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } } } - //add this to the transitive closure module - Node oldRep = trep2; - Node newRep = trep1; - if( trep1.getKind()!=APPLY_CONSTRUCTOR && trep2.getKind()==APPLY_CONSTRUCTOR ){ - oldRep = trep1; - newRep = trep2; - } - /* - bool result = d_cycle_check.addEdgeNode( oldRep, newRep ); - //d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl; - if( result ){ - checkCycles(); - if( d_conflict ){ - Debug("datatypes-cycles-find") << "Cycle found." << std::endl; - return; - }else{ - Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl; - d_cycle_check.debugPrint(); - } - } - */ } } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index f0704520a..7813626a7 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -228,6 +228,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); + Debug("datatypes") << "dt mkGroundTerm " << t << std::endl; TypeNode self = TypeNode::fromType(d_self); |