more updates and minor bug fixes for fmf/inst-gen quantifier instantiation

2 files changed, 21 insertions, 22 deletions

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 02e2412a4..efe3aebf4 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -12,13 +12,10 @@
  ** \brief Implementation of Theory UF Model
  **/
 
-#include "theory/quantifiers/model_engine.h"
 #include "theory/theory_engine.h"
+#include "theory/uf/theory_uf_model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 
 #define RECONSIDER_FUNC_DEFAULT_VALUE
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index ed8ccef4a..d037c374d 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1173,27 +1173,29 @@ void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
 }
 
 void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){
-  std::vector< Node > eqcs;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    if( eqc.getType()==d_type ){
-      if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
-        eqcs.push_back( eqc );
-        //we must ensure that this equivalence class has been accounted for
-        if( d_regions_map.find( eqc )==d_regions_map.end() ){
-          Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
-          Trace("uf-ss-warn") << "  type : " << d_type << std::endl;
-          Trace("uf-ss-warn") << "  kind : " << eqc.getKind() << std::endl;
+  if( Trace.isOn("uf-ss-warn") ){
+    std::vector< Node > eqcs;
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+    while( !eqcs_i.isFinished() ){
+      Node eqc = (*eqcs_i);
+      if( eqc.getType()==d_type ){
+        if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
+          eqcs.push_back( eqc );
+          //we must ensure that this equivalence class has been accounted for
+          if( d_regions_map.find( eqc )==d_regions_map.end() ){
+            Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
+            Trace("uf-ss-warn") << "  type : " << d_type << std::endl;
+            Trace("uf-ss-warn") << "  kind : " << eqc.getKind() << std::endl;
+          }
         }
       }
+      ++eqcs_i;
+    }
+    if( (int)eqcs.size()!=d_cardinality ){
+      Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
+      Trace("uf-ss-warn") << "  cardinality : " << d_cardinality << std::endl;
+      Trace("uf-ss-warn") << "  # reps : " << (int)eqcs.size() << std::endl;
     }
-    ++eqcs_i;
-  }
-  if( (int)eqcs.size()!=d_cardinality ){
-    Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
-    Trace("uf-ss-warn") << "  cardinality : " << d_cardinality << std::endl;
-    Trace("uf-ss-warn") << "  # reps : " << (int)eqcs.size() << std::endl;
   }
 }