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.

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;