diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-20 15:29:55 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-20 15:30:02 +0200 |
commit | bb41d77bae405cad83ee26b85cda7ad84e0abb14 (patch) | |
tree | 8ad17e2d7ab3005e92e349f756f785a34c9ee976 /src | |
parent | 4ea0a9a8c26970649dfa207eebd1add755948c7d (diff) |
Minor cleanup in datatypes.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 15 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 38 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 |
3 files changed, 19 insertions, 36 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index c8ce9833c..0bbb97076 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -269,7 +269,7 @@ public: return false; } /** get instantiate cons */ - static Node getInstCons( Node n, const Datatype& dt, int index, bool mkVar = false ) { + static Node getInstCons( Node n, const Datatype& dt, int index ) { Type tspec; if( dt.isParametric() ){ tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); @@ -278,13 +278,6 @@ public: children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ Node nc = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); - if( mkVar ){ - TypeNode tn = nc.getType(); - if( dt.isParametric() ){ - tn = TypeNode::fromType( tspec )[i]; - } - nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created for inst cons" ); - } children.push_back( nc ); } Node n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); @@ -319,6 +312,12 @@ public: } return false; } + static Node mkTester( Node n, int i, const Datatype& dt ){ + //Node ret = n.eqNode( DatatypesRewriter::getInstCons( n, dt, i ) ); + //Assert( isTester( ret )==i ); + Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n ); + return ret; + } static bool isNullaryApplyConstructor( Node n ){ Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); for( unsigned i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 06d07f425..62f5ad3ff 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -216,14 +216,14 @@ void TheoryDatatypes::check(Effort e) { if( needSplit && consIndex!=-1 ) { //if only one constructor, then this term must be this constructor if( dt.getNumConstructors()==1 ){ - Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); + Node t = DatatypesRewriter::mkTester( n, 0, dt ); d_pending.push_back( t ); d_pending_exp[ t ] = d_true; Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ if( options::dtBinarySplit() ){ - Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); + Node test = DatatypesRewriter::mkTester( n, consIndex, dt ); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; test = Rewriter::rewrite( test ); NodeBuilder<> nb(kind::OR); @@ -235,7 +235,7 @@ void TheoryDatatypes::check(Effort e) { Trace("dt-split") << "*************Split for constructors on " << n << endl; std::vector< Node > children; for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n ); + Node test = DatatypesRewriter::mkTester( n, i, dt ); children.push_back( test ); } Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children ); @@ -954,7 +954,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ } } } - Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); + Node t_concl = DatatypesRewriter::mkTester( tt[0], testerIndex, dt ); Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_pending.push_back( t_concl ); d_pending_exp[ t_concl ] = t_concl_exp; @@ -1093,23 +1093,7 @@ void TheoryDatatypes::computeCareGraph(){ break; }else if( !areEqual( x, y ) ){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; - //check if they are definately disequal - bool defDiseq = false; -/* - TNode rx = getRepresentative( x ); - EqcInfo* eix = getOrMakeEqcInfo( rx, false ); - if( eix ){ - TNode ry = getRepresentative( y ); - EqcInfo* eiy = getOrMakeEqcInfo( ry, false ); - if( eiy ){ - if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){ - defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator(); - }else{ - } - } - } -*/ - if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ + if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); if( eqStatus!=EQUALITY_UNKNOWN ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); @@ -1283,7 +1267,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ for( unsigned i=0; i<pcons.size(); i++ ){ //must try the infinite ones first if( pcons[i] && (r==1)==dt[ i ].isFinite() ){ - neqc = getInstantiateCons( eqc, dt, i, false, false ); + neqc = getInstantiateCons( eqc, dt, i, false ); for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ @@ -1415,7 +1399,7 @@ void TheoryDatatypes::collectTerms( Node n ) { const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ - Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); + Node test = DatatypesRewriter::mkTester( n[0], i, dt ); children.push_back( test ); } } @@ -1442,13 +1426,13 @@ void TheoryDatatypes::processNewTerm( Node n ){ } } -Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){ +Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool isActive ){ std::map< int, Node >::iterator it = d_inst_map[n].find( index ); if( it!=d_inst_map[n].end() ){ return it->second; }else{ //add constructor to equivalence class - Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar ); + Node n_ic = DatatypesRewriter::getInstCons( n, dt, index ); if( isActive ){ for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){ processNewTerm( n_ic[i] ); @@ -1480,7 +1464,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() //instantiate this equivalence class eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index, false, true ); + Node tt_cons = getInstantiateCons( tt, dt, index, true ); Node eq; if( tt!=tt_cons ){ eq = tt.eqNode( tt_cons ); @@ -1763,7 +1747,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ // (4) collapse selector : S( C( t1...tn ) ) = t' // (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn ) // (6) non-negative size : 0 <= size( t ) - //We may need to communicate (3) outwards if the conclusions involve other theories. Also communicate (5) and (6). + //We may need to communicate (3) outwards if the conclusions involve other theories. Also communicate (5), (6), and OR conclusions. Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; bool addLemma = false; if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index d698e80c9..81cbe7523 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -258,7 +258,7 @@ private: /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ); + Node getInstantiateCons( Node n, const Datatype& dt, int index, bool isActive ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ |