Document/refactor datatypes sygus simple symmetry breaking (#2233)

8 files changed, 717 insertions, 455 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 677b99d9a..c2a620f57 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -370,6 +370,8 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes_type_rules.h \
 	theory/datatypes/type_enumerator.cpp \
 	theory/datatypes/type_enumerator.h \
+	theory/datatypes/sygus_simple_sym.cpp \
+	theory/datatypes/sygus_simple_sym.h \
 	theory/ext_theory.cpp \
 	theory/ext_theory.h \
 	theory/fp/theory_fp.cpp \
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d95a5763c..aea449fd1 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -35,14 +35,16 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
 SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
-                                   quantifiers::TermDbSygus* tds,
+                                   QuantifiersEngine* qe,
                                    context::Context* c)
     : d_td(td),
-      d_tds(tds),
+      d_tds(qe->getTermDatabaseSygus()),
+      d_ssb(qe),
       d_testers(c),
       d_testers_exp(c),
       d_active_terms(c),
-      d_currTermSize(c) {
+      d_currTermSize(c)
+{
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_true = NodeManager::currentNM()->mkConst(true);
 }
@@ -481,7 +483,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
     std::map<unsigned, unsigned> children_solved;
     for (unsigned j = 0; j < dt_index_nargs; j++)
     {
-      int i = d_tds->solveForArgument(tn, tindex, j);
+      int i = d_ssb.solveForArgument(tn, tindex, j);
       if (i >= 0)
       {
         children_solved[j] = i;
@@ -622,7 +624,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
             {
               Trace("sygus-sb-simple-debug") << "  argument " << j << " " << k
                                              << " is : " << nck << std::endl;
-              red = !d_tds->considerArgKind(tnc, tn, nck, nk, j);
+              red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j);
             }
             else
             {
@@ -632,7 +634,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
                 Trace("sygus-sb-simple-debug")
                     << "  argument " << j << " " << k << " is constant : " << cc
                     << std::endl;
-                red = !d_tds->considerConst(tnc, tn, cc, nk, j);
+                red = !d_ssb.considerConst(tnc, tn, cc, nk, j);
                 if (usingAnyConstCons)
                 {
                   // we only consider concrete constant constructors
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 5f6ca935d..c5f3fe560 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -29,6 +29,7 @@
 #include "context/context.h"
 #include "expr/datatype.h"
 #include "expr/node.h"
+#include "theory/datatypes/sygus_simple_sym.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus_sampler.h"
@@ -60,7 +61,7 @@ class SygusSymBreakNew
 
  public:
   SygusSymBreakNew(TheoryDatatypes* td,
-                   quantifiers::TermDbSygus* tds,
+                   QuantifiersEngine* qe,
                    context::Context* c);
   ~SygusSymBreakNew();
   /**
@@ -117,6 +118,8 @@ class SygusSymBreakNew
   TheoryDatatypes* d_td;
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
+  /** the simple symmetry breaking utility */
+  SygusSimpleSymBreak d_ssb;
   /**
    * Map from terms to the index of the tester that is asserted for them in
    * the current SAT context. In other words, if d_testers[n] = 2, then the
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
new file mode 100644
index 000000000..4aef1231c
--- /dev/null
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -0,0 +1,594 @@
+/*********************                                                        */
+/*! \file sygus_simple_sym.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 simple symmetry breaking for sygus
+ **/
+
+#include "theory/datatypes/sygus_simple_sym.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
+    : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil())
+{
+}
+
+/** Requirement trie
+ *
+ * This class is used to make queries about sygus grammars, including what
+ * constructors they contain, and their types.
+ *
+ * As a simple example, consider the trie:
+ * root:
+ *   d_req_kind = PLUS
+ *   d_children[0]:
+ *     d_req_type = A
+ *   d_children[1]:
+ *     d_req_type = A
+ * This trie is satisfied by sygus types that have a constructor whose builtin
+ * kind is PLUS and whose argument types are both A.
+ */
+class ReqTrie
+{
+ public:
+  ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
+  /** the children of this node */
+  std::map<unsigned, ReqTrie> d_children;
+  /** the (builtin) kind required by this node */
+  Kind d_req_kind;
+  /** the type that this node is required to be */
+  TypeNode d_req_type;
+  /** the constant required by this node */
+  Node d_req_const;
+  /** print this trie */
+  void print(const char* c, int indent = 0)
+  {
+    if (d_req_kind != UNDEFINED_KIND)
+    {
+      Trace(c) << d_req_kind << " ";
+    }
+    else if (!d_req_type.isNull())
+    {
+      Trace(c) << d_req_type;
+    }
+    else if (!d_req_const.isNull())
+    {
+      Trace(c) << d_req_const;
+    }
+    else
+    {
+      Trace(c) << "_";
+    }
+    Trace(c) << std::endl;
+    for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
+         it != d_children.end();
+         ++it)
+    {
+      for (int i = 0; i <= indent; i++)
+      {
+        Trace(c) << "  ";
+      }
+      Trace(c) << it->first << " : ";
+      it->second.print(c, indent + 1);
+    }
+  }
+  /**
+   * Are the requirements of this trie satisfied by sygus type tn?
+   * tdb is a reference to the sygus term database.
+   */
+  bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
+  {
+    if (!d_req_const.isNull())
+    {
+      if (!tdb->hasConst(tn, d_req_const))
+      {
+        return false;
+      }
+    }
+    if (!d_req_type.isNull())
+    {
+      Trace("sygus-sb-debug")
+          << "- check if " << tn << " is type " << d_req_type << std::endl;
+      if (tn != d_req_type)
+      {
+        return false;
+      }
+    }
+    if (d_req_kind != UNDEFINED_KIND)
+    {
+      Trace("sygus-sb-debug")
+          << "- check if " << tn << " has " << d_req_kind << std::endl;
+      std::vector<TypeNode> argts;
+      if (tdb->canConstructKind(tn, d_req_kind, argts))
+      {
+        bool ret = true;
+        for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
+             it != d_children.end();
+             ++it)
+        {
+          if (it->first < argts.size())
+          {
+            TypeNode tnc = argts[it->first];
+            if (!it->second.satisfiedBy(tdb, tnc))
+            {
+              return false;
+            }
+          }
+          else
+          {
+            return false;
+          }
+        }
+        if (!ret)
+        {
+          return false;
+        }
+      }
+      else
+      {
+        return false;
+      }
+    }
+    return true;
+  }
+  /** is this the empty (trivially satisfied) trie? */
+  bool empty()
+  {
+    return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
+           && d_req_type.isNull() && d_children.empty();
+  }
+};
+
+bool SygusSimpleSymBreak::considerArgKind(
+    TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
+{
+  const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
+  const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+  Assert(d_tds->hasKind(tn, k));
+  Assert(d_tds->hasKind(tnp, pk));
+  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
+                          << ", arg = " << arg << " in " << tnp << "?"
+                          << std::endl;
+  int c = d_tds->getKindConsNum(tn, k);
+  int pc = d_tds->getKindConsNum(tnp, pk);
+  // check for associativity
+  if (k == pk && quantifiers::TermUtil::isAssoc(k))
+  {
+    // if the operator is associative, then a repeated occurrence should only
+    // occur in the leftmost argument position
+    int firstArg = getFirstArgOccurrence(pdt[pc], tn);
+    Assert(firstArg != -1);
+    if (arg == firstArg)
+    {
+      return true;
+    }
+    // the argument types of the child must be the parent's type
+    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
+    {
+      TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
+      if (tn != tnp)
+      {
+        return true;
+      }
+    }
+    Trace("sygus-sb-simple")
+        << "  sb-simple : do not consider " << k << " at child arg " << arg
+        << " of " << k
+        << " since it is associative, with first arg = " << firstArg
+        << std::endl;
+    return false;
+  }
+  // describes the shape of an alternate term to construct
+  //  we check whether this term is in the sygus grammar below
+  ReqTrie rt;
+  Assert(rt.empty());
+
+  // construct rt by cases
+  if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
+  {
+    // negation normal form
+    if (pk == k)
+    {
+      rt.d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+    }
+    else
+    {
+      Kind reqk = UNDEFINED_KIND;      // required kind for all children
+      std::map<unsigned, Kind> reqkc;  // required kind for some children
+      if (pk == NOT)
+      {
+        if (k == AND)
+        {
+          rt.d_req_kind = OR;
+          reqk = NOT;
+        }
+        else if (k == OR)
+        {
+          rt.d_req_kind = AND;
+          reqk = NOT;
+        }
+        else if (k == EQUAL)
+        {
+          rt.d_req_kind = XOR;
+        }
+        else if (k == XOR)
+        {
+          rt.d_req_kind = EQUAL;
+        }
+        else if (k == ITE)
+        {
+          rt.d_req_kind = ITE;
+          reqkc[1] = NOT;
+          reqkc[2] = NOT;
+          rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+        }
+        else if (k == LEQ || k == GT)
+        {
+          //  (not (~ x y)) ----->  (~ (+ y 1) x)
+          rt.d_req_kind = k;
+          rt.d_children[0].d_req_kind = PLUS;
+          rt.d_children[0].d_children[0].d_req_type =
+              TypeNode::fromType(dt[c].getArgType(1));
+          rt.d_children[0].d_children[1].d_req_const =
+              NodeManager::currentNM()->mkConst(Rational(1));
+          rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+        }
+        else if (k == LT || k == GEQ)
+        {
+          //  (not (~ x y)) ----->  (~ y (+ x 1))
+          rt.d_req_kind = k;
+          rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+          rt.d_children[1].d_req_kind = PLUS;
+          rt.d_children[1].d_children[0].d_req_type =
+              TypeNode::fromType(dt[c].getArgType(0));
+          rt.d_children[1].d_children[1].d_req_const =
+              NodeManager::currentNM()->mkConst(Rational(1));
+        }
+      }
+      else if (pk == BITVECTOR_NOT)
+      {
+        if (k == BITVECTOR_AND)
+        {
+          rt.d_req_kind = BITVECTOR_OR;
+          reqk = BITVECTOR_NOT;
+        }
+        else if (k == BITVECTOR_OR)
+        {
+          rt.d_req_kind = BITVECTOR_AND;
+          reqk = BITVECTOR_NOT;
+        }
+        else if (k == BITVECTOR_XNOR)
+        {
+          rt.d_req_kind = BITVECTOR_XOR;
+        }
+        else if (k == BITVECTOR_XOR)
+        {
+          rt.d_req_kind = BITVECTOR_XNOR;
+        }
+      }
+      else if (pk == UMINUS)
+      {
+        if (k == PLUS)
+        {
+          rt.d_req_kind = PLUS;
+          reqk = UMINUS;
+        }
+      }
+      else if (pk == BITVECTOR_NEG)
+      {
+        if (k == PLUS)
+        {
+          rt.d_req_kind = PLUS;
+          reqk = BITVECTOR_NEG;
+        }
+      }
+      if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
+      {
+        int pcr = d_tds->getKindConsNum(tnp, rt.d_req_kind);
+        if (pcr != -1)
+        {
+          Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
+          // must have same number of arguments
+          if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
+          {
+            for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
+            {
+              Kind rk = reqk;
+              if (reqk == UNDEFINED_KIND)
+              {
+                std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
+                if (itr != reqkc.end())
+                {
+                  rk = itr->second;
+                }
+              }
+              if (rk != UNDEFINED_KIND)
+              {
+                rt.d_children[i].d_req_kind = rk;
+                rt.d_children[i].d_children[0].d_req_type =
+                    TypeNode::fromType(dt[c].getArgType(i));
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  else if (k == MINUS || k == BITVECTOR_SUB)
+  {
+    if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
+        || pk == LT || pk == GEQ || pk == GT)
+    {
+      int oarg = arg == 0 ? 1 : 0;
+      //  (~ x (- y z))  ---->  (~ (+ x z) y)
+      //  (~ (- y z) x)  ---->  (~ y (+ x z))
+      rt.d_req_kind = pk;
+      rt.d_children[arg].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+      rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
+      rt.d_children[oarg].d_children[0].d_req_type =
+          TypeNode::fromType(pdt[pc].getArgType(oarg));
+      rt.d_children[oarg].d_children[1].d_req_type =
+          TypeNode::fromType(dt[c].getArgType(1));
+    }
+    else if (pk == PLUS || pk == BITVECTOR_PLUS)
+    {
+      //  (+ x (- y z))  -----> (- (+ x y) z)
+      //  (+ (- y z) x)  -----> (- (+ x y) z)
+      rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
+      int oarg = arg == 0 ? 1 : 0;
+      rt.d_children[0].d_req_kind = pk;
+      rt.d_children[0].d_children[0].d_req_type =
+          TypeNode::fromType(pdt[pc].getArgType(oarg));
+      rt.d_children[0].d_children[1].d_req_type =
+          TypeNode::fromType(dt[c].getArgType(0));
+      rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+    }
+  }
+  else if (k == ITE)
+  {
+    if (pk != ITE)
+    {
+      //  (o X (ite y z w) X')  -----> (ite y (o X z X') (o X w X'))
+      rt.d_req_kind = ITE;
+      rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+      unsigned n_args = pdt[pc].getNumArgs();
+      for (unsigned r = 1; r <= 2; r++)
+      {
+        rt.d_children[r].d_req_kind = pk;
+        for (unsigned q = 0; q < n_args; q++)
+        {
+          if ((int)q == arg)
+          {
+            rt.d_children[r].d_children[q].d_req_type =
+                TypeNode::fromType(dt[c].getArgType(r));
+          }
+          else
+          {
+            rt.d_children[r].d_children[q].d_req_type =
+                TypeNode::fromType(pdt[pc].getArgType(q));
+          }
+        }
+      }
+      // this increases term size but is probably a good idea
+    }
+  }
+  else if (k == NOT)
+  {
+    if (pk == ITE)
+    {
+      //  (ite (not y) z w)  -----> (ite y w z)
+      rt.d_req_kind = ITE;
+      rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+      rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(2));
+      rt.d_children[2].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+    }
+  }
+  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
+                          << ", arg = " << arg << "?" << std::endl;
+  if (!rt.empty())
+  {
+    rt.print("sygus-sb-debug");
+    // check if it meets the requirements
+    if (rt.satisfiedBy(d_tds, tnp))
+    {
+      Trace("sygus-sb-debug") << "...success!" << std::endl;
+      Trace("sygus-sb-simple")
+          << "  sb-simple : do not consider " << k << " as arg " << arg
+          << " of " << pk << std::endl;
+      // do not need to consider the kind in the search since there are ways to
+      // construct equivalent terms
+      return false;
+    }
+    else
+    {
+      Trace("sygus-sb-debug") << "...failed." << std::endl;
+    }
+    Trace("sygus-sb-debug") << std::endl;
+  }
+  // must consider this kind in the search
+  return true;
+}
+
+bool SygusSimpleSymBreak::considerConst(
+    TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
+{
+  const Datatype& pdt = static_cast<DatatypeType>(tnp.toType()).getDatatype();
+  // child grammar-independent
+  if (!considerConst(pdt, tnp, c, pk, arg))
+  {
+    return false;
+  }
+  // this can probably be made child grammar independent
+  int pc = d_tds->getKindConsNum(tnp, pk);
+  if (pdt[pc].getNumArgs() == 2)
+  {
+    Kind ok;
+    int offset;
+    if (d_tutil->hasOffsetArg(pk, arg, offset, ok))
+    {
+      Trace("sygus-sb-simple-debug")
+          << pk << " has offset arg " << ok << " " << offset << std::endl;
+      int ok_arg = d_tds->getKindConsNum(tnp, ok);
+      if (ok_arg != -1)
+      {
+        Trace("sygus-sb-simple-debug")
+            << "...at argument " << ok_arg << std::endl;
+        // other operator be the same type
+        if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
+        {
+          int status;
+          Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status);
+          Trace("sygus-sb-simple-debug")
+              << c << " with offset " << offset << " is " << co
+              << ", status=" << status << std::endl;
+          if (status == 0 && !co.isNull())
+          {
+            if (d_tds->hasConst(tn, co))
+            {
+              Trace("sygus-sb-simple")
+                  << "  sb-simple : by offset reasoning, do not consider const "
+                  << c;
+              Trace("sygus-sb-simple")
+                  << " as arg " << arg << " of " << pk << " since we can use "
+                  << co << " under " << ok << " " << std::endl;
+              return false;
+            }
+          }
+        }
+      }
+    }
+  }
+  return true;
+}
+
+bool SygusSimpleSymBreak::considerConst(
+    const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg)
+{
+  Assert(d_tds->hasKind(tnp, pk));
+  int pc = d_tds->getKindConsNum(tnp, pk);
+  bool ret = true;
+  Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
+                          << ", arg = " << arg << "?" << std::endl;
+  if (d_tutil->isIdempotentArg(c, pk, arg))
+  {
+    if (pdt[pc].getNumArgs() == 2)
+    {
+      int oarg = arg == 0 ? 1 : 0;
+      TypeNode otn = TypeNode::fromType(pdt[pc].getArgType(oarg));
+      if (otn == tnp)
+      {
+        Trace("sygus-sb-simple")
+            << "  sb-simple : " << c << " is idempotent arg " << arg << " of "
+            << pk << "..." << std::endl;
+        ret = false;
+      }
+    }
+  }
+  else
+  {
+    Node sc = d_tutil->isSingularArg(c, pk, arg);
+    if (!sc.isNull())
+    {
+      if (d_tds->hasConst(tnp, sc))
+      {
+        Trace("sygus-sb-simple")
+            << "  sb-simple : " << c << " is singular arg " << arg << " of "
+            << pk << ", evaluating to " << sc << "..." << std::endl;
+        ret = false;
+      }
+    }
+  }
+  if (ret)
+  {
+    ReqTrie rt;
+    Assert(rt.empty());
+    Node max_c = d_tutil->getTypeMaxValue(c.getType());
+    Node zero_c = d_tutil->getTypeValue(c.getType(), 0);
+    Node one_c = d_tutil->getTypeValue(c.getType(), 1);
+    if (pk == XOR || pk == BITVECTOR_XOR)
+    {
+      if (c == max_c)
+      {
+        rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
+      }
+    }
+    else if (pk == ITE)
+    {
+      if (arg == 0)
+      {
+        if (c == max_c)
+        {
+          rt.d_children[1].d_req_type = tnp;
+        }
+        else if (c == zero_c)
+        {
+          rt.d_children[2].d_req_type = tnp;
+        }
+      }
+    }
+    else if (pk == STRING_SUBSTR)
+    {
+      if (c == one_c && arg == 2)
+      {
+        rt.d_req_kind = STRING_CHARAT;
+        rt.d_children[0].d_req_type = TypeNode::fromType(pdt[pc].getArgType(0));
+        rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+      }
+    }
+    if (!rt.empty())
+    {
+      // check if satisfied
+      if (rt.satisfiedBy(d_tds, tnp))
+      {
+        Trace("sygus-sb-simple") << "  sb-simple : do not consider const " << c
+                                 << " as arg " << arg << " of " << pk;
+        Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
+        // do not need to consider the constant in the search since there are
+        // ways to construct equivalent terms
+        ret = false;
+      }
+    }
+  }
+  return ret;
+}
+
+int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
+                                          unsigned cindex,
+                                          unsigned arg)
+{
+  // we currently do not solve for arguments
+  return -1;
+}
+
+int SygusSimpleSymBreak::getFirstArgOccurrence(const DatatypeConstructor& c,
+                                               TypeNode tn)
+{
+  for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
+  {
+    TypeNode tni = TypeNode::fromType(c.getArgType(i));
+    if (tni == tn)
+    {
+      return i;
+    }
+  }
+  return -1;
+}
+
+}  // namespace datatypes
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h
new file mode 100644
index 000000000..7fb7f4653
--- /dev/null
+++ b/src/theory/datatypes/sygus_simple_sym.h
@@ -0,0 +1,107 @@
+/*********************                                                        */
+/*! \file sygus_simple_sym.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Simple symmetry breaking for sygus.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#define __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+
+#include <map>
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+/** SygusSimpleSymBreak
+ *
+ * This class implements queries that can be queried statically about sygus
+ * grammars, for example, concerning which constructors need not appear at
+ * argument positions of others. This is used by the sygus extension of the
+ * quantifier-free datatypes procedure for adding symmetry breaking lemmas.
+ * We call this class of techniques "simple static symmetry breaking". These
+ * techniques have the advantage over "dynamic symmetry breaking" (blocking
+ * redundant solutions on demand in datatypes_sygus.h) in that we can design
+ * efficient encodings of symmetry breaking constraints, whereas dynamic
+ * symmetry breaking may in the worst case block solutions one by one.
+ */
+class SygusSimpleSymBreak
+{
+ public:
+  SygusSimpleSymBreak(QuantifiersEngine* qe);
+  ~SygusSimpleSymBreak() {}
+  /** consider argument kind
+   *
+   * This method returns false if the arg^th argument of terms of parent kind
+   * pk need not be of kind k. The type tnp is the sygus type of type
+   * containing pk, and tn is the sygus type of the arg^th argument of the
+   * constructor whose builtin kind is pk.
+   *
+   * For example, given grammar:
+   *   A -> A + A | 0 | 1 | x | -A
+   * This method will return false for inputs such as:
+   *   A, A, -, -, 0  (due to cancelling of double unary minus)
+   *   A, A, +, +, 1  (due to commutativity of addition, we can assume all
+   *                   nested + occurs in the 0^th argument)
+   */
+  bool considerArgKind(TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg);
+  /** consider constant
+   *
+   * Similar to the above function, this method returns false if the arg^th
+   * argument of terms of parent kind pk need not be the constant c. The type
+   * tnp is the sygus type of type containing pk, and tn is the sygus type of
+   * the arg^th argument of the constructor whose builtin kind is pk.
+   *
+   * For example, given grammar:
+   *   A -> B * B | A + A | 0 | 1 | x | -A
+   *   B -> 0 | x
+   * This method will return false for inputs such as:
+   *   A, A, 0, +, 0 (due to identity of addition with zero)
+   *   B, A, 0, *, 0 (due to simplification 0*x --> 0, and 0 is generated by A)
+   */
+  bool considerConst(TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg);
+  /** solve for argument
+   *
+   * If this method returns a non-negative integer n, then all terms at
+   * the arg^th position of the cindex^th constructor of sygus type tnp need
+   * only be of the n^th constructor of that argument.
+   *
+   * For example, given grammar:
+   *   A -> A - A | A + A | 0 | 1 | x | y
+   * Say solveForArgument(A, 0, 0)=2. This indicates that all terms of the form
+   * x1-x2 need only be such that x1 is 0.
+   */
+  int solveForArgument(TypeNode tnp, unsigned cindex, unsigned arg);
+
+ private:
+  /** Pointer to the sygus term database */
+  quantifiers::TermDbSygus* d_tds;
+  /** Pointer to the quantifiers term utility */
+  quantifiers::TermUtil* d_tutil;
+  /** return the index of the first argument position of c that has type tn */
+  int getFirstArgOccurrence(const DatatypeConstructor& c, TypeNode tn);
+  /**
+   * Helper function for consider const above, pdt is the datatype of the type
+   * of tnp.
+   */
+  bool considerConst(
+      const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg);
+};
+
+}  // namespace datatypes
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index cf690af57..f886c6d3f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -540,9 +540,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
 
 void TheoryDatatypes::finishInit() {
   if( getQuantifiersEngine() && options::ceGuidedInst() ){
-    quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
-    Assert( tds!=NULL );
-    d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
+    d_sygus_sym_break =
+        new SygusSymBreakNew(this, getQuantifiersEngine(), getSatContext());
     // do congruence on evaluation functions
     d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
   }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 54e731694..64adea6c5 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -322,417 +322,6 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){
   return weight + sum;
 }
 
-class ReqTrie {
-public:
-  ReqTrie() : d_req_kind( UNDEFINED_KIND ){}
-  std::map< unsigned, ReqTrie > d_children;
-  Kind d_req_kind;
-  TypeNode d_req_type;
-  Node d_req_const;
-  void print( const char * c, int indent = 0 ){
-    if( d_req_kind!=UNDEFINED_KIND ){
-      Trace(c) << d_req_kind << " ";
-    }else if( !d_req_type.isNull() ){
-      Trace(c) << d_req_type;
-    }else if( !d_req_const.isNull() ){
-      Trace(c) << d_req_const;
-    }else{
-      Trace(c) << "_";
-    }
-    Trace(c) << std::endl;
-    for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-      for( int i=0; i<=indent; i++ ) { Trace(c) << "  "; }
-      Trace(c) << it->first << " : ";
-      it->second.print( c, indent+1 );
-    }
-  }
-  bool satisfiedBy( quantifiers::TermDbSygus * tdb, TypeNode tn ){
-    if( !d_req_const.isNull() ){
-      if( !tdb->hasConst( tn, d_req_const ) ){
-        return false;
-      }
-    }
-    if( !d_req_type.isNull() ){
-      Trace("sygus-sb-debug") << "- check if " << tn << " is type "
-                              << d_req_type << std::endl;
-      if( tn!=d_req_type ){
-        return false;
-      }
-    }
-    if( d_req_kind!=UNDEFINED_KIND ){
-      Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind
-                              << std::endl;
-      std::vector<TypeNode> argts;
-      if (tdb->canConstructKind(tn, d_req_kind, argts))
-      {
-        bool ret = true;
-        for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-          if (it->first < argts.size())
-          {
-            TypeNode tnc = argts[it->first];
-            if( !it->second.satisfiedBy( tdb, tnc ) ){
-              return false;
-            }
-          }else{
-            return false;
-          }
-        }
-        if( !ret ){
-          return false;
-        }
-      }else{
-        return false;
-      }
-    }
-    return true;
-  }
-  bool empty()
-  {
-    return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
-           && d_req_type.isNull() && d_children.empty();
-  }
-};
-
-//this function gets all easy redundant cases, before consulting rewriters
-bool TermDbSygus::considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg ) {
-  const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
-  const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-  Assert( hasKind( tn, k ) );
-  Assert( hasKind( tnp, pk ) );
-  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
-                          << ", arg = " << arg << " in " << tnp << "?"
-                          << std::endl;
-  int c = getKindConsNum( tn, k );
-  int pc = getKindConsNum( tnp, pk );
-    //check for associativity
-  if (k == pk && quantifiers::TermUtil::isAssoc(k))
-  {
-    // if the operator is associative, then a repeated occurrence should only
-    // occur in the leftmost argument position
-    int firstArg = getFirstArgOccurrence(pdt[pc], tn);
-    Assert(firstArg != -1);
-    if (arg == firstArg)
-    {
-      return true;
-    }
-    // the argument types of the child must be the parent's type
-    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
-    {
-      TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
-      if (tn != tnp)
-      {
-        return true;
-      }
-    }
-    Trace("sygus-sb-simple")
-        << "  sb-simple : do not consider " << k << " at child arg " << arg
-        << " of " << k
-        << " since it is associative, with first arg = " << firstArg
-        << std::endl;
-    return false;
-  }
-  //describes the shape of an alternate term to construct
-  //  we check whether this term is in the sygus grammar below
-  ReqTrie rt;
-  Assert( rt.empty() );
-  
-  //construct rt by cases
-  if( pk==NOT || pk==BITVECTOR_NOT || pk==UMINUS || pk==BITVECTOR_NEG ){
-    //negation normal form
-    if( pk==k ){
-      rt.d_req_type = getArgType( dt[c], 0 );
-    }else{
-      Kind reqk = UNDEFINED_KIND;       //required kind for all children
-      std::map< unsigned, Kind > reqkc; //required kind for some children
-      if( pk==NOT ){
-        if( k==AND ) {
-          rt.d_req_kind = OR;reqk = NOT;
-        }else if( k==OR ){
-          rt.d_req_kind = AND;reqk = NOT;
-        //AJR : eliminate this if we eliminate xor
-        }else if( k==EQUAL ) {
-          rt.d_req_kind = XOR;
-        }else if( k==XOR ) {
-          rt.d_req_kind = EQUAL;
-        }else if( k==ITE ){
-          rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT;
-          rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
-        }else if( k==LEQ || k==GT ){
-          //  (not (~ x y)) ----->  (~ (+ y 1) x)
-          rt.d_req_kind = k;
-          rt.d_children[0].d_req_kind = PLUS;
-          rt.d_children[0].d_children[0].d_req_type = getArgType( dt[c], 1 );
-          rt.d_children[0].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-          rt.d_children[1].d_req_type = getArgType( dt[c], 0 );
-          //TODO: other possibilities?
-        }else if( k==LT || k==GEQ ){
-          //  (not (~ x y)) ----->  (~ y (+ x 1))
-          rt.d_req_kind = k;
-          rt.d_children[0].d_req_type = getArgType( dt[c], 1 );
-          rt.d_children[1].d_req_kind = PLUS;
-          rt.d_children[1].d_children[0].d_req_type = getArgType( dt[c], 0 );
-          rt.d_children[1].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-        }
-      }else if( pk==BITVECTOR_NOT ){
-        if( k==BITVECTOR_AND ) {
-          rt.d_req_kind = BITVECTOR_OR;reqk = BITVECTOR_NOT;
-        }else if( k==BITVECTOR_OR ){
-          rt.d_req_kind = BITVECTOR_AND;reqk = BITVECTOR_NOT;
-        }else if( k==BITVECTOR_XNOR ) {
-          rt.d_req_kind = BITVECTOR_XOR;
-        }else if( k==BITVECTOR_XOR ) {
-          rt.d_req_kind = BITVECTOR_XNOR;
-        }
-      }else if( pk==UMINUS ){
-        if( k==PLUS ){
-          rt.d_req_kind = PLUS;reqk = UMINUS;
-        }
-      }else if( pk==BITVECTOR_NEG ){
-        if( k==PLUS ){
-          rt.d_req_kind = PLUS;reqk = BITVECTOR_NEG;
-        }
-      }
-      if( !rt.empty() && ( reqk!=UNDEFINED_KIND || !reqkc.empty() ) ){
-        int pcr = getKindConsNum( tnp, rt.d_req_kind );
-        if( pcr!=-1 ){
-          Assert( pcr<(int)pdt.getNumConstructors() );
-          //must have same number of arguments
-          if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
-            for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
-              Kind rk = reqk;
-              if( reqk==UNDEFINED_KIND ){
-                std::map< unsigned, Kind >::iterator itr = reqkc.find( i );
-                if( itr!=reqkc.end() ){
-                  rk = itr->second;
-                }
-              }
-              if( rk!=UNDEFINED_KIND ){
-                rt.d_children[i].d_req_kind = rk;
-                rt.d_children[i].d_children[0].d_req_type = getArgType( dt[c], i );
-              }
-            }
-          }
-        }
-      }
-    }
-  }else if( k==MINUS || k==BITVECTOR_SUB ){
-    if( pk==EQUAL || 
-        pk==MINUS || pk==BITVECTOR_SUB || 
-        pk==LEQ || pk==LT || pk==GEQ || pk==GT ){
-      int oarg = arg==0 ? 1 : 0;
-      //  (~ x (- y z))  ---->  (~ (+ x z) y)
-      //  (~ (- y z) x)  ---->  (~ y (+ x z))
-      rt.d_req_kind = pk;
-      rt.d_children[arg].d_req_type = getArgType( dt[c], 0 );
-      rt.d_children[oarg].d_req_kind = k==MINUS ? PLUS : BITVECTOR_PLUS;
-      rt.d_children[oarg].d_children[0].d_req_type = getArgType( pdt[pc], oarg );
-      rt.d_children[oarg].d_children[1].d_req_type = getArgType( dt[c], 1 );
-    }else if( pk==PLUS || pk==BITVECTOR_PLUS ){
-      //  (+ x (- y z))  -----> (- (+ x y) z)
-      //  (+ (- y z) x)  -----> (- (+ x y) z)
-      rt.d_req_kind = pk==PLUS ? MINUS : BITVECTOR_SUB;
-      int oarg = arg==0 ? 1 : 0;
-      rt.d_children[0].d_req_kind = pk;
-      rt.d_children[0].d_children[0].d_req_type = getArgType( pdt[pc], oarg );
-      rt.d_children[0].d_children[1].d_req_type = getArgType( dt[c], 0 );
-      rt.d_children[1].d_req_type = getArgType( dt[c], 1 );
-      // TODO : this is subsumbed by solving for MINUS
-    }
-  }else if( k==ITE ){
-    if( pk!=ITE ){
-      //  (o X (ite y z w) X')  -----> (ite y (o X z X') (o X w X'))
-      rt.d_req_kind = ITE;
-      rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
-      unsigned n_args = pdt[pc].getNumArgs();
-      for( unsigned r=1; r<=2; r++ ){
-        rt.d_children[r].d_req_kind = pk;
-        for( unsigned q=0; q<n_args; q++ ){
-          if( (int)q==arg ){
-            rt.d_children[r].d_children[q].d_req_type = getArgType( dt[c], r );
-          }else{
-            rt.d_children[r].d_children[q].d_req_type = getArgType( pdt[pc], q );
-          }
-        }
-      }
-      //TODO: this increases term size but is probably a good idea
-    }
-  }else if( k==NOT ){
-    if( pk==ITE ){
-      //  (ite (not y) z w)  -----> (ite y w z)
-      rt.d_req_kind = ITE;
-      rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
-      rt.d_children[1].d_req_type = getArgType( pdt[pc], 2 );
-      rt.d_children[2].d_req_type = getArgType( pdt[pc], 1 );
-    }
-  }
-  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk << ", arg = " << arg << "?" << std::endl;
-  if( !rt.empty() ){
-    rt.print("sygus-sb-debug");
-    //check if it meets the requirements
-    if( rt.satisfiedBy( this, tnp ) ){
-      Trace("sygus-sb-debug") << "...success!" << std::endl;
-      Trace("sygus-sb-simple") << "  sb-simple : do not consider " << k << " as arg " << arg << " of " << pk << std::endl;
-      //do not need to consider the kind in the search since there are ways to construct equivalent terms
-      return false;
-    }else{
-      Trace("sygus-sb-debug") << "...failed." << std::endl;
-    }
-    Trace("sygus-sb-debug") << std::endl;
-  }
-  //must consider this kind in the search  
-  return true;
-}
-
-bool TermDbSygus::considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg ) {
-  const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
-  // child grammar-independent
-  if( !considerConst( pdt, tnp, c, pk, arg ) ){
-    return false;
-  }
-  // TODO : this can probably be made child grammar independent
-  int pc = getKindConsNum( tnp, pk );
-  if( pdt[pc].getNumArgs()==2 ){
-    Kind ok;
-    int offset;
-    if (d_quantEngine->getTermUtil()->hasOffsetArg(pk, arg, offset, ok))
-    {
-      Trace("sygus-sb-simple-debug") << pk << " has offset arg " << ok << " " << offset << std::endl;
-      int ok_arg = getKindConsNum( tnp, ok );
-      if( ok_arg!=-1 ){
-        Trace("sygus-sb-simple-debug") << "...at argument " << ok_arg << std::endl;
-        //other operator be the same type
-        if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){
-          int status;
-          Node co = d_quantEngine->getTermUtil()->getTypeValueOffset(
-              c.getType(), c, offset, status);
-          Trace("sygus-sb-simple-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl;
-          if( status==0 && !co.isNull() ){
-            if( hasConst( tn, co ) ){
-              Trace("sygus-sb-simple") << "  sb-simple : by offset reasoning, do not consider const " << c;
-              Trace("sygus-sb-simple") << " as arg " << arg << " of " << pk << " since we can use " << co << " under " << ok << " " << std::endl;
-              return false;
-            }
-          }
-        }
-      }
-    }
-  }
-  return true;
-}
-
-bool TermDbSygus::considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg ) {
-  Assert( hasKind( tnp, pk ) );
-  int pc = getKindConsNum( tnp, pk );
-  bool ret = true;
-  Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk << ", arg = " << arg << "?" << std::endl;
-  if (d_quantEngine->getTermUtil()->isIdempotentArg(c, pk, arg))
-  {
-    if( pdt[pc].getNumArgs()==2 ){
-      int oarg = arg==0 ? 1 : 0;
-      TypeNode otn = TypeNode::fromType( ((SelectorType)pdt[pc][oarg].getType()).getRangeType() );
-      if( otn==tnp ){
-        Trace("sygus-sb-simple") << "  sb-simple : " << c << " is idempotent arg " << arg << " of " << pk << "..." << std::endl;
-        ret = false;
-      }
-    }
-  }else{
-    Node sc = d_quantEngine->getTermUtil()->isSingularArg(c, pk, arg);
-    if( !sc.isNull() ){
-      if( hasConst( tnp, sc ) ){
-        Trace("sygus-sb-simple") << "  sb-simple : " << c << " is singular arg " << arg << " of " << pk << ", evaluating to " << sc << "..." << std::endl;
-        ret = false;
-      }
-    }
-  }
-  if( ret ){
-    ReqTrie rt;
-    Assert( rt.empty() );
-    Node max_c = d_quantEngine->getTermUtil()->getTypeMaxValue(c.getType());
-    Node zero_c = d_quantEngine->getTermUtil()->getTypeValue(c.getType(), 0);
-    Node one_c = d_quantEngine->getTermUtil()->getTypeValue(c.getType(), 1);
-    if( pk==XOR || pk==BITVECTOR_XOR ){
-      if( c==max_c ){
-        rt.d_req_kind = pk==XOR ? NOT : BITVECTOR_NOT;
-      }
-    }else if( pk==ITE ){
-      if( arg==0 ){
-        if( c==max_c ){
-          rt.d_children[1].d_req_type = tnp;
-        }
-        else if (c == zero_c)
-        {
-          rt.d_children[2].d_req_type = tnp;
-        }
-      }
-    }else if( pk==STRING_SUBSTR ){
-      if (c == one_c && arg == 2)
-      {
-        rt.d_req_kind = STRING_CHARAT;
-        rt.d_children[0].d_req_type = getArgType( pdt[pc], 0 );
-        rt.d_children[1].d_req_type = getArgType( pdt[pc], 1 );
-      }
-    }
-    if( !rt.empty() ){
-      //check if satisfied
-      if( rt.satisfiedBy( this, tnp ) ){
-        Trace("sygus-sb-simple") << "  sb-simple : do not consider const " << c << " as arg " << arg << " of " << pk;
-        Trace("sygus-sb-simple") << " in " << ((DatatypeType)tnp.toType()).getDatatype().getName() << std::endl;
-        //do not need to consider the constant in the search since there are ways to construct equivalent terms
-        ret = false;
-      }
-    }
-  }
-  // TODO : cache?
-  return ret;
-}
-
-int TermDbSygus::solveForArgument( TypeNode tn, unsigned cindex, unsigned arg ) {
-  // FIXME
-  return -1;  // TODO : if using, modify considerArgKind above
-  Assert( isRegistered( tn ) );
-  const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-  Assert( cindex<dt.getNumConstructors() );
-  Assert( arg<dt[cindex].getNumArgs() );
-  Kind nk = getConsNumKind( tn, cindex );
-  TypeNode tnc = getArgType( dt[cindex], arg );
-  const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
-
-  ReqTrie rt;
-  Assert( rt.empty() );
-  int solve_ret = -1;
-  if( nk==MINUS || nk==BITVECTOR_SUB ){
-    if( dt[cindex].getNumArgs()==2 && arg==0 ){
-      TypeNode tnco = getArgType( dt[cindex], 1 );
-      Node builtin = d_quantEngine->getTermUtil()->getTypeValue(
-          sygusToBuiltinType(tnc), 0);
-      solve_ret = getConstConsNum( tn, builtin );
-      if( solve_ret!=-1 ){
-        // t - s    ----->  ( 0 - s ) + t
-        rt.d_req_kind = nk == MINUS ? PLUS : BITVECTOR_PLUS;
-        rt.d_children[0].d_req_type = tn; // avoid?
-        rt.d_children[0].d_req_kind = nk;
-        rt.d_children[0].d_children[0].d_req_const = builtin;
-        rt.d_children[0].d_children[0].d_req_type = tnco;
-        rt.d_children[1].d_req_type = tnc;
-        // TODO : this can be made more general for multiple type grammars to remove MINUS entirely 
-      }
-    }
-  }
-  
-  if( !rt.empty() ){
-    Assert( solve_ret>=0 );
-    Assert( solve_ret<=(int)cdt.getNumConstructors() );
-    //check if satisfied
-    if( rt.satisfiedBy( this, tn ) ){
-      Trace("sygus-sb-simple") << "  sb-simple : ONLY consider " << cdt[solve_ret].getSygusOp() << " as arg " << arg << " of " << nk;
-      Trace("sygus-sb-simple") << " in " << ((DatatypeType)tn.toType()).getDatatype().getName() << std::endl;
-      return solve_ret;
-    }
-  }
-  
-  return -1;
-}
-
 void TermDbSygus::registerSygusType( TypeNode tn ) {
   std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
   if( itr==d_register.end() ){
@@ -1260,17 +849,6 @@ TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
       static_cast<SelectorType>(c[i].getType()).getRangeType());
 }
 
-/** get first occurrence */
-int TermDbSygus::getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ) {
-  for( unsigned i=0; i<c.getNumArgs(); i++ ){
-    TypeNode tni = getArgType( c, i );
-    if( tni==tn ){
-      return i;
-    }
-  }
-  return -1;
-}
-
 bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ) {
   if( c1.getNumArgs()!=c2.getNumArgs() ){
     return false;
@@ -1486,19 +1064,6 @@ Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) {
   }
 }
 
-Node TermDbSygus::getSemanticSkolem( TypeNode tn, Node n, bool doMk ){
-  std::map< Node, Node >::iterator its = d_semantic_skolem[tn].find( n );
-  if( its!=d_semantic_skolem[tn].end() ){
-    return its->second;
-  }else if( doMk ){
-    Node ss = NodeManager::currentNM()->mkSkolem( "sem", tn, "semantic skolem for sygus" );
-    d_semantic_skolem[tn][n] = ss;
-    return ss;
-  }else{
-    return Node::null();
-  }
-}
-
 bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 3631ee520..fee556cf8 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -378,8 +378,6 @@ class TermDbSygus {
   bool isConstArg( TypeNode tn, int i );
   /** get arg type */
   TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
-  /** get first occurrence */
-  int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
   /** is type match */
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
   /**
@@ -431,19 +429,11 @@ class TermDbSygus {
   /** get comparison kind */
   Kind getComparisonKind( TypeNode tn );
   Kind getPlusKind( TypeNode tn, bool is_neg = false );
-  // get semantic skolem for n (a sygus term whose builtin version is n)
-  Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true );
   /** involves div-by-zero */
   bool involvesDivByZero( Node n );
   /** get anchor */
   static Node getAnchor( Node n );
   static unsigned getAnchorDepth( Node n );
-  
-public: // for symmetry breaking
-  bool considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg );
-  bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
-  bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
-  int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
 
  public:
   /** unfold