Remove subsort symmetry breaking (#1807)

8 files changed, 142 insertions, 583 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 80bd082d6..886cd1af9 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -499,8 +499,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus_inference.h \
 	theory/quantifiers/sygus_sampler.cpp \
 	theory/quantifiers/sygus_sampler.h \
-	theory/quantifiers/symmetry_breaking.cpp \
-	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/term_database.cpp \
 	theory/quantifiers/term_database.h \
 	theory/quantifiers/term_enumeration.cpp \
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 06f58cca3..791b6e0bb 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -95,15 +95,6 @@ header = "options/uf_options.h"
   help       = "use cliques instead of splitting on demand to shrink model"
 
 [[option]]
-  name       = "ufssSymBreak"
-  category   = "regular"
-  long       = "uf-ss-sym-break"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "finite model finding symmetry breaking techniques"
-
-[[option]]
   name       = "ufssFairness"
   category   = "regular"
   long       = "uf-ss-fair"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97fbe82b8..55576870d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1846,9 +1846,6 @@ void SmtEngine::setDefaults() {
       options::mbqiMode.set( quantifiers::MBQI_FMC );
     }
   }
-  if( options::ufssSymBreak() ){
-    options::sortInference.set( true );
-  }
   if( options::fmfFunWellDefinedRelevant() ){
     if( !options::fmfFunWellDefined.wasSetByUser() ){
       options::fmfFunWellDefined.set( true );
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
deleted file mode 100644
index a8218480b..000000000
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ /dev/null
@@ -1,316 +0,0 @@
-/*********************                                                        */
-/*! \file symmetry_breaking.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief symmetry breaking module
- **
- **/
-
-#include "theory/quantifiers/symmetry_breaking.h"
-
-#include <vector>
-
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-#include "theory/sort_inference.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace std;
-
-namespace CVC4 {
-
-
-SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) :
-d_qe(qe), d_conflict(c,false) {
-  d_true =  NodeManager::currentNM()->mkConst( true );
-}
-
-eq::EqualityEngine * SubsortSymmetryBreaker::getEqualityEngine() {
-  return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
-}
-
-bool SubsortSymmetryBreaker::areEqual( Node n1, Node n2 ) {
-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
-}
-
-bool SubsortSymmetryBreaker::areDisequal( Node n1, Node n2 ) {
-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
-}
-
-
-Node SubsortSymmetryBreaker::getRepresentative( Node n ) {
-  return getEqualityEngine()->getRepresentative( n );
-}
-
-uf::StrongSolverTheoryUF * SubsortSymmetryBreaker::getStrongSolver() {
-  return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver();
-}
-
-SubsortSymmetryBreaker::TypeInfo::TypeInfo( context::Context * c ) :
-d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) {
-}
-
-SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) :
-d_dom_constants( c ), d_first_active( c, 0 ){
-  d_dc_nodes = 0;
-}
-
-unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() {
-  if( d_nodes.empty() ){
-    return 0;
-  }else{
-    return 1 + d_dom_constants.size();
-  }
-}
-
-Node SubsortSymmetryBreaker::SubSortInfo::getDomainConstant( int i ) {
-  if( i==0 ){
-    return d_nodes[0];
-  }else{
-    Assert( i<=(int)d_dom_constants.size() );
-    return d_dom_constants[i-1];
-  }
-}
-
-Node SubsortSymmetryBreaker::SubSortInfo::getFirstActive(eq::EqualityEngine * ee) {
-  if( d_first_active.get()<(int)d_nodes.size() ){
-    Node fa = d_nodes[d_first_active.get()];
-    return ee->hasTerm( fa ) ? fa : Node::null();
-  }else{
-    return Node::null();
-  }
-}
-
-SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn ) {
-  if( d_t_info.find( tn )==d_t_info.end() ){
-    d_t_info[tn] = new TypeInfo( d_qe->getSatContext() );
-  }
-  return d_t_info[tn];
-}
-
-SubsortSymmetryBreaker::SubSortInfo * SubsortSymmetryBreaker::getSubSortInfo( TypeNode tn, int sid ) {
-  if( d_type_info.find( sid )==d_type_info.end() ){
-    d_type_info[sid] = new SubSortInfo( d_qe->getSatContext() );
-    d_sub_sorts[tn].push_back( sid );
-    d_sid_to_type[sid] = tn;
-  }
-  return d_type_info[sid];
-}
-
-void SubsortSymmetryBreaker::newEqClass( Node n ) {
-  Trace("sym-break-temp") << "New eq class " << n << std::endl;
-  if( !d_conflict ){
-    TypeNode tn = n.getType();
-    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
-    if( si->isWellSorted( n ) ){
-      int sid = si->getSortId( n );
-      Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl;
-      SubSortInfo * ti = getSubSortInfo( tn, sid );
-      if( std::find( ti->d_nodes.begin(), ti->d_nodes.end(), n )==ti->d_nodes.end() ){
-        if( ti->d_nodes.empty() ){
-          //for first subsort, we add unit equality
-          if( d_sub_sorts[tn][0]!=sid ){
-            Trace("sym-break-temp") << "Do sym break unit with " << d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() << std::endl;
-            //add unit symmetry breaking lemma
-            Node eq = n.eqNode( d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() );
-            eq = Rewriter::rewrite( eq );
-            d_unit_lemmas.push_back( eq );
-            Trace("sym-break-lemma") << "*** SymBreak : Unit lemma (" << sid << "==" << d_sub_sorts[tn][0] << ") : " << eq << std::endl;
-            d_pending_lemmas.push_back( eq );
-          }
-          Trace("sym-break-dc") << "* Set first domain constant : " << n << " for " << tn << " : " << sid << std::endl;
-          ti->d_dc_nodes++;
-        }
-        ti->d_node_to_id[n] = ti->d_nodes.size();
-        ti->d_nodes.push_back( n );
-      }
-      TypeInfo * tti = getTypeInfo( tn );
-      if( !tti->d_has_dom_const_sort.get() ){
-        tti->d_has_dom_const_sort.set( true );
-        tti->d_max_dom_const_sort.set( sid );
-      }
-    }
-  }
-  Trace("sym-break-temp") << "Done new eq class" << std::endl;
-}
-
-
-
-void SubsortSymmetryBreaker::merge( Node a, Node b ) {
-  if( Trace.isOn("sym-break-debug") ){
-    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
-    int as = si->getSortId( a );
-    int bs = si->getSortId( b );
-    Trace("sym-break-debug") << "SSB: New merge " << a.getType() << " :: " << a << " : " << as;
-    Trace("sym-break-debug") << " == " << b << " : " << bs << std::endl;
-  }
-}
-
-void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) {
-  if( Trace.isOn("sym-break-debug") ){
-    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
-    int as = si->getSortId( a );
-    int bs = si->getSortId( b );
-    Trace("sym-break-debug") << "SSB: New assert disequal " << a.getType() << " :: " << a << " : " << as;
-    Trace("sym-break-debug") << " != " << b << " : " << bs << std::endl;
-  }
-}
-
-void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){
-  SubSortInfo * ti = getSubSortInfo( tn, sid );
-  if( (int)ti->getNumDomainConstants()<curr_card ){
-      //static int checkCount = 0;
-      //checkCount++;
-      //if( checkCount%1000==0 ){
-      //  std::cout << "Check count = " << checkCount << std::endl;
-      //}
-
-    Trace("sym-break-dc-debug") << "Check for domain constants " << tn << " : " << sid << ", curr_card = " << curr_card << ", ";
-    Trace("sym-break-dc-debug") << "#domain constants = " << ti->getNumDomainConstants() << std::endl;
-    Node fa = ti->getFirstActive(getEqualityEngine());
-    bool invalid = true;
-    while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){
-      invalid = false;
-      unsigned deq = 0;
-      for( unsigned i=0; i<ti->getNumDomainConstants(); i++ ){
-        Node dc = ti->getDomainConstant( i );
-        if( areEqual( fa, dc ) ){
-          invalid = true;
-          break;
-        }else if( areDisequal( fa, dc ) ){
-          deq++;
-        }
-      }
-      if( deq==ti->getNumDomainConstants() ){
-        Trace("sym-break-dc") << "* Can infer domain constant #" << ti->getNumDomainConstants()+1;
-        Trace("sym-break-dc") << " : " << fa << " for " << tn << " : " << sid << std::endl;
-        //add to domain constants
-        ti->d_dom_constants.push_back( fa );
-        if( ti->d_node_to_id[fa]>ti->d_dc_nodes ){
-          Trace("sym-break-dc-debug") << "Swap nodes... " << ti->d_dc_nodes << " " << ti->d_node_to_id[fa] << " " << ti->d_nodes.size() << std::endl;
-          //swap
-          Node on = ti->d_nodes[ti->d_dc_nodes];
-          int id = ti->d_node_to_id[fa];
-
-          ti->d_nodes[ti->d_dc_nodes] = fa;
-          ti->d_nodes[id] = on;
-          ti->d_node_to_id[fa] = ti->d_dc_nodes;
-          ti->d_node_to_id[on] = id;
-        }
-        ti->d_dc_nodes++;
-        Trace("sym-break-dc-debug") << "Get max type info..." << std::endl;
-        TypeInfo * tti = getTypeInfo( tn );
-        Assert( tti->d_has_dom_const_sort.get() );
-        int msid = tti->d_max_dom_const_sort.get();
-        SubSortInfo * max_ti = getSubSortInfo( d_sid_to_type[msid], msid );
-        Trace("sym-break-dc-debug") << "Swap nodes..." << std::endl;
-        //now, check if we can apply symmetry breaking to another sort
-        if( ti->getNumDomainConstants()>max_ti->getNumDomainConstants() ){
-          Trace("sym-break-dc") << "Max domain constant subsort for " << tn << " becomes " << sid << std::endl;
-          tti->d_max_dom_const_sort.set( sid );
-        }else if( ti!=max_ti ){
-          //construct symmetry breaking lemma
-          //current domain constant must be disequal from all current ones
-          Trace("sym-break-dc") << "Get domain constant " << ti->getNumDomainConstants()-1;
-          Trace("sym-break-dc") << " from max_ti, " << max_ti->getNumDomainConstants() << std::endl;
-          //apply a symmetry breaking lemma
-          Node m = max_ti->getDomainConstant(ti->getNumDomainConstants()-1);
-          //if fa and m are disequal from all previous domain constants in the other sort
-          std::vector< Node > cc;
-          for( unsigned r=0; r<2; r++ ){
-            Node n = ((r==0)==(msid>sid)) ? fa : m;
-            Node on = ((r==0)==(msid>sid)) ? m : fa;
-            SubSortInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti;
-            for( unsigned i=0; i<t->d_node_to_id[on]; i++ ){
-              cc.push_back( n.eqNode( t->d_nodes[i] ) );
-            }
-          }
-          //then, we can assume fa = m
-          cc.push_back( fa.eqNode( m ) );
-          Node lem = NodeManager::currentNM()->mkNode( kind::OR, cc );
-          lem = Rewriter::rewrite( lem );
-          if( std::find( d_lemmas.begin(), d_lemmas.end(), lem )==d_lemmas.end() ){
-            d_lemmas.push_back( lem );
-            Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << tti->d_max_dom_const_sort.get() << ") : ";
-            Trace("sym-break-lemma") << lem << std::endl;
-            d_pending_lemmas.push_back( lem );
-          }
-        }
-        invalid = true;
-      }
-      if( invalid ){
-        ti->d_first_active.set( ti->d_first_active + 1 );
-        fa = ti->getFirstActive(getEqualityEngine());
-      }
-    }
-  }
-}
-
-void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) {
-  Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl;
-  Trace(c) << "  Domain constants : ";
-  SubSortInfo * ti = getSubSortInfo( tn, sid );
-  for( NodeList::const_iterator it = ti->d_dom_constants.begin(); it != ti->d_dom_constants.end(); ++it ){
-    Node dc = *it;
-    Trace(c) << dc << " ";
-  }
-  Trace(c) << std::endl;
-  Trace(c) << "  First active node : " << ti->getFirstActive(getEqualityEngine()) << std::endl;
-}
-
-bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
-
-  Trace("sym-break-debug") << "SymBreak : check " << level << std::endl;
-  /*
-  while( d_fact_index.get()<d_fact_list.size() ){
-    Node f = d_fact_list[d_fact_index.get()];
-    d_fact_index.set( d_fact_index.get() + 1 );
-    if( f.getKind()==EQUAL ){
-      merge( f[0], f[1] );
-    }else if( f.getKind()==NOT && f[0].getKind()==EQUAL ){
-      assertDisequal( f[0][0], f[0][1] );
-    }else{
-      newEqClass( f );
-    }
-  }
-  */
-  Trace("sym-break-debug") << "SymBreak : update first actives" << std::endl;
-  for( std::map< TypeNode, std::vector< int > >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){
-    int card = getStrongSolver()->getCardinality( it->first );
-    for( unsigned i=0; i<it->second.size(); i++ ){
-      //check if the first active is disequal from all domain constants
-      processFirstActive( it->first, it->second[i], card );
-    }
-  }
-
-
-  Trace("sym-break-debug") << "SymBreak : finished check, now flush lemmas... (#lemmas = " << d_pending_lemmas.size() << ")" << std::endl;
-  //flush pending lemmas
-  if( !d_pending_lemmas.empty() ){
-    for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){
-      getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i], false, true );
-      ++( getStrongSolver()->d_statistics.d_sym_break_lemmas );
-    }
-    d_pending_lemmas.clear();
-    return true;
-  }else{
-    return false;
-  }
-}
-
-
-
-}
-
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
deleted file mode 100644
index 091490cec..000000000
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                                        */
-/*! \file symmetry_breaking.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Pre-process step for first-order reasoning
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H
-#define __CVC4__QUANT_SYMMETRY_BREAKING_H
-
-#include <iostream>
-#include <map>
-#include <string>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/sort_inference.h"
-#include "theory/theory.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace uf {
-  class StrongSolverTheoryUF;
-}
-
-class SubsortSymmetryBreaker {
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef context::CDList<Node> NodeList;
-private:
-  /** quantifiers engine */
-  QuantifiersEngine* d_qe;
-  eq::EqualityEngine * getEqualityEngine();
-  bool areDisequal( Node n1, Node n2 );
-  bool areEqual( Node n1, Node n2 );
-  Node getRepresentative( Node n );
-  uf::StrongSolverTheoryUF * getStrongSolver();
-  std::vector< Node > d_unit_lemmas;
-  Node d_true;
-  context::CDO< bool > d_conflict;
-public:
-  SubsortSymmetryBreaker( QuantifiersEngine* qe, context::Context* c );
-  ~SubsortSymmetryBreaker(){}
-
-private:
-  class TypeInfo {
-  public:
-    TypeInfo( context::Context* c );
-    context::CDO< int > d_max_dom_const_sort;
-    context::CDO< bool > d_has_dom_const_sort;
-  };
-  class SubSortInfo {
-  public:
-    SubSortInfo( context::Context* c );
-    //list of all nodes from this (sub)type
-    std::vector< Node > d_nodes;
-    //the current domain constants for this (sub)type
-    NodeList d_dom_constants;
-    //# nodes in d_nodes that have been domain constants, size of this distinct # of domain constants seen
-    unsigned d_dc_nodes;
-    //the node we are currently watching to become a domain constant
-    context::CDO< int > d_first_active;
-    //node to id
-    std::map< Node, unsigned > d_node_to_id;
-    Node getBaseConstant() { return d_nodes.empty() ? Node::null() : d_nodes[0]; }
-    bool hasDomainConstant( Node n );
-    unsigned getNumDomainConstants();
-    Node getDomainConstant( int i );
-    Node getFirstActive(eq::EqualityEngine * ee);
-  };
-  std::map< TypeNode, std::vector< int > > d_sub_sorts;
-  std::map< int, TypeNode > d_sid_to_type;
-  std::map< TypeNode, TypeInfo * > d_t_info;
-  std::map< int, SubSortInfo * > d_type_info;
-
-  TypeInfo * getTypeInfo( TypeNode tn );
-  SubSortInfo * getSubSortInfo( TypeNode tn, int sid );
-
-  void processFirstActive( TypeNode tn, int sid, int curr_card );
-private:
-  //void printDebugNodeInfo( const char * c, Node n );
-  void printDebugSubSortInfo( const char * c, TypeNode tn, int sid );
-  /** fact list */
-  std::vector< Node > d_pending_lemmas;
-  std::vector< Node > d_lemmas;
-public:
-  /** new node */
-  void newEqClass( Node n );
-  /** merge */
-  void merge( Node a, Node b );
-  /** assert disequal */
-  void assertDisequal( Node a, Node b );
-  /** check */
-  bool check( Theory::Effort level );
-};
-
-}
-}
-
-#endif
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index b469ac9d0..7a059771f 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -117,6 +117,7 @@ void SortInference::reset() {
 void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){
   if( doSortInference ){
     Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
     //process all assertions
     std::map< Node, int > visited;
     for( unsigned i=0; i<assertions.size(); i++ ){
@@ -152,118 +153,161 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doSortInfere
       Trace("sort-inference") << std::endl;
     }
 
-    if( !options::ufssSymBreak() ){
-      bool rewritten = false;
-      //determine monotonicity of sorts
-      Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..." << std::endl;
-      std::map< Node, std::map< int, bool > > visited;
-      for( unsigned i=0; i<assertions.size(); i++ ){
-        Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
-        std::map< Node, Node > var_bound;
-        processMonotonic( assertions[i], true, true, var_bound, visited );
-      }
-      Trace("sort-inference-proc") << "...done" << std::endl;
-
-      Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
-      for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
-        printSort( "sort-inference", d_sub_sorts[i] );
-        if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
-          Trace("sort-inference") << " is interpreted." << std::endl;
-        }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
-          Trace("sort-inference") << " is monotonic." << std::endl;
-        }else{
-          Trace("sort-inference") << " is not monotonic." << std::endl;
-        }
+    bool rewritten = false;
+    // determine monotonicity of sorts
+    Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..."
+                                 << std::endl;
+    std::map<Node, std::map<int, bool> > visitedm;
+    for (const Node& a : assertions)
+    {
+      Trace("sort-inference-debug") << "Process monotonicity for " << a
+                                    << std::endl;
+      std::map<Node, Node> var_bound;
+      processMonotonic(a, true, true, var_bound, visitedm);
+    }
+    Trace("sort-inference-proc") << "...done" << std::endl;
+
+    Trace("sort-inference") << "We have " << d_sub_sorts.size()
+                            << " sub-sorts : " << std::endl;
+    for (unsigned i = 0, size = d_sub_sorts.size(); i < size; i++)
+    {
+      printSort("sort-inference", d_sub_sorts[i]);
+      if (d_type_types.find(d_sub_sorts[i]) != d_type_types.end())
+      {
+        Trace("sort-inference") << " is interpreted." << std::endl;
+      }
+      else if (d_non_monotonic_sorts.find(d_sub_sorts[i])
+               == d_non_monotonic_sorts.end())
+      {
+        Trace("sort-inference") << " is monotonic." << std::endl;
+      }
+      else
+      {
+        Trace("sort-inference") << " is not monotonic." << std::endl;
       }
+    }
 
-      //simplify all assertions by introducing new symbols wherever necessary
-      Trace("sort-inference-proc") << "Perform simplification..." << std::endl;
-      std::map< Node, std::map< TypeNode, Node > > visited2;
-      for( unsigned i=0; i<assertions.size(); i++ ){
-        Node prev = assertions[i];
-        std::map< Node, Node > var_bound;
-        Trace("sort-inference-debug") << "Simplify " << assertions[i] << std::endl;
-        TypeNode tnn;
-        Node curr = simplifyNode( assertions[i], var_bound, tnn, visited2 );
-        Trace("sort-inference-debug") << "Done." << std::endl;
-        if( curr!=assertions[i] ){
-          Trace("sort-inference-debug") << "Rewrite " << curr << std::endl;
-          curr = theory::Rewriter::rewrite( curr );
-          rewritten = true;
-          Trace("sort-inference-rewrite") << assertions << std::endl;
-          Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
-          PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
-          assertions[i] = curr;
-        }
+    // simplify all assertions by introducing new symbols wherever necessary
+    Trace("sort-inference-proc") << "Perform simplification..." << std::endl;
+    std::map<Node, std::map<TypeNode, Node> > visited2;
+    for (unsigned i = 0, size = assertions.size(); i < size; i++)
+    {
+      Node prev = assertions[i];
+      std::map<Node, Node> var_bound;
+      Trace("sort-inference-debug") << "Simplify " << prev << std::endl;
+      TypeNode tnn;
+      Node curr = simplifyNode(assertions[i], var_bound, tnn, visited2);
+      Trace("sort-inference-debug") << "Done." << std::endl;
+      if (curr != assertions[i])
+      {
+        Trace("sort-inference-debug") << "Rewrite " << curr << std::endl;
+        curr = theory::Rewriter::rewrite(curr);
+        rewritten = true;
+        Trace("sort-inference-rewrite") << assertions << std::endl;
+        Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
+        PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]););
+        assertions[i] = curr;
       }
-      Trace("sort-inference-proc") << "...done" << std::endl;
-      //now, ensure constants are distinct
-      for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
-        std::vector< Node > consts;
-        for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-          Assert( it2->first.isConst() );
-          consts.push_back( it2->second );
-        }
-        //add lemma enforcing introduced constants to be distinct
-        if( consts.size()>1 ){
-          Node distinct_const = NodeManager::currentNM()->mkNode( kind::DISTINCT, consts );
-          Trace("sort-inference-rewrite") << "Add the constant distinctness lemma: " << std::endl;
-          Trace("sort-inference-rewrite") << "  " << distinct_const << std::endl;
-          assertions.push_back( distinct_const );
-          rewritten = true;
-        }
+    }
+    Trace("sort-inference-proc") << "...done" << std::endl;
+    // now, ensure constants are distinct
+    for (std::map<TypeNode, std::map<Node, Node> >::iterator it =
+             d_const_map.begin();
+         it != d_const_map.end();
+         ++it)
+    {
+      std::vector<Node> consts;
+      for (std::map<Node, Node>::iterator it2 = it->second.begin();
+           it2 != it->second.end();
+           ++it2)
+      {
+        Assert(it2->first.isConst());
+        consts.push_back(it2->second);
+      }
+      // add lemma enforcing introduced constants to be distinct
+      if (consts.size() > 1)
+      {
+        Node distinct_const = nm->mkNode(kind::DISTINCT, consts);
+        Trace("sort-inference-rewrite")
+            << "Add the constant distinctness lemma: " << std::endl;
+        Trace("sort-inference-rewrite") << "  " << distinct_const << std::endl;
+        assertions.push_back(distinct_const);
+        rewritten = true;
       }
+    }
 
-      //enforce constraints based on monotonicity
-      Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl;
-      for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
-        int nmonSort = -1;
-        for( unsigned i=0; i<it->second.size(); i++ ){
-          if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
-            nmonSort = it->second[i];
-            break;
-          }
+    // enforce constraints based on monotonicity
+    Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl;
+    for (std::map<TypeNode, std::vector<int> >::iterator it =
+             d_type_sub_sorts.begin();
+         it != d_type_sub_sorts.end();
+         ++it)
+    {
+      int nmonSort = -1;
+      unsigned nsorts = it->second.size();
+      for (unsigned i = 0; i < nsorts; i++)
+      {
+        if (d_non_monotonic_sorts.find(it->second[i])
+            != d_non_monotonic_sorts.end())
+        {
+          nmonSort = it->second[i];
+          break;
         }
-        if( nmonSort!=-1 ){
-          std::vector< Node > injections;
-          TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
-          for( unsigned i=0; i<it->second.size(); i++ ){
-            if( it->second[i]!=nmonSort ){
-              TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
-              //make injection to nmonSort
-              Node a1 = mkInjection( new_tn, base_tn );
-              injections.push_back( a1 );
-              if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
-                //also must make injection from nmonSort to this
-                Node a2 = mkInjection( base_tn, new_tn );
-                injections.push_back( a2 );
-              }
+      }
+      if (nmonSort != -1)
+      {
+        std::vector<Node> injections;
+        TypeNode base_tn = getOrCreateTypeForId(nmonSort, it->first);
+        for (unsigned i = 0; i < nsorts; i++)
+        {
+          if (it->second[i] != nmonSort)
+          {
+            TypeNode new_tn = getOrCreateTypeForId(it->second[i], it->first);
+            // make injection to nmonSort
+            Node a1 = mkInjection(new_tn, base_tn);
+            injections.push_back(a1);
+            if (d_non_monotonic_sorts.find(it->second[i])
+                != d_non_monotonic_sorts.end())
+            {
+              // also must make injection from nmonSort to this
+              Node a2 = mkInjection(base_tn, new_tn);
+              injections.push_back(a2);
             }
           }
+        }
+        if (Trace.isOn("sort-inference-rewrite"))
+        {
           Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
-          for( unsigned j=0; j<injections.size(); j++ ){
-            Trace("sort-inference-rewrite") << "   " << injections[j] << std::endl;
-          }
-          assertions.insert( assertions.end(), injections.begin(), injections.end() );
-          if( !injections.empty() ){
-            rewritten = true;
+          for (const Node& i : injections)
+          {
+            Trace("sort-inference-rewrite") << "   " << i << std::endl;
           }
         }
+        assertions.insert(
+            assertions.end(), injections.begin(), injections.end());
+        if (!injections.empty())
+        {
+          rewritten = true;
+        }
       }
-      Trace("sort-inference-proc") << "...done" << std::endl;
-      //no sub-sort information is stored
-      reset();
-      Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten << std::endl;
     }
+    Trace("sort-inference-proc") << "...done" << std::endl;
+    // no sub-sort information is stored
+    reset();
+    Trace("sort-inference-debug")
+        << "Finished sort inference, rewritten = " << rewritten << std::endl;
+
     initialSortCount = sortCount;
   }
   if( doMonotonicyInference ){
-    std::map< Node, std::map< int, bool > > visited;
+    std::map<Node, std::map<int, bool> > visitedmt;
     Trace("sort-inference-proc") << "Calculating monotonicty for types..." << std::endl;
-    for( unsigned i=0; i<assertions.size(); i++ ){
-      Trace("sort-inference-debug") << "Process type monotonicity for " << assertions[i] << std::endl;
+    for (const Node& a : assertions)
+    {
+      Trace("sort-inference-debug") << "Process type monotonicity for " << a
+                                    << std::endl;
       std::map< Node, Node > var_bound;
-      processMonotonic( assertions[i], true, true, var_bound, visited, true );
+      processMonotonic(a, true, true, var_bound, visitedmt, true);
     }
     Trace("sort-inference-proc") << "...done" << std::endl;
   }
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 */