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, 12 insertions, 10 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8fecc6ee0..a16f46ace 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,18 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
   }
 }
 
-void QuantifiersEngine::printInstantiations( const char * c ) {
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
-      it->second->print( c, it->first );
-    }
-  }else{
+void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+  //Trace("ajr-temp") << "QE print inst." << std::endl;
+  //if( options::incrementalSolving() ){
+  //  for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+  //    out << "Instantiations of " << it->first << " : " << std::endl;
+  //    it->second->print( out, it->first );
+  //  }
+  //}else{
     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
-      it->second.print( c, it->first );
+      out << "Instantiations of " << it->first << " : " << std::endl;
+      it->second.print( out, it->first );
+      out << std::endl;
     }
-  }
+  //}
 }
 
 QuantifiersEngine::Statistics::Statistics():