diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-06 14:05:08 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-06 14:05:08 +0100 |
commit | e6a588264154bf4b93abd0aaac39dbf10c496e6f (patch) | |
tree | b2d5f35dc6280419f27b13af007ed8d6e634a069 /src | |
parent | 60e8c65407a34d75ccaa88e1ccbb5adb89799330 (diff) |
Minor fix for getInstCons
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 15 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 |
2 files changed, 6 insertions, 11 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 215eb46ca..22c0477d8 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1279,7 +1279,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 ); + neqc = DatatypesRewriter::getInstCons( eqc, dt, i ); 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] ) ){ @@ -1420,7 +1420,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ } } -Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool isActive ){ +Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){ std::map< int, Node >::iterator it = d_inst_map[n].find( index ); if( it!=d_inst_map[n].end() ){ return it->second; @@ -1435,14 +1435,9 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, d_out->lemma( eq ); } Node n_ic = DatatypesRewriter::getInstCons( k, dt, index ); - if( isActive ){ - for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){ - Assert( n_ic[i]==Rewriter::rewrite( n_ic[i] ) ); - //processNewTerm( n_ic[i] ); - } - collectTerms( n_ic ); - } + //Assert( n_ic==Rewriter::rewrite( n_ic ) ); n_ic = Rewriter::rewrite( n_ic ); + collectTerms( n_ic ); Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; d_inst_map[n][index] = n_ic; return n_ic; @@ -1467,7 +1462,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, true ); + Node tt_cons = getInstantiateCons( tt, dt, index ); Node eq; if( tt!=tt_cons ){ eq = tt.eqNode( tt_cons ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 174117a8f..2777e775a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -260,7 +260,7 @@ private: /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index, bool isActive ); + Node getInstantiateCons( Node n, const Datatype& dt, int index ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ |