Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity. Minor cleanup.

2 files changed, 18 insertions, 10 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0fe50aad6..2ae5edb39 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -632,8 +632,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
     return r;
   }else{
     int sortId = 0;
-    if( optInternalRepSortInference() ){
-    //if( options::ufssSymBreak() ){
+    if( optInternalRepSortInference() && !f.isNull() ){
       sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
     }
     if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
@@ -646,12 +645,20 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       }else{
         std::vector< Node > eqc;
         getEquivalenceClass( r, eqc );
+        Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
+        for( unsigned i=0; i<eqc.size(); i++ ){
+          if( i>0 ) Trace("internal-rep-select") << ", ";
+          Trace("internal-rep-select") << eqc[i];
+        }
+        Trace("internal-rep-select")  << " } " << std::endl;
         int r_best_score = -1;
         for( size_t i=0; i<eqc.size(); i++ ){
-          int score = getRepScore( eqc[i], f, index );
+          //if cbqi is active, do not choose instantiation constant terms
           if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
-            if( optInternalRepSortInference() ){
-              int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
+            int score = getRepScore( eqc[i], f, index );
+            //base it on sort information as well
+            if( sortId!=0 ){
+              int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] );
               if( score>=0 && e_sortId!=sortId ){
                 score += 100;
               }
@@ -661,12 +668,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
               r_best = eqc[i];
               r_best_score = score;
             }
-		  }
+		      }
         }
         if( r_best.isNull() ){
-	      Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-		  r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-		}
+	        Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+		      r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+		    }
         //now, make sure that no other member of the class is an instance
         if( !optInternalRepSortInference() ){
           r_best = getInstance( r_best, eqc );
@@ -675,6 +682,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         if( d_rep_score.find( r_best )==d_rep_score.end() ){
           d_rep_score[ r_best ] = d_reset_count;
         }
+        Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
       }
       d_int_rep[sortId][r] = r_best;
       if( r_best!=a ){
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 163dd3c1f..8c85e4dd2 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1152,7 +1152,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
     clique.pop_back();
   }
   //debugging information
-  if( options::ufssSymBreak() ){
+  if( Trace.isOn("uf-ss-cliques") ){
     std::vector< Node > clique_vec;
     clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
     addClique( d_cardinality, clique_vec );