diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/theory/rep_set.cpp | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
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; |