2 files changed, 27 insertions, 3 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 7e0af3e9f..cab5dac42 100755
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -58,6 +58,14 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
       printSort( "sort-inference", it->second );
       Trace("sort-inference") << std::endl;
     }
+    for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
+      Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;
+      for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        printSort( "sort-inference", it2->second );
+        Trace("sort-inference") << std::endl;
+      }
+      Trace("sort-inference") << std::endl;
+    }
   }
   if( doRewrite ){
     //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
@@ -149,11 +157,11 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
       //TODO: try applying sort inference to quantified variables
-      //d_var_types[n][ n[0][i] ] = sortCount;
-      //sortCount++;
+      d_var_types[n][ n[0][i] ] = sortCount;
+      sortCount++;
 
       //type of the quantified variable must be the same
-      d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
+      //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
       var_bound[ n[0][i] ] = n;
     }
   }
@@ -404,5 +412,17 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   }
 
 }
+int SortInference::getSortId( Node n ) {
+  Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
+  return getRepresentative( d_op_return_types[op] );
+}
+
+int SortInference::getSortId( Node f, Node v ) {
+  return getRepresentative( d_var_types[f][v] );
+}
 
+void SortInference::setSkolemVar( Node f, Node v, Node sk ){
+  d_op_return_types[sk] = getSortId( f, v );
 }
+
+}
+\ No newline at end of file
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 363dbd84d..1378a266c 100755
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -65,6 +65,10 @@ public:
   ~SortInference(){}
 
   void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  int getSortId( Node n );
+  int getSortId( Node f, Node v );
+  //set that sk is the skolem variable of v for quantifier f
+  void setSkolemVar( Node f, Node v, Node sk );
 };
 
 }