diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-16 03:47:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-16 03:47:25 +0000 |
commit | f55dfd4df98fbecbd0ef0f86da79d537457109d6 (patch) | |
tree | 8979e0e92e4d228d285c847f4af4913d4d8a7638 /src/theory | |
parent | b9118b75a8ee24a94a693cd3f850c63eb5085ef1 (diff) |
Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris!
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 10 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 7a45c98aa..23768545d 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -67,7 +67,7 @@ public: size_t selectorIndex = Datatype::indexOf(selectorExpr); size_t constructorIndex = Datatype::indexOf(constructorExpr); const Datatype& dt = Datatype::datatypeOf(constructorExpr); - const Datatype::Constructor& c = dt[constructorIndex]; + const DatatypeConstructor& c = dt[constructorIndex]; if(c.getNumArgs() > selectorIndex && c[selectorIndex].getSelector() == selectorExpr) { Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6b067c681..75980993b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -32,7 +32,7 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons ) +const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons ) { Expr consExpr = cons.toExpr(); return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ]; @@ -272,7 +272,7 @@ void TheoryDatatypes::check(Effort e) { } } if( !cons.isNull() ) { - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first ); NodeBuilder<> nb(kind::OR); @@ -464,7 +464,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) vector< Node > selectorVals; selectorVals.push_back( cons ); bool foundSel = false; - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); for( unsigned int i=0; i<cn.getNumArgs(); i++ ) { Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); if( d_selectors.find( s ) != d_selectors.end() ) { @@ -480,7 +480,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) 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())]; + const DatatypeConstructor& 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; @@ -537,7 +537,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) { Node sel = t.getOperator(); TypeNode selType = sel.getType(); Node cons = getConstructorForSelector( sel ); - const Datatype::Constructor& cn = getConstructor( cons ); + const DatatypeConstructor& cn = getConstructor( cons ); Node tmp = find( t[0] ); Node retNode = t; if( tmp.getKind() == APPLY_CONSTRUCTOR ) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 433af38c3..4d429bc54 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -65,7 +65,7 @@ private: /** has seen cycle */ context::CDO< bool > d_hasSeenCycle; /** get the constructor for the node */ - const Datatype::Constructor& getConstructor( Node cons ); + const DatatypeConstructor& getConstructor( Node cons ); /** get the constructor for the selector */ Node getConstructorForSelector( Node sel ); |