diff options
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 2e8eb51b1..7dd8d02f6 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -37,10 +37,10 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{ } } -void RepSet::add( Node n ){ - TypeNode t = n.getType(); - d_tmap[ n ] = (int)d_type_reps[t].size(); - d_type_reps[t].push_back( n ); +void RepSet::add( TypeNode tn, Node n ){ + d_tmap[ n ] = (int)d_type_reps[tn].size(); + Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl; + d_type_reps[tn].push_back( n ); } int RepSet::getIndexFor( Node n ) const { @@ -59,7 +59,7 @@ void RepSet::complete( TypeNode t ){ while( !te.isFinished() ){ Node n = *te; if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){ - add( n ); + add( t, n ); } ++te; } @@ -143,7 +143,7 @@ bool RepSetIterator::initialize(){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; - d_rep_set->add( var ); + d_rep_set->add( tn, var ); } }else if( tn.isInteger() ){ bool inc = false; |