Remove subsort symmetry breaking (#1807)

2 files changed, 4 insertions, 44 deletions

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 76cb95867..0e3f9c7a2 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_model.h"
-#include "theory/quantifiers/symmetry_breaking.h"
 
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS
@@ -144,9 +143,6 @@ void Region::setEqual( Node a, Node b ){
         if( !isDisequal( a, n, t ) ){
           setDisequal( a, n, t, true );
           nr->setDisequal( n, a, t, true );
-          if( options::ufssSymBreak() ){
-            d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
-          }
         }
         setDisequal( b, n, t, false );
         nr->setDisequal( n, b, t, false );
@@ -608,12 +604,6 @@ void SortModel::merge( Node a, Node b ){
         d_regions_map[b] = -1;
       }
       d_reps = d_reps - 1;
-
-      if( !d_conflict ){
-        if( options::ufssSymBreak() ){
-          d_thss->getSymmetryBreaker()->merge(a, b);
-        }
-      }
     }
   }
 }
@@ -659,12 +649,6 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
           checkRegion( ai );
           checkRegion( bi );
         }
-
-        if( !d_conflict ){
-          if( options::ufssSymBreak() ){
-            d_thss->getSymmetryBreaker()->assertDisequal(a, b);
-          }
-        }
       }
     }
   }
@@ -1508,7 +1492,8 @@ Node SortModel::getCardinalityLiteral( int c ) {
 
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
                                            context::UserContext* u,
-                                           OutputChannel& out, TheoryUF* th)
+                                           OutputChannel& out,
+                                           TheoryUF* th)
     : d_out(&out),
       d_th(th),
       d_conflict(c, false),
@@ -1518,11 +1503,8 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
       d_min_pos_com_card(c, -1),
       d_card_assertions_eqv_lemma(u),
       d_min_pos_tn_master_card(c, -1),
-      d_rel_eqc(c),
-      d_sym_break(NULL) {
-  if (options::ufssSymBreak()) {
-    d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
-  }
+      d_rel_eqc(c)
+{
 }
 
 StrongSolverTheoryUF::~StrongSolverTheoryUF() {
@@ -1530,9 +1512,6 @@ StrongSolverTheoryUF::~StrongSolverTheoryUF() {
        it != d_rep_model.end(); ++it) {
     delete it->second;
   }
-  if (d_sym_break) {
-    delete d_sym_break;
-  }
 }
 
 SortInference* StrongSolverTheoryUF::getSortInference() {
@@ -1555,9 +1534,6 @@ void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) {
     d_rel_eqc[a] = true;
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
     c->newEqClass( a );
-    if( options::ufssSymBreak() ){
-      d_sym_break->newEqClass( a );
-    }
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
   }
 }
@@ -1589,9 +1565,6 @@ void StrongSolverTheoryUF::newEqClass( Node a ){
 #else
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
     c->newEqClass( a );
-    if( options::ufssSymBreak() ){
-      d_sym_break->newEqClass( a );
-    }
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
 #endif
   }
@@ -1790,10 +1763,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
           break;
         }
       }
-      //check symmetry breaker
-      if( !d_conflict && options::ufssSymBreak() ){
-        d_sym_break->check( level );
-      }
     }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
       if( level==Theory::EFFORT_FULL ){
         // split on an equality between two equivalence classes (at most one per type)
@@ -2125,7 +2094,6 @@ StrongSolverTheoryUF::Statistics::Statistics():
   d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
   d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0),
   d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0),
-  d_sym_break_lemmas("StrongSolverTheoryUF::Symmetry_Breaking_Lemmas", 0),
   d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
   d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
 {
@@ -2133,7 +2101,6 @@ StrongSolverTheoryUF::Statistics::Statistics():
   smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
   smtStatisticsRegistry()->registerStat(&d_split_lemmas);
   smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas);
   smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
   smtStatisticsRegistry()->registerStat(&d_max_model_size);
 }
@@ -2143,7 +2110,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index f634a493c..ecbfd9a87 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -26,7 +26,6 @@
 namespace CVC4 {
 class SortInference;
 namespace theory {
-class SubsortSymmetryBreaker;
 namespace uf {
 class TheoryUF;
 } /* namespace CVC4::theory::uf */
@@ -370,8 +369,6 @@ public:
   ~StrongSolverTheoryUF();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** symmetry breaker */
-  SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; }
   /** get sort inference module */
   SortInference* getSortInference();
   /** get default sat context */
@@ -421,7 +418,6 @@ public:
     IntStat d_clique_lemmas;
     IntStat d_split_lemmas;
     IntStat d_disamb_term_lemmas;
-    IntStat d_sym_break_lemmas;
     IntStat d_totality_lemmas;
     IntStat d_max_model_size;
     Statistics();
@@ -468,8 +464,6 @@ public:
   context::CDO<int> d_min_pos_tn_master_card;
   /** relevant eqc */
   NodeBoolMap d_rel_eqc;
-  /** symmetry breaking techniques */
-  SubsortSymmetryBreaker* d_sym_break;
 }; /* class StrongSolverTheoryUF */