Statically eliminate redundant sygus constructors (#1560)

17 files changed, 460 insertions, 439 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 4720186f4..0006a8521 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -463,6 +463,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus_grammar_cons.h \
 	theory/quantifiers/sygus_grammar_norm.cpp \
 	theory/quantifiers/sygus_grammar_norm.h \
+	theory/quantifiers/sygus_grammar_red.cpp \
+	theory/quantifiers/sygus_grammar_red.h \
 	theory/quantifiers/sygus_process_conj.cpp \
 	theory/quantifiers/sygus_process_conj.h \
 	theory/quantifiers/sygus_sampler.cpp \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c58313390..48a577faf 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -270,8 +270,6 @@ option sygusQePreproc --sygus-qe-preproc bool :default false
   
 option sygusMinGrammar --sygus-min-grammar bool :default true
   statically minimize sygus grammars
-option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false
-  aggressively minimize sygus grammars
 option sygusAddConstGrammar --sygus-add-const-grammar bool :default true
   statically add constants appearing in conjecture to grammars
 option sygusGrammarNorm --sygus-grammar-norm bool :default false
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 14de0ac6d..cc8edadd0 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -516,6 +516,18 @@ Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
 #endif
 }
 
+Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt)
+{
+  std::vector<Node> splits;
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    Node test = mkTester(n, i, dt);
+    splits.push_back(test);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  return splits.size() == 1 ? splits[0] : nm->mkNode(kind::OR, splits);
+}
+
 bool DatatypesRewriter::isNullaryApplyConstructor(Node n)
 {
   Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index fb9c02e94..8d9ddbf50 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -61,6 +61,12 @@ public:
  static int isTester(Node n);
  /** make tester is-C( n ), where C is the i^{th} constructor of dt */
  static Node mkTester(Node n, int i, const Datatype& dt);
+ /** make tester split
+  *
+  * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
+  * are the constructors of n's type (dt).
+  */
+ static Node mkSplit(Node n, const Datatype& dt);
  /** returns true iff n is a constructor term with no datatype children */
  static bool isNullaryApplyConstructor(Node n);
  /** returns true iff c is a constructor with no datatype children */
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 0f204383a..5198b44d0 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -34,40 +34,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-Node SygusSplitNew::getSygusSplit( quantifiers::TermDbSygus * tds, Node n, const Datatype& dt ) {
-  TypeNode tnn = n.getType();
-  tds->registerSygusType( tnn );
-  std::vector< Node > curr_splits;
-  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-    Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << dt[i].getName() << " : ";
-    if( !tds->isGenericRedundant( tnn, i ) ){
-      std::vector< Node > test_c;
-      test_c.push_back( DatatypesRewriter::mkTester( n, i, dt ) );
-      Node test = test_c.size()==1 ? test_c[0] : NodeManager::currentNM()->mkNode( AND, test_c );
-      curr_splits.push_back( test );
-      Trace("sygus-split-debug2") << "SUCCESS" << std::endl;
-      Trace("sygus-split-debug") << "Disjunct #" << curr_splits.size() << " : " << test << std::endl;
-    }else{
-      Trace("sygus-split-debug2") << "redundant operator" << std::endl;
-    }
-  }
-  Assert( !curr_splits.empty() );
-  return curr_splits.size()==1 ? curr_splits[0] : NodeManager::currentNM()->mkNode( OR, curr_splits );
-
-}
- 
-void SygusSplitNew::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) {
-  Assert( dt.isSygus() );
-  if( d_splits.find( n )==d_splits.end() ){
-    Trace("sygus-split") << "Get sygus splits " << n << std::endl;
-    Node split = getSygusSplit( d_tds, n, dt );
-    Assert( !split.isNull() );
-    d_splits[n].push_back( split );
-  }
-  //copy to splits
-  splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
-}
-
 SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
                                    quantifiers::TermDbSygus* tds,
                                    context::Context* c)
@@ -209,39 +175,42 @@ void SygusSymBreakNew::assertIsConst( Node n, bool polarity, std::vector< Node >
 }
 
 Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
+  NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > comm_disj;
   // (1) size of left is greater than size of right
-  Node sz_less = NodeManager::currentNM()->mkNode( GT, NodeManager::currentNM()->mkNode( DT_SIZE, n1 ), 
-                                                       NodeManager::currentNM()->mkNode( DT_SIZE, n2 ) );
+  Node sz_less =
+      nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
   comm_disj.push_back( sz_less );
   // (2) ...or sizes are equal and first child is less by term order
-  std::vector< Node > sz_eq_cases; 
-  Node sz_eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( DT_SIZE, n1 ), 
-                                                        NodeManager::currentNM()->mkNode( DT_SIZE, n2 ) );
+  std::vector<Node> sz_eq_cases;
+  Node sz_eq =
+      nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
   sz_eq_cases.push_back( sz_eq );
   if( options::sygusOpt1() ){
     TypeNode tnc = n1.getType();
     const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
     for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
-      if( !d_tds->isGenericRedundant( tnc, j ) ){
-        std::vector< Node > case_conj;
-        for( unsigned k=0; k<j; k++ ){
-          if( !d_tds->isGenericRedundant( tnc, k ) ){
-            case_conj.push_back( DatatypesRewriter::mkTester( n2, k, cdt ).negate() );
-          }
-        }
-        if( !case_conj.empty() ){
-          Node corder = NodeManager::currentNM()->mkNode( kind::OR, DatatypesRewriter::mkTester( n1, j, cdt ).negate(),
-                                                          case_conj.size()==1 ? case_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, case_conj ) );
-          sz_eq_cases.push_back( corder );
-        }
+      std::vector<Node> case_conj;
+      for (unsigned k = 0; k < j; k++)
+      {
+        case_conj.push_back(DatatypesRewriter::mkTester(n2, k, cdt).negate());
+      }
+      if (!case_conj.empty())
+      {
+        Node corder = nm->mkNode(
+            kind::OR,
+            DatatypesRewriter::mkTester(n1, j, cdt).negate(),
+            case_conj.size() == 1 ? case_conj[0]
+                                  : nm->mkNode(kind::AND, case_conj));
+        sz_eq_cases.push_back(corder);
       }
     }
   }
-  Node sz_eqc = sz_eq_cases.size()==1 ? sz_eq_cases[0] : NodeManager::currentNM()->mkNode( kind::AND, sz_eq_cases );
+  Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0]
+                                        : nm->mkNode(kind::AND, sz_eq_cases);
   comm_disj.push_back( sz_eqc );
-  
-  return NodeManager::currentNM()->mkNode( kind::OR, comm_disj );
+
+  return nm->mkNode(kind::OR, comm_disj);
 }
   
 void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
@@ -441,13 +410,14 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
         std::vector< Node > disj;
         bool excl = false;
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          if( !d_tds->isGenericRedundant( ntn, i ) ){
-            int sindexi = dt[i].getSelectorIndexInternal( selExpr );
-            if( sindexi!=-1 ){
-              disj.push_back( DatatypesRewriter::mkTester( n[0], i, dt ) );
-            }else{
-              excl = true;
-            }
+          int sindexi = dt[i].getSelectorIndexInternal(selExpr);
+          if (sindexi != -1)
+          {
+            disj.push_back(DatatypesRewriter::mkTester(n[0], i, dt));
+          }
+          else
+          {
+            excl = true;
           }
         }
         Assert( !disj.empty() );
@@ -624,28 +594,36 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
                 TypeNode tnc = nc.getType();
                 const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
                 for( unsigned k=0; k<cdt.getNumConstructors(); k++ ){
-                  // if not already generic redundant
-                  if( !d_tds->isGenericRedundant( tnc, k ) ){
-                    Kind nck = d_tds->getConsNumKind( tnc, k );
-                    bool red = false;
-                    //check if the argument is redundant
-                    if( nck!=UNDEFINED_KIND ){
-                      Trace("sygus-sb-simple-debug") << "  argument " << j << " " << k << " is : " << nck << std::endl;
-                      red = !d_tds->considerArgKind( tnc, tn, nck, nk, j );
+                  Kind nck = d_tds->getConsNumKind(tnc, k);
+                  bool red = false;
+                  // check if the argument is redundant
+                  if (nck != UNDEFINED_KIND)
+                  {
+                    Trace("sygus-sb-simple-debug")
+                        << "  argument " << j << " " << k << " is : " << nck
+                        << std::endl;
+                    red = !d_tds->considerArgKind(tnc, tn, nck, nk, j);
+                  }
+                  else
+                  {
+                    Node cc = d_tds->getConsNumConst(tnc, k);
+                    if (!cc.isNull())
+                    {
+                      Trace("sygus-sb-simple-debug")
+                          << "  argument " << j << " " << k
+                          << " is constant : " << cc << std::endl;
+                      red = !d_tds->considerConst(tnc, tn, cc, nk, j);
                     }else{
-                      Node cc = d_tds->getConsNumConst( tnc, k  );
-                      if( !cc.isNull() ){
-                        Trace("sygus-sb-simple-debug") << "  argument " << j << " " << k << " is constant : " << cc << std::endl;
-                        red = !d_tds->considerConst( tnc, tn, cc, nk, j );
-                      }else{
-                        //defined function?
-                      }
-                    }
-                    if( red ){
-                      Trace("sygus-sb-simple-debug") << "  ...redundant." << std::endl;
-                      sbp_conj.push_back( DatatypesRewriter::mkTester( nc, k, cdt ).negate() );
+                      // defined function?
                     }
                   }
+                  if (red)
+                  {
+                    Trace("sygus-sb-simple-debug")
+                        << "  ...redundant." << std::endl;
+                    sbp_conj.push_back(
+                        DatatypesRewriter::mkTester(nc, k, cdt).negate());
+                  }
                 }
               }
             }
@@ -1192,16 +1170,6 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   }
 }
 
-void SygusSymBreakNew::getPossibleCons( const Datatype& dt, TypeNode tn, std::vector< bool >& pcons ) {
-  Assert( pcons.size()==dt.getNumConstructors() );
-  d_tds->registerSygusType( tn );
-  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-    if( d_tds->isGenericRedundant( tn, i ) ){
-      pcons[i] = false;
-    }
-  }
-}
-
 bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ) {
   Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
   if( Trace.isOn("sygus-sb-warn") ){
@@ -1222,7 +1190,7 @@ bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node
     Trace("sygus-sb-warn") << "- has tester : " << tst << " : " << ( hastst ? "true" : "false" );
     Trace("sygus-sb-warn") << ", value=" << tstrep << std::endl;
     if( !hastst ){
-      Node split = SygusSplitNew::getSygusSplit( d_tds, n, dt );
+      Node split = DatatypesRewriter::mkSplit(n, dt);
       Assert( !split.isNull() );
       lemmas.push_back( split );
       return false;
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 1162f767f..ff2d2a873 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -39,19 +39,6 @@ namespace datatypes {
 
 class TheoryDatatypes;
 
-class SygusSplitNew
-{
-private:
-  quantifiers::TermDbSygus * d_tds;
-  std::map< Node, std::vector< Node > > d_splits;
-public:
-  SygusSplitNew( quantifiers::TermDbSygus * tds ) : d_tds( tds ){}
-  virtual ~SygusSplitNew(){}
-  /** get sygus splits */
-  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas );
-  static Node getSygusSplit( quantifiers::TermDbSygus * tds, Node n, const Datatype& dt );
-};
-
 class SygusSymBreakNew
 {
 private:
@@ -184,7 +171,6 @@ public:
   void assertFact( Node n, bool polarity, std::vector< Node >& lemmas );
   void preRegisterTerm( TNode n, std::vector< Node >& lemmas  );
   void check( std::vector< Node >& lemmas );
-  void getPossibleCons( const Datatype& dt, TypeNode tn, std::vector< bool >& pcons );
 public:
   Node getNextDecisionRequest( unsigned& priority, std::vector< Node >& lemmas );
 };
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c17c022a1..d91eace99 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -74,7 +74,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
   d_dtfCounter = 0;
 
-  d_sygus_split = NULL;
   d_sygus_sym_break = NULL;
 }
 
@@ -85,7 +84,6 @@ TheoryDatatypes::~TheoryDatatypes() {
     Assert(current != NULL);
     delete current;
   }
-  delete d_sygus_split;
   delete d_sygus_sym_break;
 }
 
@@ -309,27 +307,7 @@ void TheoryDatatypes::check(Effort e) {
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
-                    std::vector< Node > children;
-                    if( dt.isSygus() && d_sygus_split ){
-                      Trace("dt-split") << "DtSygus : split on " << n
-                                        << std::endl;
-                      std::vector< Node > lemmas;
-                      d_sygus_split->getSygusSplits( n, dt, children, lemmas );
-                      Trace("dt-split") << "Finished compute split, returned "
-                                        << lemmas.size() << " lemmas."
-                                        << std::endl;
-                      for( unsigned i=0; i<lemmas.size(); i++ ){
-                        Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
-                        doSendLemma( lemmas[i] );
-                      }
-                    }else{
-                      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                        Node test = DatatypesRewriter::mkTester( n, i, dt );
-                        children.push_back( test );
-                      }
-                    }
-                    Assert( !children.empty() );
-                    Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
+                    Node lemma = DatatypesRewriter::mkSplit(n, dt);
                     Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
                     //doSendLemma( lemma );
                     d_out->lemma( lemma, false, false, true );
@@ -551,7 +529,6 @@ void TheoryDatatypes::finishInit() {
   if( getQuantifiersEngine() && options::ceGuidedInst() ){
     quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
     Assert( tds!=NULL );
-    d_sygus_split = new SygusSplitNew( tds );
     d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
   }
 }
@@ -1026,10 +1003,6 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
         Assert( tindex!=-1 );
         pcons[ tindex ] = false;
       }
-      //further limit the possibilities based on grammar minimization
-      if( d_sygus_sym_break && dt.isSygus() ){
-        d_sygus_sym_break->getPossibleCons( dt, tn, pcons );
-      }
     }
   }
 }
@@ -1157,7 +1130,7 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
               break;
             }
           }
-          Assert( dt.isSygus() || testerIndex!=-1 );
+          Assert(testerIndex != -1);
           //we must explain why each term in the set of testers for this equivalence class is equal
           std::vector< Node > eq_terms;
           NodeBuilder<> nb(kind::AND);
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index b3d88bb1c..a3001d042 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -321,9 +321,9 @@ private:
   bool areCareDisequal( TNode x, TNode y );
   TNode getRepresentative( TNode a );
 private:
-  /** sygus utilities */
-  SygusSplitNew * d_sygus_split;
-  SygusSymBreakNew * d_sygus_sym_break;
+ /** sygus symmetry breaking utility */
+ SygusSymBreakNew* d_sygus_sym_break;
+
 public:
   Node getNextDecisionRequest( unsigned& priority );
 };/* class TheoryDatatypes */
diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp
index 67c40d6aa..1b5cd3452 100644
--- a/src/theory/quantifiers/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus_grammar_norm.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus_grammar_red.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -118,6 +119,20 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
   Trace("sygus-grammar-normalize") << "---------------------------------\n";
 }
 
+void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm,
+                                             TypeObject& to,
+                                             const Datatype& dt,
+                                             std::vector<unsigned>& op_pos)
+{
+  std::vector<unsigned> difference;
+  std::set_difference(op_pos.begin(),
+                      op_pos.end(),
+                      d_drop_indices.begin(),
+                      d_drop_indices.end(),
+                      std::back_inserter(difference));
+  op_pos = difference;
+}
+
 /* TODO #1304: have more operators and types. Moreover, have more general ways
    of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
    function should realize that it is chainable for integers */
@@ -264,7 +279,33 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
 {
   NodeManager* nm = NodeManager::currentNM();
   TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
-  /* TODO #1304: step 0: look for redundant constructors to drop */
+  Trace("sygus-gnorm") << "Infer transf for " << dt.getName() << "..."
+                       << std::endl;
+  Trace("sygus-gnorm") << "  #cons = " << op_pos.size() << " / "
+                       << dt.getNumConstructors() << std::endl;
+  // look for redundant constructors to drop
+  if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
+  {
+    SygusRedundantCons src;
+    src.initialize(d_qe, tn);
+    std::vector<unsigned> rindices;
+    src.getRedundant(rindices);
+    if (!rindices.empty())
+    {
+      Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/"
+                           << op_pos.size() << " constructors." << std::endl;
+      Assert(rindices.size() < op_pos.size());
+      return new TransfDrop(rindices);
+    }
+  }
+
+  // if normalization option is not enabled, we do not infer the transformations
+  // below
+  if (!options::sygusGrammarNorm())
+  {
+    return nullptr;
+  }
+
   /* TODO #1304: step 1: look for singleton */
   /* step 2: look for chain */
   unsigned chain_op_pos = dt.getNumConstructors();
@@ -319,6 +360,7 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
   /* Typenode admits a chain transformation for normalization */
   if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
   {
+    Trace("sygus-gnorm") << "...chain transf." << std::endl;
     Trace("sygus-grammar-normalize-infer")
         << "\tInfering chain transformation\n";
     return new TransfChain(chain_op_pos, elem_pos);
@@ -372,19 +414,16 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
   }
   /* Creates type object for normalization */
   TypeObject to(tn, unres_tn);
-  /* If normalization option enabled, infer transformations to be applied in the
-   * type */
-  if (options::sygusGrammarNorm())
+
+  /* Determine normalization transformation based on sygus type and given
+    * operators */
+  Transf* transformation = inferTransf(tn, dt, op_pos);
+  /* If a transformation was selected, apply it */
+  if (transformation != nullptr)
   {
-    /* Determine normalization transformation based on sygus type and given
-     * operators */
-    Transf* transformation = inferTransf(tn, dt, op_pos);
-    /* If a transformation was selected, apply it */
-    if (transformation != nullptr)
-    {
-      transformation->buildType(this, to, dt, op_pos);
-    }
+    transformation->buildType(this, to, dt, op_pos);
   }
+
   /* Remaining operators are rebuilt as they are */
   for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
   {
diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h
index 38e3f168e..d1894ac2e 100644
--- a/src/theory/quantifiers/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus_grammar_norm.h
@@ -254,6 +254,25 @@ class SygusGrammarNorm
                            std::vector<unsigned>& op_pos) = 0;
   }; /* class Transf */
 
+  /** Drop transformation class
+   *
+   * This class builds a type by dropping a set of redundant constructors,
+   * whose indices are given as input to the constructor of this class.
+   */
+  class TransfDrop : public Transf
+  {
+   public:
+    TransfDrop(std::vector<unsigned>& indices) : d_drop_indices(indices) {}
+    /** build type */
+    virtual void buildType(SygusGrammarNorm* sygus_norm,
+                           TypeObject& to,
+                           const Datatype& dt,
+                           std::vector<unsigned>& op_pos);
+
+   private:
+    std::vector<unsigned> d_drop_indices;
+  };
+
   /** Chain transformation class
    *
    * Determines how to build normalized types by chaining the application of one
@@ -275,7 +294,7 @@ class SygusGrammarNorm
   class TransfChain : public Transf
   {
    public:
-    TransfChain(unsigned chain_op_pos, std::vector<unsigned> elem_pos)
+    TransfChain(unsigned chain_op_pos, std::vector<unsigned>& elem_pos)
         : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
 
     /** builds types encoding a chain in which each link contains a repetition
diff --git a/src/theory/quantifiers/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus_grammar_red.cpp
new file mode 100644
index 000000000..056fc455a
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_red.cpp
@@ -0,0 +1,136 @@
+/*********************                                                        */
+/*! \file sygus_grammar_red.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Implementation of sygus_grammar_red
+ **/
+
+#include "theory/quantifiers/sygus_grammar_red.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
+{
+  Assert(qe != nullptr);
+  Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
+  d_type = tn;
+  Assert(tn.isDatatype());
+  TermDbSygus* tds = qe->getTermDatabaseSygus();
+  tds->registerSygusType(tn);
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  TypeNode btn = TypeNode::fromType(dt.getSygusType());
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
+                       << std::endl;
+    std::map<int, Node> pre;
+    Node g = tds->mkGeneric(dt, i, pre);
+    Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
+    Assert(g.getNumChildren() == dt[i].getNumArgs());
+    d_gen_terms[i] = g;
+    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+    {
+      pre[j] = g[j];
+    }
+    std::vector<Node> glist;
+    getGenericList(tds, dt, i, 0, pre, glist);
+    // call the extended rewriter
+    bool red = false;
+    for (const Node& gr : glist)
+    {
+      Trace("sygus-red-debug") << "  ...variant : " << gr << std::endl;
+      std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr);
+      if (itg != d_gen_cons.end() && itg->second != i)
+      {
+        red = true;
+        Trace("sygus-red") << "  ......redundant, since a variant of " << g
+                           << " and " << d_gen_terms[itg->second]
+                           << " both rewrite to " << gr << std::endl;
+        break;
+      }
+      else
+      {
+        d_gen_cons[gr] = i;
+        Trace("sygus-red") << "  ......not redundant." << std::endl;
+      }
+    }
+    d_sygus_red_status.push_back(red ? 1 : 0);
+  }
+}
+
+void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
+{
+  const Datatype& dt = static_cast<DatatypeType>(d_type.toType()).getDatatype();
+  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    if (isRedundant(i))
+    {
+      indices.push_back(i);
+    }
+  }
+}
+
+bool SygusRedundantCons::isRedundant(unsigned i)
+{
+  Assert(i < d_sygus_red_status.size());
+  return d_sygus_red_status[i] == 1;
+}
+
+void SygusRedundantCons::getGenericList(TermDbSygus* tds,
+                                        const Datatype& dt,
+                                        unsigned c,
+                                        unsigned index,
+                                        std::map<int, Node>& pre,
+                                        std::vector<Node>& terms)
+{
+  if (index == dt[c].getNumArgs())
+  {
+    Node gt = tds->mkGeneric(dt, c, pre);
+    gt = tds->getExtRewriter()->extendedRewrite(gt);
+    terms.push_back(gt);
+    return;
+  }
+  // with no swap
+  getGenericList(tds, dt, c, index + 1, pre, terms);
+  // swapping is exponential, only use for operators with small # args.
+  if (dt[c].getNumArgs() <= 5)
+  {
+    TypeNode atype = tds->getArgType(dt[c], index);
+    for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++)
+    {
+      if (tds->getArgType(dt[c], s) == atype)
+      {
+        // swap s and index
+        Node tmp = pre[s];
+        pre[s] = pre[index];
+        pre[index] = tmp;
+        getGenericList(tds, dt, c, index + 1, pre, terms);
+        // revert
+        tmp = pre[s];
+        pre[s] = pre[index];
+        pre[index] = tmp;
+      }
+    }
+  }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus_grammar_red.h b/src/theory/quantifiers/sygus_grammar_red.h
new file mode 100644
index 000000000..b65a12da2
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_red.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file sygus_grammar_red.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 sygus_grammar_red
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+
+#include <map>
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** SygusRedundantCons
+ *
+ * This class computes the subset of indices of the constructors of a sygus type
+ * that are redundant. To use this class, first call initialize( qe, tn ),
+ * where tn is a sygus tn. Then, use getRedundant and/or isRedundant to get the
+ * indicies of the constructors of tn that are redundant.
+ */
+class SygusRedundantCons
+{
+ public:
+  SygusRedundantCons() {}
+  ~SygusRedundantCons() {}
+  /** register type tn
+   *
+   * qe : pointer to the quantifiers engine,
+   * tn : the (sygus) type to compute redundant constructors for
+   */
+  void initialize(QuantifiersEngine* qe, TypeNode tn);
+  /** Get the indices of the redundant constructors of the register type */
+  void getRedundant(std::vector<unsigned>& indices);
+  /**
+   * This function returns true if the i^th constructor of the registered type
+   * is redundant.
+   */
+  bool isRedundant(unsigned i);
+
+ private:
+  /** the registered type */
+  TypeNode d_type;
+  /** redundant status
+   *
+   * For each constructor, status indicating whether the constructor is
+   * redundant, where:
+   *
+   * 0 : not redundant,
+   * 1 : redundant since another constructor can be used to construct values for
+   * this constructor.
+   *
+   * For example, for grammar:
+   *   A -> C > B | B < C | not D
+   *   B -> x | y
+   *   C -> 0 | 1 | C+C
+   *   D -> B >= C
+   * If A is register with this class, then we store may store { 0, 1, 0 },
+   * noting that the second constructor of A can be simulated with the first.
+   * Notice that the third constructor is not considered redundant.
+   */
+  std::vector<int> d_sygus_red_status;
+  /**
+   * Map from constructor indices to the generic term for that constructor,
+   * where the generic term for a constructor is the (canonical) term returned
+   * by a call to TermDbSygus::mkGeneric.
+   */
+  std::map<unsigned, Node> d_gen_terms;
+  /**
+   * Map from the rewritten form of generic terms for constructors of the
+   * registered type to their corresponding constructor index.
+   */
+  std::map<Node, unsigned> d_gen_cons;
+  /** get generic list
+   *
+   * This function constructs all well-typed variants of a term of the form
+   *    op( x1, ..., xn )
+   * where op is the builtin operator for dt[c], and xi = pre[i] for i=1,...,n.
+   *
+   * It constructs a list of terms of the form g * sigma, where sigma
+   * is an automorphism on { x1...xn } such that for all xi -> xj in sigma,
+   * the type for arguments i and j of dt[c] are the same. We store this
+   * list of terms in terms.
+   *
+   * This function recurses on the arguments of g, index is the current argument
+   * we are processing, and pre stores the current arguments of
+   *
+   * For example, for a sygus grammar
+   *   A -> and( A, A, B )
+   *   B -> false
+   * passing arguments such that g=and( x1, x2, x3 ) to this function will add:
+   *   and( x1, x2, x3 ) and and( x2, x1, x3 )
+   * to terms.
+   */
+  void getGenericList(TermDbSygus* tds,
+                      const Datatype& dt,
+                      unsigned c,
+                      unsigned index,
+                      std::map<int, Node>& pre,
+                      std::vector<Node>& terms);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 82720dd5e..f824cd6f7 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -468,9 +468,9 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   Assert(dt.isSygus());
   Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
-  Trace("sygus-sample-grammar") << "Sygus random value " << tn
-                                << ", depth = " << depth
-                                << ", rchance = " << rchance << std::endl;
+  Trace("sygus-sample-grammar")
+      << "Sygus random value " << tn << ", depth = " << depth
+      << ", rchance = " << rchance << std::endl;
   // check if we terminate on this call
   // we refuse to enumerate terms of 10+ depth as a hard limit
   bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10;
@@ -480,12 +480,12 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
   unsigned ncons = cindices.size();
   // select a random constructor, or random value when index=ncons.
   unsigned index = Random::getRandom().pick(0, ncons);
-  Trace("sygus-sample-grammar") << "Random index 0..." << ncons
-                                << " was : " << index << std::endl;
+  Trace("sygus-sample-grammar")
+      << "Random index 0..." << ncons << " was : " << index << std::endl;
   if (index < ncons)
   {
-    Trace("sygus-sample-grammar") << "Recurse constructor index #" << index
-                                  << std::endl;
+    Trace("sygus-sample-grammar")
+        << "Recurse constructor index #" << index << std::endl;
     unsigned cindex = cindices[index];
     Assert(cindex < dt.getNumConstructors());
     const DatatypeConstructor& dtc = dt[cindex];
@@ -504,8 +504,8 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
         Trace("sygus-sample-grammar") << "...fail." << std::endl;
         break;
       }
-      Trace("sygus-sample-grammar") << "  child #" << i << " : " << c
-                                    << std::endl;
+      Trace("sygus-sample-grammar")
+          << "  child #" << i << " : " << c << std::endl;
       pre[i] = c;
     }
     if (success)
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 7d7cc624e..cda652ee7 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -109,8 +109,12 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   return d_fv_stype[v];
 }
 
-Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) {
-  Assert( c>=0 && c<(int)dt.getNumConstructors() );
+Node TermDbSygus::mkGeneric(const Datatype& dt,
+                            unsigned c,
+                            std::map<TypeNode, int>& var_count,
+                            std::map<int, Node>& pre)
+{
+  Assert(c < dt.getNumConstructors());
   Assert( dt.isSygus() );
   Assert( !dt[c].getSygusOp().isNull() );
   std::vector< Node > children;
@@ -119,7 +123,8 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
     children.push_back( op );
   }
   Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
-  for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
+  for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
+  {
     TypeNode tna = getArgType( dt[c], i );
     Node a;
     std::map< int, Node >::iterator it = pre.find( i );
@@ -128,11 +133,14 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
     }else{
       a = getFreeVarInc( tna, var_count, true );
     }
+    Trace("sygus-db-debug")
+        << "  child " << i << " : " << a << " : " << a.getType() << std::endl;
     Assert( !a.isNull() );
     children.push_back( a );
   }
   Node ret;
   if( op.getKind()==BUILTIN ){
+    Trace("sygus-db-debug") << "Make builtin node..." << std::endl;
     ret = NodeManager::currentNM()->mkNode( op, children );
   }else{
     Kind ok = getOperatorKind( op );
@@ -196,19 +204,6 @@ Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& ar
   return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() );
 }
 
-Node TermDbSygus::getNormalized(TypeNode t, Node prog)
-{
-  std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
-  if( itn==d_normalized[t].end() ){
-    Node progr = Rewriter::rewrite( prog );
-    Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
-    d_normalized[t][prog] = progr;
-    return progr;
-  }else{
-    return itn->second;
-  }
-}
-
 unsigned TermDbSygus::getSygusTermSize( Node n ){
   if( n.getNumChildren()==0 ){
     return 0;
@@ -226,23 +221,6 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){
   }
 }
 
-unsigned TermDbSygus::getSygusConstructors( Node n, std::vector< Node >& cons ) {
-  Assert( n.getKind()==APPLY_CONSTRUCTOR );
-  Node op = n.getOperator();
-  if( std::find( cons.begin(), cons.end(), op )==cons.end() ){
-    cons.push_back( op );
-  }
-  if( n.getNumChildren()==0 ){
-    return 0;
-  }else{
-    unsigned sum = 0;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      sum += getSygusConstructors( n[i], cons );
-    }
-    return 1+sum;
-  }
-}
-
 class ReqTrie {
 public:
   ReqTrie() : d_req_kind( UNDEFINED_KIND ){}
@@ -632,49 +610,6 @@ int TermDbSygus::solveForArgument( TypeNode tn, unsigned cindex, unsigned arg )
   return -1;
 }
 
-class ReconstructTrie {
-public:
-  std::map< Node, ReconstructTrie > d_children;
-  std::vector< Node > d_reconstruct;
-  void add( std::vector< Node >& cons, Node r, unsigned index = 0 ){
-    if( index==cons.size() ){
-      d_reconstruct.push_back( r );
-    }else{
-      d_children[cons[index]].add( cons, r, index+1 );
-    }
-  }
-  Node getReconstruct( std::map< Node, int >& rcons, unsigned depth ) {
-    if( !d_reconstruct.empty() ){
-      for( unsigned i=0; i<d_reconstruct.size(); i++ ){
-        Node r = d_reconstruct[i];
-        if( rcons[r]==0 ){
-          Trace("sygus-static-enum") << "...eliminate constructor " << r << std::endl;
-          rcons[r] = 1;
-          return r;
-        }
-      }
-    }
-    if( depth>0 ){
-      for( unsigned w=0; w<2; w++ ){
-        for( std::map< Node, ReconstructTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-          Node n = it->first;
-          if( ( w==0 && rcons[n]!=0 ) || ( w==1 && rcons[n]==0 ) ){
-            Node r = it->second.getReconstruct( rcons, depth - w );
-            if( !r.isNull() ){
-              if( w==1 ){
-                Trace("sygus-static-enum") << "...use " << n << " to eliminate constructor " << r << std::endl;
-                rcons[n] = -1;
-              }
-              return r;
-            }
-          }
-        }
-      }
-    }
-    return Node::null();
-  }
-};
-
 void TermDbSygus::registerSygusType( TypeNode tn ) {
   std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
   if( itr==d_register.end() ){
@@ -723,147 +658,6 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
             registerSygusType( getArgType( dt[i], j ) );
           }
         }
-        
-        //compute the redundant operators
-        if( options::sygusMinGrammar() ){
-          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-            bool nred = true;
-            Trace("sygus-split-debug") << "Is " << dt[i].getName() << " a redundant operator?" << std::endl;
-            Kind ck = getConsNumKind( tn, i );
-            if( ck!=UNDEFINED_KIND ){
-              Kind dk;
-              if (TermUtil::isAntisymmetric(ck, dk))
-              {
-                int j = getKindConsNum( tn, dk );
-                if( j!=-1 ){
-                  Trace("sygus-split-debug") << "Possible redundant operator : " << ck << " with " << dk << std::endl;
-                  //check for type mismatches
-                  bool success = true;
-                  for( unsigned k=0; k<2; k++ ){
-                    unsigned ko = k==0 ? 1 : 0;
-                    TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
-                    TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
-                    if( tni!=tnj ){
-                      Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
-                      success = false;
-                      break;
-                    }
-                  }
-                  if( success ){
-                    Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << ck << " terms." << std::endl;
-                    nred = false;
-                  }
-                }
-              }
-            }
-            if( nred ){
-              Trace("sygus-split-debug") << "Check " << dt[i].getName() << " based on generic rewriting" << std::endl;
-              std::map< TypeNode, int > var_count;
-              std::map< int, Node > pre;
-              Node g = mkGeneric( dt, i, var_count, pre );
-              nred = !computeGenericRedundant( tn, g );
-              Trace("sygus-split-debug") << "...done check " << dt[i].getName() << " based on generic rewriting" << std::endl;
-            }
-            d_sygus_red_status[tn].push_back( nred ? 0 : 1 );
-          }
-          // run an enumerator for this type
-          if( options::sygusMinGrammarAgg() ){
-            TypeEnumerator te(tn);
-            unsigned count = 0;
-            std::map< Node, std::vector< Node > > builtin_to_orig;
-            Trace("sygus-static-enum") << "Static enumerate " << dt.getName() << "..." << std::endl;
-            while( !te.isFinished() && count<1000 ){
-              Node n = *te;
-              Node bn = sygusToBuiltin( n, tn );
-              Trace("sygus-static-enum") << "  " << bn;
-              Node bnr = Rewriter::rewrite( bn );
-              Trace("sygus-static-enum") << "  ..." << bnr << std::endl;
-              builtin_to_orig[bnr].push_back( n );
-              ++te;
-              count++;
-            }
-            std::map< Node, bool > reserved;
-            for( unsigned i=0; i<=2; i++ ){
-              Node rsv =
-                  i == 2 ? d_quantEngine->getTermUtil()->getTypeMaxValue(btn)
-                         : d_quantEngine->getTermUtil()->getTypeValue(btn, i);
-              if( !rsv.isNull() ){
-                reserved[ rsv ] = true;
-              }
-            }
-            Trace("sygus-static-enum") << "...make the reconstruct index data structure..." << std::endl;
-            ReconstructTrie rt;
-            std::map< Node, int > rcons;
-            unsigned max_depth = 0;
-            for( std::map< Node, std::vector< Node > >::iterator itb = builtin_to_orig.begin(); itb != builtin_to_orig.end(); ++itb ){
-              if( itb->second.size()>0 ){
-                std::map< Node, std::vector< Node > > clist;
-                Node single_cons;
-                for( unsigned j=0; j<itb->second.size(); j++ ){
-                  Node e = itb->second[j];
-                  getSygusConstructors( e, clist[e] );
-                  if( clist[e].size()>max_depth ){
-                    max_depth = clist[e].size();
-                  }
-                  for( unsigned k=0; k<clist[e].size(); k++ ){
-                    /*
-                    unsigned cindex = Datatype::indexOf( clist[e][k].toExpr() );
-                    if( isGenericRedundant( tn, cindex ) ){
-                      is_gen_redundant = true;
-                      break;
-                    }else{
-                    */
-                    rcons[clist[e][k]] = 0;
-                  }
-                  //if( is_gen_redundant ){
-                  //  clist.erase( e );
-                  //}else{
-                  if( clist[e].size()==1 ){
-                    Trace("sygus-static-enum") << "...single constructor term : " << e << ", builtin is " << itb->first << ", cons is " << clist[e][0] << std::endl;
-                    if( single_cons.isNull() ){
-                      single_cons = clist[e][0];
-                    }else{
-                      Trace("sygus-static-enum") << "*** already can eliminate constructor " << clist[e][0] << std::endl;
-                      unsigned cindex =  Datatype::indexOf( clist[e][0].toExpr() );
-                      d_sygus_red_status[tn][cindex] = 1;
-                    }
-                  }
-                  //}
-                }
-                // do not eliminate 0, 1, or max
-                if( !single_cons.isNull() && reserved.find( itb->first )==reserved.end() ){
-                  Trace("sygus-static-enum") << "...possibly elim " << single_cons << std::endl;
-                  for( std::map< Node, std::vector< Node > >::iterator itc = clist.begin(); itc != clist.end(); ++itc ){
-                    if( std::find( itc->second.begin(), itc->second.end(), single_cons )==itc->second.end() ){
-                      rt.add( itc->second, single_cons );
-                    }
-                  }
-                }
-              }
-            }
-            Trace("sygus-static-enum") << "...compute reconstructions..." << std::endl;
-            Node next_rcons;
-            do {
-              unsigned depth = 0;
-              do{
-                next_rcons = rt.getReconstruct( rcons, depth );
-                depth++;
-              }while( next_rcons.isNull() && depth<=max_depth );
-              // if we found a constructor to eliminate
-              if( !next_rcons.isNull() ){
-                Trace("sygus-static-enum") << "*** eliminate constructor " << next_rcons << std::endl;
-                unsigned cindex =  Datatype::indexOf( next_rcons.toExpr() );
-                d_sygus_red_status[tn][cindex] = 2;
-              }
-            }while( !next_rcons.isNull() );
-            Trace("sygus-static-enum") << "...finished..." << std::endl;
-          }
-        }else{
-          // assume all are non-redundant
-          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-            d_sygus_red_status[tn].push_back( 0 );
-          }
-        }
       }
     }
   }
@@ -980,11 +774,10 @@ unsigned TermDbSygus::getMinTermSize( TypeNode tn ) {
   if( it==d_min_term_size.end() ){
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      if( !isGenericRedundant( tn, i ) ){
-        if( dt[i].getNumArgs()==0 ){
-          d_min_term_size[tn] = 0;
-          return 0;
-        }
+      if (dt[i].getNumArgs() == 0)
+      {
+        d_min_term_size[tn] = 0;
+        return 0;
       }
     }
     // TODO : improve
@@ -997,7 +790,6 @@ unsigned TermDbSygus::getMinTermSize( TypeNode tn ) {
 
 unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
   Assert( isRegistered( tn ) );
-  Assert( !isGenericRedundant( tn, cindex ) );
   std::map< unsigned, unsigned >::iterator it = d_min_cons_term_size[tn].find( cindex );
   if( it==d_min_cons_term_size[tn].end() ){
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -1140,8 +932,9 @@ bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
   }
 }
 
-TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
-  Assert( i>=0 && i<(int)c.getNumArgs() );
+TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i)
+{
+  Assert(i < c.getNumArgs());
   return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
 }
 
@@ -1688,40 +1481,6 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) {
   return evaluateWithUnfolding( n, visited );
 }
 
-bool TermDbSygus::computeGenericRedundant( TypeNode tn, Node g ) {
-  //everything added to this cache should be mutually exclusive cases
-  std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
-  if( it==d_gen_redundant[tn].end() ){
-    Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
-    Node gr = getNormalized(tn, g);
-    Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
-    std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
-    bool red = true;
-    if( itg==d_gen_terms[tn].end() ){
-      red = false;
-      d_gen_terms[tn][gr] = g;
-      Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
-      Trace("sygus-nf-reg") << "*** Sygus (generic) normal form : normal form of " << g << " is " << gr << std::endl;
-    }else{
-      Trace("sygus-gnf-debug") << "...redundant." << std::endl;
-      Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
-    }
-    d_gen_redundant[tn][g] = red;
-    return red;
-  }else{
-    return it->second;
-  }
-}
-
-bool TermDbSygus::isGenericRedundant( TypeNode tn, unsigned i ) {
-  Assert( i<d_sygus_red_status[tn].size() );
-  if( options::sygusMinGrammarAgg() ){
-    return d_sygus_red_status[tn][i]!=0;
-  }else{
-    return d_sygus_red_status[tn][i]==1;
-  }
-}
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index af1ef50b6..b9af26b6e 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -103,7 +103,7 @@ class TermDbSygus {
    *     and var_count[Ti] is incremented.
    */
   Node mkGeneric(const Datatype& dt,
-                 int c,
+                 unsigned c,
                  std::map<TypeNode, int>& var_count,
                  std::map<int, Node>& pre);
   /** same as above, but with empty var_count */
@@ -178,8 +178,6 @@ private:
   std::map<TypeNode, std::map<Node, int> > d_ops;
   std::map<TypeNode, std::map<int, Node> > d_arg_ops;
   std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
-  // normalized map
-  std::map<TypeNode, std::map<Node, Node> > d_normalized;
   // grammar information
   // root -> type -> _
   std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
@@ -215,7 +213,7 @@ private:
   bool isKindArg( TypeNode tn, int i );
   bool isConstArg( TypeNode tn, int i );
   /** get arg type */
-  TypeNode getArgType( const DatatypeConstructor& c, int i );
+  TypeNode getArgType(const DatatypeConstructor& c, unsigned i);
   /** get first occurrence */
   int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
   /** is type match */
@@ -226,8 +224,6 @@ private:
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);
   unsigned getSygusTermSize( Node n );
-  // returns size
-  unsigned getSygusConstructors( Node n, std::vector< Node >& cons );
   /** given a term, construct an equivalent smaller one that respects syntax */
   Node minimizeBuiltinTerm( Node n );
   /** given a term, expand it into more basic components */
@@ -281,18 +277,6 @@ public:
   Node evaluateWithUnfolding(
       Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
   Node evaluateWithUnfolding( Node n );
-//for calculating redundant operators
-private:
-  //whether each constructor is redundant
-  // 0 : not redundant, 1 : redundant, 2 : partially redundant
-  std::map< TypeNode, std::vector< int > > d_sygus_red_status;
-  // type to (rewritten) to original
-  std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
-  std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
-  //compute generic redundant
-  bool computeGenericRedundant( TypeNode tn, Node g );
-public:
-  bool isGenericRedundant( TypeNode tn, unsigned i );
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 9b9f1feb2..9e7427eb0 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -78,7 +78,8 @@ TESTS = commutative.sy \
         hd-19-d1-prog-dup-op.sy \
         real-grammar-neg.sy \
         real-si-all.sy  \
-        c100.sy
+        c100.sy \
+        check-generic-red.sy
 
 # disabled, takes too long with and without CBQI BV
 # Base16_1.sy
diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy
new file mode 100644
index 000000000..917c1473a
--- /dev/null
+++ b/test/regress/regress0/sygus/check-generic-red.sy
@@ -0,0 +1,19 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic LIA)
+
+(synth-fun P ((x Int) (y Int)) Bool
+  ((Start Bool ((and Start Start)
+                (not Start)
+                (<= StartInt StartIntC)
+                (<= StartInt StartInt)
+                (>= StartInt StartInt)
+                (<= StartIntC StartInt)
+                (>= StartIntC StartInt)
+                (<= StartIntC StartIntC)
+                ))
+   (StartIntC Int (0 0 1))
+   (StartInt Int (x y 0 1))))
+
+(constraint (P 0 2))
+(check-synth)