merged golden

11 files changed, 397 insertions, 122 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7f0f79ebc..199581b98 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1348,7 +1348,7 @@ void EqualityEngine::propagate() {
     }
 
     // If not merging internal nodes, notify the master
-    if (d_masterEqualityEngine && !d_isInternal[mergeInto]) {
+    if (d_masterEqualityEngine && !d_isInternal[t1classId] && !d_isInternal[t2classId]) {
       d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
       d_masterEqualityEngine->propagate();
     }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 206fb61c7..8d1b6f1d9 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -211,11 +211,6 @@ public:
     }
   };/* struct EqualityEngine::statistics */
 
-  /**
-   * Store the application lookup, with enough information to backtrack
-   */
-  void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
-
 private:
 
   /** The context we are using */
@@ -254,6 +249,11 @@ private:
   /** Number of application lookups, for backtracking.  */
   context::CDO<DefaultSizeType> d_applicationLookupsCount;
 
+  /**
+   * Store the application lookup, with enough information to backtrack
+   */
+  void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
+
   /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */
   std::vector<Node> d_nodes;
 
@@ -741,7 +741,7 @@ public:
   /**
    * Adds a predicate p with given polarity. The predicate asserted
    * should be in the congruence closure kinds (otherwise it's
-   * useless.
+   * useless).
    *
    * @param p the (non-negated) predicate
    * @param polarity true if asserting the predicate, false if
@@ -777,7 +777,7 @@ public:
   void getUseListTerms(TNode t, std::set<TNode>& output);
 
   /**
-   * Get an explanation of the equality t1 = t2 begin true of false.
+   * Get an explanation of the equality t1 = t2 being true or false.
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 33d1255ef..b9f60b83d 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -8,6 +8,9 @@ module UF "theory/uf/options.h" Uninterpreted functions theory
 option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true
  use UF symmetry breaker (Deharbe et al., CADE 2011)
 
+option condenseFunctionValues condense-function-values --condense-function-values bool :default true
+ condense models for functions rather than explicitly representing them
+
 option ufssRegions /--disable-uf-ss-regions bool :default true
  disable region-based method for discovering cliques and splits in uf strong solver
 option ufssEagerSplits --uf-ss-eager-split bool :default false
@@ -20,6 +23,8 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
  apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
 option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
  apply totality axioms lazily
+option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
+ apply symmetry breaking for totality axioms
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
  tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
 option ufssSmartSplits --uf-ss-smart-split bool :default false
@@ -30,5 +35,12 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
  always use simple clique lemmas for uf strong solver
 option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
  eagerly propagate disequalities for uf strong solver
+option ufssMinimalModel /--disable-uf-ss-min-model bool :default true
+ disable finding a minimal model in uf strong solver
+option ufssCliqueSplits --uf-ss-clique-splits bool :default false
+ use cliques instead of splitting on demand to shrink model
+
+option ufssSymBreak --uf-ss-sym-break bool :default false
+ finite model finding symmetry breaking techniques
 
 endmodule
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index fcb6c3cd5..f5d7f9235 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -52,6 +52,8 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+using namespace ::CVC4::context;
+
 SymmetryBreaker::Template::Template() :
   d_template(),
   d_sets(),
@@ -165,7 +167,10 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker() :
+SymmetryBreaker::SymmetryBreaker(context::Context* context) :
+  ContextNotifyObj(context),
+  d_assertionsToRerun(context),
+  d_rerunningAssertions(false),
   d_phi(),
   d_phiSet(),
   d_permutations(),
@@ -175,6 +180,31 @@ SymmetryBreaker::SymmetryBreaker() :
   d_termEqs() {
 }
 
+class SBGuard {
+  bool& d_ref;
+  bool d_old;
+public:
+  SBGuard(bool& b) : d_ref(b), d_old(b) {}
+  ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; }
+};/* class SBGuard */
+
+void SymmetryBreaker::rerunAssertionsIfNecessary() {
+  if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) {
+    return;
+  }
+
+  SBGuard g(d_rerunningAssertions);
+  d_rerunningAssertions = true;
+
+  Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl;
+  for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin();
+      i != d_assertionsToRerun.end();
+      ++i) {
+    assertFormula(*i);
+  }
+  Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl;
+}
+
 Node SymmetryBreaker::norm(TNode phi) {
   Node n = Rewriter::rewrite(phi);
   return normInternal(n);
@@ -254,6 +284,10 @@ Node SymmetryBreaker::normInternal(TNode n) {
 }
 
 void SymmetryBreaker::assertFormula(TNode phi) {
+  rerunAssertionsIfNecessary();
+  if(!d_rerunningAssertions) {
+    d_assertionsToRerun.push_back(phi);
+  }
   // use d_phi, put into d_permutations
   Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
   d_phi.push_back(phi);
@@ -322,6 +356,7 @@ void SymmetryBreaker::clear() {
 }
 
 void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
+  rerunAssertionsIfNecessary();
   guessPermutations();
   Debug("ufsymm") << "UFSYMM =====================================================" << endl
                   << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index cf54b62c2..d04da048a 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -50,13 +50,15 @@
 
 #include "expr/node.h"
 #include "expr/node_builder.h"
+#include "context/context.h"
+#include "context/cdlist.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class SymmetryBreaker {
+class SymmetryBreaker : public context::ContextNotifyObj {
 
   class Template {
     Node d_template;
@@ -92,6 +94,19 @@ public:
 
 private:
 
+  /**
+   * This class wasn't initially built to be incremental.  It should
+   * be attached to a UserContext so that it clears everything when
+   * a pop occurs.  This "assertionsToRerun" is a set of assertions to
+   * feed back through assertFormula() when we started getting things
+   * again.  It's not just a matter of effectiveness, but also soundness;
+   * if some assertions (still in scope) are not seen by a symmetry-breaking
+   * round, then some symmetries that don't actually exist might be broken,
+   * leading to unsound results!
+   */
+  context::CDList<Node> d_assertionsToRerun;
+  bool d_rerunningAssertions;
+
   std::vector<Node> d_phi;
   std::set<TNode> d_phiSet;
   Permutations d_permutations;
@@ -101,6 +116,7 @@ private:
   TermEqs d_termEqs;
 
   void clear();
+  void rerunAssertionsIfNecessary();
 
   void guessPermutations();
   bool invariantByPermutations(const Permutation& p);
@@ -140,9 +156,17 @@ private:
                  d_initNormalizationTimer,
                  "theory::uf::symmetry_breaker::timers::initNormalization");
 
+protected:
+
+  void contextNotifyPop() {
+    Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
+    clear();
+  }
+
 public:
 
-  SymmetryBreaker();
+  SymmetryBreaker(context::Context* context);
+  ~SymmetryBreaker() throw() {}
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 69a963360..41935984f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -38,7 +38,8 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   d_conflict(c, false),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
-  d_functionsTerms(c)
+  d_functionsTerms(c),
+  d_symb(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 228cfd2c4..c0d114052 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -17,6 +17,10 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/options.h"
+
+#include <vector>
+#include <stack>
 
 #define RECONSIDER_FUNC_DEFAULT_VALUE
 #define USE_PARTIAL_DEFAULT_VALUES
@@ -133,28 +137,60 @@ Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& inde
   }
 }
 
-Node UfModelTreeNode::getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue ){
-  if( !d_data.empty() ){
+Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
+  if(!d_data.empty()) {
     Node defaultValue = argDefaultValue;
-    if( d_data.find( Node::null() )!=d_data.end() ){
-      defaultValue = d_data[Node::null()].getFunctionValue( args, index+1, argDefaultValue );
+    if(d_data.find(Node::null()) != d_data.end()) {
+      defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
     }
-    std::vector< Node > caseArgs;
-    std::map< Node, Node > caseValues;
-    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      if( !it->first.isNull() ){
-        Node val = it->second.getFunctionValue( args, index+1, defaultValue );
-        caseArgs.push_back( it->first );
-        caseValues[ it->first ] = val;
+
+    vector<Node> caseArgs;
+    map<Node, Node> caseValues;
+
+    for(map< Node, UfModelTreeNode>::iterator it = d_data.begin(); it != d_data.end(); ++it) {
+      if(!it->first.isNull()) {
+        Node val = it->second.getFunctionValue(args, index + 1, defaultValue, simplify);
+        caseArgs.push_back(it->first);
+        caseValues[it->first] = val;
       }
     }
+
+    NodeManager* nm = NodeManager::currentNM();
     Node retNode = defaultValue;
-    for( int i=((int)caseArgs.size()-1); i>=0; i-- ){
-      retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArgs[ i ] ), caseValues[ caseArgs[ i ] ], retNode );
+
+    if(!simplify) {
+      // "non-simplifying" mode - expand function values to things like:
+      //   IF      (x=0 AND y=0 AND z=0) THEN value1
+      //   ELSE IF (x=0 AND y=0 AND z=1) THEN value2
+      //   [...etc...]
+      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
+        Node val = caseValues[ caseArgs[ i ] ];
+        if(val.getKind() == ITE) {
+          // use a stack to reverse the order, since we're traversing outside-in
+          stack<TNode> stk;
+          do {
+            stk.push(val);
+            val = val[2];
+          } while(val.getKind() == ITE);
+          AlwaysAssert(val == defaultValue, "default values don't match when constructing function definition!");
+          while(!stk.empty()) {
+            val = stk.top();
+            stk.pop();
+            retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
+          }
+        } else {
+          retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
+        }
+      }
+    } else {
+      // "simplifying" mode - condense function values
+      for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
+        retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
+      }
     }
     return retNode;
-  }else{
-    Assert( !d_value.isNull() );
+  } else {
+    Assert(!d_value.isNull());
     return d_value;
   }
 }
@@ -259,14 +295,16 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
   }
 }
 
-Node UfModelTree::getFunctionValue( std::vector< Node >& args ){
-  Node body = d_tree.getFunctionValue( args, 0, Node::null() );
-  body = Rewriter::rewrite( body );
+Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
+  Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
+  if(simplify) {
+    body = Rewriter::rewrite( body );
+  }
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
 }
 
-Node UfModelTree::getFunctionValue( const char* argPrefix ){
+Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
   TypeNode type = d_op.getType();
   std::vector< Node > vars;
   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
@@ -274,7 +312,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix ){
     ss << argPrefix << (i+1);
     vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
   }
-  return getFunctionValue( vars );
+  return getFunctionValue( vars, simplify );
 }
 
 Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
@@ -309,19 +347,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground
     if( !ground ){
       int defSize = (int)d_defaults.size();
       for( int i=0; i<defSize; i++ ){
-        bool isGround;
         //for soundness, to allow variable order-independent function interpretations,
         //  we must ensure that the intersection of all default terms
         //  is also defined.
         //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
         //  then we must define f( b, a ).
-        Node ni = getIntersection( m, n, d_defaults[i], isGround );
-        if( !ni.isNull() ){
-          //if the intersection exists, and is not already defined
-          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
-              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
-            //use the current value
-            setValue( m, ni, v, isGround, false );
+        if (!options::fmfFullModelCheck()) {
+          bool isGround;
+          Node ni = getIntersection( m, n, d_defaults[i], isGround );
+          if( !ni.isNull() ){
+            //if the intersection exists, and is not already defined
+            if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+                d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+              //use the current value
+              setValue( m, ni, v, isGround, false );
+            }
           }
         }
       }
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 12c1cf244..133cd2cf2 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -46,7 +46,7 @@ public:
   /** getConstant Value function */
   Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
   /** getFunctionValue */
-  Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue );
+  Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true );
   /** update function */
   void update( TheoryModel* m );
   /** simplify function */
@@ -125,9 +125,9 @@ public:
   /** getFunctionValue
     *   Returns a representation of this function.
     */
-  Node getFunctionValue( std::vector< Node >& args );
+  Node getFunctionValue( std::vector< Node >& args, bool simplify = true );
   /** getFunctionValue for args with set prefix */
-  Node getFunctionValue( const char* argPrefix );
+  Node getFunctionValue( const char* argPrefix, bool simplify = true );
   /** update
     *   This will update all values in the tree to be representatives in m.
     */
@@ -144,18 +144,12 @@ public:
   void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){
     d_tree.debugPrint( out, m, d_index_order, ind );
   }
-private:
-  //helper for to ITE function.
-  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );
-public:
-  /** to ITE function for function model nodes */
-  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }
-  static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
 };
 
+
 class UfModelTreeGenerator
 {
-private:
+public:
   //store for set values
   Node d_default_value;
   std::map< Node, Node > d_set_values[2][2];
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 94ab47d23..40713fa41 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -21,6 +21,7 @@
 #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
 
 #include "theory/rewriter.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d64f7df60..163dd3c1f 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -20,6 +20,8 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/options.h"
 #include "theory/model.h"
+#include "theory/quantifiers/symmetry_breaking.h"
+
 
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS
@@ -117,6 +119,9 @@ void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){
           if( options::ufssDiseqPropagation() ){
             d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
           }
+          if( options::ufssSymBreak() ){
+            d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
+          }
         }
         setDisequal( b, n, t, false );
         nr->setDisequal( n, b, t, false );
@@ -322,6 +327,20 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
   return false;
 }
 
+bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) {
+  if( d_testCliqueSize>=long(cardinality+1) ){
+    //test clique is a clique
+    for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+      if( (*it).second ){
+        clique.push_back( (*it).first );
+      }
+    }
+    return true;
+  }
+  return false;
+}
+
+
 void StrongSolverTheoryUF::SortModel::Region::getRepresentatives( std::vector< Node >& reps ){
   for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
     RegionNodeInfo* rni = it->second;
@@ -394,9 +413,9 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 
 
 
-StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
+StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
-          d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( 0 ),
+          d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
           d_cardinality_assertions( c ), d_hasCard( c, false ){
   d_cardinality_term = n;
 }
@@ -501,9 +520,14 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
       }
       d_reps = d_reps - 1;
 
-      if( options::ufssDiseqPropagation() && !d_conflict ){
-        //notify the disequality propagator
-        d_thss->getDisequalityPropagator()->merge(a, b);
+      if( !d_conflict ){
+        if( options::ufssDiseqPropagation() ){
+          //notify the disequality propagator
+          d_thss->getDisequalityPropagator()->merge(a, b);
+        }
+        if( options::ufssSymBreak() ){
+          d_thss->getSymmetryBreaker()->merge(a, b);
+        }
       }
     }
   }
@@ -551,9 +575,14 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso
           checkRegion( bi );
         }
 
-        if( options::ufssDiseqPropagation() && !d_conflict ){
-          //notify the disequality propagator
-          d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
+        if( !d_conflict ){
+          if( options::ufssDiseqPropagation() ){
+            //notify the disequality propagator
+            d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
+          }
+          if( options::ufssSymBreak() ){
+            d_thss->getSymmetryBreaker()->assertDisequal(a, b);
+          }
         }
       }
     }
@@ -595,9 +624,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           if( d_regions[i]->d_valid ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              //add clique lemma
-              addCliqueLemma( clique, out );
-              return;
+              if( options::ufssMinimalModel() ){
+                //add clique lemma
+                addCliqueLemma( clique, out );
+                return;
+              }
             }else{
               Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
             }
@@ -623,11 +654,21 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
             if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){
-              if( addSplit( d_regions[i], out ) ){
-                addedLemma = true;
+              //just add the clique lemma
+              if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
+                std::vector< Node > clique;
+                if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){
+                  //add clique lemma
+                  addCliqueLemma( clique, out );
+                  return;
+                }
+              }else{
+                if( addSplit( d_regions[i], out ) ){
+                  addedLemma = true;
 #ifdef ONE_SPLIT_REGION
-                break;
+                  break;
 #endif
+                }
               }
             }
           }
@@ -644,7 +685,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
               for( int i=0; i<(int)d_regions_index; i++ ){
                 if( d_regions[i]->d_valid ){
                   Node op = d_regions[i]->d_nodes.begin()->first;
-                  int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op);
+                  int sort_id = d_thss->getSortInference()->getSortId(op);
                   if( sortsFound.find( sort_id )!=sortsFound.end() ){
                     combineRegions( sortsFound[sort_id], i );
                     recheck = true;
@@ -659,13 +700,17 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
               //naive strategy, force region combination involving the first valid region
               for( int i=0; i<(int)d_regions_index; i++ ){
                 if( d_regions[i]->d_valid ){
-                  forceCombineRegion( i, false );
-                  recheck = true;
-                  break;
+                  int fcr = forceCombineRegion( i, false );
+                  Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
+                  if( options::ufssMinimalModel() || fcr!=-1 ){
+                    recheck = true;
+                    break;
+                  }
                 }
               }
             }
             if( recheck ){
+              Trace("uf-ss-debug") << "Must recheck." << std::endl;
               check( level, out );
             }
           }
@@ -869,8 +914,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
     //now check if region is in conflict
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      //explain clique
-      addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      if( options::ufssMinimalModel() ){
+        //explain clique
+        addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      }
     }
   }
 }
@@ -947,18 +994,33 @@ void StrongSolverTheoryUF::SortModel::moveNode( Node n, int ri ){
 void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
   if( d_aloc_cardinality>0 ){
     Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl;
-    if( Trace.isOn("uf-ss-cliques") ){
-      Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " : " << std::endl;
-      for( size_t i=0; i<d_cliques[ d_aloc_cardinality ].size(); i++ ){
-        Trace("uf-ss-cliques") << "  ";
-        for( size_t j=0; j<d_cliques[ d_aloc_cardinality ][i].size(); j++ ){
-          Trace("uf-ss-cliques") << d_cliques[ d_aloc_cardinality ][i][j] << " ";
-        }
-        Trace("uf-ss-cliques") << std::endl;
+  }
+  if( Trace.isOn("uf-ss-cliques") ){
+    Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " for " << d_type << " : " << std::endl;
+    for( size_t i=0; i<d_cliques[ d_aloc_cardinality ].size(); i++ ){
+      Trace("uf-ss-cliques") << "  ";
+      for( size_t j=0; j<d_cliques[ d_aloc_cardinality ][i].size(); j++ ){
+        Trace("uf-ss-cliques") << d_cliques[ d_aloc_cardinality ][i][j] << " ";
       }
+      Trace("uf-ss-cliques") << std::endl;
+    }
+  }
+  /*
+  if( options::ufssSymBreak() ){
+    std::vector< Node > reps;
+    getRepresentatives( reps );
+    if( d_aloc_cardinality>0 ){
+      d_thss->getSymmetryBreaker()->allocateCardinality( out, d_type, d_aloc_cardinality+1, d_cliques[ d_aloc_cardinality ], reps );
+    }else{
+      std::vector< Node > clique;
+      clique.push_back( d_cardinality_term );
+      std::vector< std::vector< Node > > cliques;
+      cliques.push_back( clique );
+      d_thss->getSymmetryBreaker()->allocateCardinality( out, d_type, 1, cliques, reps );
     }
   }
-  d_aloc_cardinality++;
+  */
+  d_aloc_cardinality = d_aloc_cardinality + 1;
 
   //check for abort case
   if( options::ufssAbortCardinality()==d_aloc_cardinality ){
@@ -969,7 +1031,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     if( applyTotality( d_aloc_cardinality ) ){
       //must generate new cardinality lemma term
       Node var;
-      if( d_aloc_cardinality==1 ){
+      if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){
         //get arbitrary ground term
         var = d_cardinality_term;
       }else{
@@ -1013,8 +1075,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 }
 
 bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+  Node s;
   if( r->hasSplits() ){
-    Node s;
     if( !options::ufssSmartSplits() ){
       //take the first split you find
       for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
@@ -1038,13 +1100,31 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
         }
       }
     }
+    Assert( s!=Node::null() );
+  }else{
+    if( !options::ufssMinimalModel() ){
+      //since candidate clique is not reported, we may need to find splits manually
+      for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+        if ( it->second->d_valid ){
+          for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){
+            if ( it->second!=it2->second && it2->second->d_valid ){
+              if( !r->isDisequal( it->first, it2->first, 1 ) ){
+                s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first );
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  if (!s.isNull() ){
     //add lemma to output channel
-    Assert( s!=Node::null() && s.getKind()==EQUAL );
+    Assert( s.getKind()==EQUAL );
     s = Rewriter::rewrite( s );
     Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
     if( options::sortInference()) {
       for( int i=0; i<2; i++ ){
-        int si = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] );
+        int si = d_thss->getSortInference()->getSortId( s[i] );
         Trace("uf-ss-split-si") << si << " ";
       }
       Trace("uf-ss-split-si")  << std::endl;
@@ -1071,6 +1151,12 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
+  //debugging information
+  if( options::ufssSymBreak() ){
+    std::vector< Node > clique_vec;
+    clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
+    addClique( d_cardinality, clique_vec );
+  }
   if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
     //add as lemma
     std::vector< Node > eqs;
@@ -1083,16 +1169,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
     }
     eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
     Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
-    Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl;
+    Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
     ++( d_thss->d_statistics.d_clique_lemmas );
     out->lemma( lem );
   }else{
-    //debugging information
-    if( Trace.isOn("uf-ss-cliques") ){
-      std::vector< Node > clique_vec;
-      clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
-      d_cliques[ d_cardinality ].push_back( clique_vec );
-    }
     //found a clique
     Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
     Debug("uf-ss-cliques") << "   ";
@@ -1217,19 +1297,49 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
 }
 
 void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
-  Node cardLit = d_cardinality_literal[ cardinality ];
-  std::vector< Node > eqs;
-  for( int i=0; i<cardinality; i++ ){
-    eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
+  if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
+    if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
+      d_totality_lems[n].push_back( cardinality );
+      Node cardLit = d_cardinality_literal[ cardinality ];
+      int sort_id = 0;
+      if( options::sortInference() ){
+        sort_id = d_thss->getSortInference()->getSortId(n);
+      }
+      Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl;
+      int use_cardinality = cardinality;
+      if( options::ufssTotalitySymBreak() ){
+        if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){
+          use_cardinality = d_sym_break_index[n];
+        }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()<cardinality-1 ){
+          use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1;
+          d_sym_break_terms[n.getType()][sort_id].push_back( n );
+          d_sym_break_index[n] = use_cardinality;
+          Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl;
+        }
+      }
+
+      std::vector< Node > eqs;
+      for( int i=0; i<use_cardinality; i++ ){
+        eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
+      }
+      Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+      Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
+      Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
+      //send as lemma to the output channel
+      d_thss->getOutputChannel().lemma( lem );
+      ++( d_thss->d_statistics.d_totality_lemmas );
+    }
   }
-  Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
-  Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
-  Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
-  //send as lemma to the output channel
-  d_thss->getOutputChannel().lemma( lem );
-  ++( d_thss->d_statistics.d_totality_lemmas );
 }
 
+void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) {
+
+  if( d_clique_trie[c].add( clique ) ){
+    d_cliques[ c ].push_back( clique );
+  }
+}
+
+
 /** apply totality */
 bool StrongSolverTheoryUF::SortModel::applyTotality( int cardinality ){
   return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
@@ -1307,22 +1417,16 @@ int StrongSolverTheoryUF::SortModel::getNumRegions(){
 }
 
 void StrongSolverTheoryUF::SortModel::getRepresentatives( std::vector< Node >& reps ){
-  //if( !options::ufssColoringSat() ){
-    bool foundRegion = false;
-    for( int i=0; i<(int)d_regions_index; i++ ){
-      //should not have multiple regions at this point
-      if( foundRegion ){
-        Assert( !d_regions[i]->d_valid );
-      }
-      if( d_regions[i]->d_valid ){
-        //this is the only valid region
-        d_regions[i]->getRepresentatives( reps );
-        foundRegion = true;
-      }
+  for( int i=0; i<(int)d_regions_index; i++ ){
+    //should not have multiple regions at this point
+    //if( foundRegion ){
+    //  Assert( !d_regions[i]->d_valid );
+    //}
+    if( d_regions[i]->d_valid ){
+      //this is the only valid region
+      d_regions[i]->getRepresentatives( reps );
     }
-  //}else{
-  //  Unimplemented("Build representatives for fmf region sat is not implemented");
-  //}
+  }
 }
 
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
@@ -1343,6 +1447,15 @@ d_rep_model_init( c )
   }else{
     d_deq_prop = NULL;
   }
+  if( options::ufssSymBreak() ){
+    d_sym_break = new SubsortSymmetryBreaker( th->getQuantifiersEngine(), c );
+  }else{
+    d_sym_break = NULL;
+  }
+}
+
+SortInference* StrongSolverTheoryUF::getSortInference() {
+  return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
 }
 
 /** get default sat context */
@@ -1361,6 +1474,9 @@ void StrongSolverTheoryUF::newEqClass( Node n ){
   if( c ){
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << n << " : " << n.getType() << std::endl;
     c->newEqClass( n );
+    if( options::ufssSymBreak() ){
+      d_sym_break->newEqClass( n );
+    }
   }
 }
 
@@ -1467,6 +1583,10 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
         break;
       }
     }
+    //check symmetry breaker
+    if( !d_conflict && options::ufssSymBreak() ){
+      d_sym_break->check( level );
+    }
     //disambiguate terms if necessary
     //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
     //  Assert( d_term_amb!=NULL );
@@ -1502,7 +1622,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
     SortModel* rm = NULL;
     if( tn.isSort() ){
       Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
-      rm  = new SortModel( n, d_th->getSatContext(), this );
+      rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
     }else{
       /*
       if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
@@ -1572,6 +1692,14 @@ int StrongSolverTheoryUF::getCardinality( Node n ) {
   }
 }
 
+int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
+  std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+  if( it!=d_rep_model.end() && it->second ){
+    return it->second->getCardinality();
+  }
+  return -1;
+}
+
 void StrongSolverTheoryUF::getRepresentatives( Node n, std::vector< Node >& reps ){
   SortModel* c = getSortModel( n );
   if( c ){
@@ -1626,6 +1754,7 @@ 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)
 {
@@ -1633,6 +1762,7 @@ StrongSolverTheoryUF::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_clique_lemmas);
   StatisticsRegistry::registerStat(&d_split_lemmas);
   StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
+  StatisticsRegistry::registerStat(&d_sym_break_lemmas);
   StatisticsRegistry::registerStat(&d_totality_lemmas);
   StatisticsRegistry::registerStat(&d_max_model_size);
 }
@@ -1642,6 +1772,7 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_clique_lemmas);
   StatisticsRegistry::unregisterStat(&d_split_lemmas);
   StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
+  StatisticsRegistry::unregisterStat(&d_sym_break_lemmas);
   StatisticsRegistry::unregisterStat(&d_totality_lemmas);
   StatisticsRegistry::unregisterStat(&d_max_model_size);
 }
@@ -1785,4 +1916,4 @@ DisequalityPropagator::Statistics::Statistics():
 
 DisequalityPropagator::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(& d_propagations);
-}
\ No newline at end of file
+}
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 0cc995723..8e568444b 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -26,7 +26,13 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class SortInference;
+
 namespace theory {
+
+class SubsortSymmetryBreaker;
+
 namespace uf {
 
 class TheoryUF;
@@ -40,11 +46,14 @@ protected:
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDList<bool> BoolList;
-  typedef context::CDList<bool> IntList;
   typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
 public:
   /** information for incremental conflict/clique finding for a particular sort */
   class SortModel {
+  private:
+    std::map< Node, std::vector< int > > d_totality_lems;
+    std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
+    std::map< Node, int > d_sym_break_index;
   public:
     /** a partition of the current equality graph for which cliques can occur internally */
     class Region {
@@ -146,6 +155,8 @@ public:
     public:
       /** check for cliques */
       bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
+      /** get candidate clique */
+      bool getCandidateClique( int cardinality, std::vector< Node >& clique );
       //print debug
       void debugPrint( const char* c, bool incClique = false );
     };
@@ -196,12 +207,29 @@ public:
     /** add totality axiom */
     void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
   private:
+    class NodeTrie {
+      std::map< Node, NodeTrie > d_children;
+    public:
+      bool add( std::vector< Node >& n, unsigned i = 0 ){
+        Assert( i<n.size() );
+        if( i==(n.size()-1) ){
+          bool ret = d_children.find( n[i] )==d_children.end();
+          d_children[n[i]].d_children.clear();
+          return ret;
+        }else{
+          return d_children[n[i]].add( n, i+1 );
+        }
+      }
+    };
+    std::map< int, NodeTrie > d_clique_trie;
+    void addClique( int c, std::vector< Node >& clique );
+  private:
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
     /** cardinality */
     context::CDO< int > d_cardinality;
     /** maximum allocated cardinality */
-    int d_aloc_cardinality;
+    context::CDO< int > d_aloc_cardinality;
     /** cardinality lemma term */
     Node d_cardinality_term;
     /** cardinality totality terms */
@@ -222,7 +250,7 @@ public:
     /** get totality lemma terms */
     Node getTotalityLemmaTerm( int cardinality, int i );
   public:
-    SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss );
+    SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
     virtual ~SortModel(){}
     /** initialize */
     void initialize( OutputChannel* out );
@@ -280,6 +308,8 @@ private:
   TermDisambiguator* d_term_amb;
   /** disequality propagator */
   DisequalityPropagator* d_deq_prop;
+  /** symmetry breaking techniques */
+  SubsortSymmetryBreaker* d_sym_break;
 public:
   StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
   ~StrongSolverTheoryUF() {}
@@ -289,6 +319,10 @@ public:
   TermDisambiguator* getTermDisambiguator() { return d_term_amb; }
   /** disequality propagator */
   DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
+  /** symmetry breaker */
+  SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; }
+  /** get sort inference module */
+  SortInference* getSortInference();
   /** get default sat context */
   context::Context* getSatContext();
   /** get default output channel */
@@ -330,8 +364,10 @@ public:
   TypeNode getCardinalityType( int i ) { return d_conf_types[i]; }
   /** get is in conflict */
   bool isConflict() { return d_conflict; }
-  /** get cardinality for sort */
+  /** get cardinality for node */
   int getCardinality( Node n );
+  /** get cardinality for type */
+  int getCardinality( TypeNode tn );
   /** get representatives */
   void getRepresentatives( Node n, std::vector< Node >& reps );
   /** minimize */
@@ -343,6 +379,7 @@ 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();