Improve simple constant symmetry breaking for sygus (#1977)

4 files changed, 323 insertions, 270 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index f9a434453..328ef03d4 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -285,10 +285,11 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   if( min_depth<=max_depth ){
     TNode x = getFreeVar( ntn );
     std::vector<Node> sb_lemmas;
+    bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m);
     for (unsigned ds = 0; ds <= max_depth; ds++)
     {
       // static conjecture-independent symmetry breaking
-      Node ipred = getSimpleSymBreakPred(ntn, tindex, ds);
+      Node ipred = getSimpleSymBreakPred(ntn, tindex, ds, usingSymCons);
       if (!ipred.isNull())
       {
         sb_lemmas.push_back(ipred);
@@ -385,282 +386,314 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
   }
 }
 
-Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned depth ) {
-  std::map< unsigned, Node >::iterator it = d_simple_sb_pred[tn][tindex].find( depth );
-  if( it==d_simple_sb_pred[tn][tindex].end() ){
-    Node n = getFreeVar( tn );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( tindex>=0 && tindex<(int)dt.getNumConstructors() ); 
-    //conjunctive conclusion of lemma
-    std::vector< Node > sbp_conj;
-    
-    if( depth==0 ){
-      //fairness
-      if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-        Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n );
-        Node szr = NodeManager::currentNM()->mkNode( DT_SIZE, DatatypesRewriter::getInstCons( n, dt, tindex ) );
-        szr = Rewriter::rewrite( szr );
-        sbp_conj.push_back( szl.eqNode( szr ) );
-        //sbp_conj.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, szl, NodeManager::currentNM()->mkConst( Rational(0) ) ) );
+Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
+                                             int tindex,
+                                             unsigned depth,
+                                             bool usingSymCons)
+{
+  std::map<unsigned, Node>::iterator it =
+      d_simple_sb_pred[tn][tindex][usingSymCons].find(depth);
+  if (it != d_simple_sb_pred[tn][tindex][usingSymCons].end())
+  {
+    return it->second;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node n = getFreeVar(tn);
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors()));
+  // conjunctive conclusion of lemma
+  std::vector<Node> sbp_conj;
+
+  if (depth == 0)
+  {
+    // fairness
+    if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
+    {
+      Node szl = nm->mkNode(DT_SIZE, n);
+      Node szr =
+          nm->mkNode(DT_SIZE, DatatypesRewriter::getInstCons(n, dt, tindex));
+      szr = Rewriter::rewrite(szr);
+      sbp_conj.push_back(szl.eqNode(szr));
+    }
+  }
+
+  // symmetry breaking
+  Kind nk = d_tds->getConsNumKind(tn, tindex);
+  // only do simple symmetry breaking up to depth 2
+  if (options::sygusSymBreak() && depth < 2)
+  {
+    unsigned dt_index_nargs = dt[tindex].getNumArgs();
+    // builtin type
+    TypeNode tnb = TypeNode::fromType(dt.getSygusType());
+    // get children
+    std::vector<Node> children;
+    for (unsigned j = 0; j < dt_index_nargs; j++)
+    {
+      Node sel = nm->mkNode(
+          APPLY_SELECTOR_TOTAL,
+          Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
+          n);
+      Assert(sel.getType().isDatatype());
+      children.push_back(sel);
+    }
+
+    // direct solving for children
+    //   for instance, we may want to insist that the LHS of MINUS is 0
+    std::map<unsigned, unsigned> children_solved;
+    for (unsigned j = 0; j < dt_index_nargs; j++)
+    {
+      int i = d_tds->solveForArgument(tn, tindex, j);
+      if (i >= 0)
+      {
+        children_solved[j] = i;
+        TypeNode ctn = children[j].getType();
+        const Datatype& cdt =
+            static_cast<DatatypeType>(ctn.toType()).getDatatype();
+        Assert(i < static_cast<int>(cdt.getNumConstructors()));
+        sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
       }
     }
-    
-    //symmetry breaking
-    Kind nk = d_tds->getConsNumKind( tn, tindex );
-    if( options::sygusSymBreak() ){
-      NodeManager* nm = NodeManager::currentNM();
-      // if less than the maximum depth we consider
-      if( depth<2 ){
-        //get children
-        std::vector< Node > children;
-        for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-          Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), j ) ), n );
-          Assert( sel.getType().isDatatype() );
-          Assert( ((DatatypeType)sel.getType().toType()).getDatatype().isSygus() );
-          children.push_back( sel );
-          d_tds->registerSygusType( sel.getType() );
-        }
-        //builtin type
-        TypeNode tnb = TypeNode::fromType( dt.getSygusType() );
-        
-        // direct solving for children
-        //   for instance, we may want to insist that the LHS of MINUS is 0
-        std::map< unsigned, unsigned > children_solved;
-        for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-          int i = d_tds->solveForArgument( tn, tindex, j );
-          if( i>=0 ){
-            children_solved[j] = i;
-            TypeNode ctn = children[j].getType();
-            const Datatype& cdt = ((DatatypeType)(ctn).toType()).getDatatype();
-            Assert( i<(int)cdt.getNumConstructors() );
-            sbp_conj.push_back( DatatypesRewriter::mkTester( children[j], i, cdt ) );
+    // depth 1 symmetry breaking : talks about direct children
+    if (depth == 1)
+    {
+      if (nk != UNDEFINED_KIND)
+      {
+        // commutative operators
+        if (quantifiers::TermUtil::isComm(nk))
+        {
+          if (children.size() == 2
+              && children[0].getType() == children[1].getType())
+          {
+            Node order_pred = getTermOrderPredicate(children[0], children[1]);
+            sbp_conj.push_back(order_pred);
           }
         }
-        
-        // depth 1 symmetry breaking : talks about direct children
-        if( depth==1 ){
-          if( nk!=UNDEFINED_KIND ){
-            // commutative operators 
-            if( quantifiers::TermUtil::isComm( nk ) ){
-              if( children.size()==2 ){
-                if( children[0].getType()==children[1].getType() ){
-                  Node order_pred = getTermOrderPredicate( children[0], children[1] );
-                  sbp_conj.push_back( order_pred );
-                }
-              }
-            }
-            // operators whose arguments are non-additive (e.g. should be different)
-            std::vector< unsigned > deq_child[2];
-            if( children.size()==2 && children[0].getType()==tn ){
-              bool argDeq = false;
-              if( quantifiers::TermUtil::isNonAdditive( nk ) ){
-                argDeq = true;
-              }else{
-                //other cases of rewriting x k x -> x'
-                Node req_const;
-                if( nk==GT || nk==LT || nk==XOR || nk==MINUS || nk==BITVECTOR_SUB || nk==BITVECTOR_XOR || nk==BITVECTOR_UREM_TOTAL ){
-                  //must have the zero element
-                  req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0);
-                }else if( nk==EQUAL || nk==LEQ || nk==GEQ || nk==BITVECTOR_XNOR ){
-                  req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb);
-                }
-                // cannot do division since we have to consider when both are zero
-                if( !req_const.isNull() ){
-                  if( d_tds->hasConst( tn, req_const ) ){
-                    argDeq = true;
-                  }
-                }
-              }
-              if( argDeq ){
-                deq_child[0].push_back( 0 );deq_child[1].push_back( 1 );
-              }
-            }
-            if( nk==ITE || nk==STRING_STRREPL ){
-              deq_child[0].push_back( 1 );deq_child[1].push_back( 2 );
+        // operators whose arguments are non-additive (e.g. should be different)
+        std::vector<unsigned> deq_child[2];
+        if (children.size() == 2 && children[0].getType() == tn)
+        {
+          bool argDeq = false;
+          if (quantifiers::TermUtil::isNonAdditive(nk))
+          {
+            argDeq = true;
+          }
+          else
+          {
+            // other cases of rewriting x k x -> x'
+            Node req_const;
+            if (nk == GT || nk == LT || nk == XOR || nk == MINUS
+                || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR
+                || nk == BITVECTOR_UREM_TOTAL)
+            {
+              // must have the zero element
+              req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0);
             }
-            if( nk==STRING_STRREPL ){
-              deq_child[0].push_back( 0 );deq_child[1].push_back( 1 );
+            else if (nk == EQUAL || nk == LEQ || nk == GEQ
+                     || nk == BITVECTOR_XNOR)
+            {
+              req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb);
             }
-            // this code adds simple symmetry breaking predicates of the form
-            // d.i != d.j, for example if we are considering an ITE constructor,
-            // we enforce that d.1 != d.2 since otherwise the ITE can be
-            // simplified.
-            for( unsigned i=0; i<deq_child[0].size(); i++ ){
-              unsigned c1 = deq_child[0][i];
-              unsigned c2 = deq_child[1][i];
-              TypeNode tnc = children[c1].getType();
-              if (tnc == children[c2].getType()
-                  && !tnc.getCardinality().isOne())
+            // cannot do division since we have to consider when both are zero
+            if (!req_const.isNull())
+            {
+              if (d_tds->hasConst(tn, req_const))
               {
-                Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
-                // must guard if there are symbolic constructors
-                // the issue is that ite( C, _any_constant, _any_constant ) is
-                // a useful solution, since the two instances of _any_constant
-                // can be repaired to different values. Hence, below, we say
-                // e.g. d.i is a symbolic constructor, or it must be different
-                // from d.j.
-                int anyc_cons_num_c = d_tds->getAnyConstantConsNum(tnc);
-                if (anyc_cons_num_c != -1)
-                {
-                  const Datatype& cdt =
-                      static_cast<DatatypeType>(tnc.toType()).getDatatype();
-                  Node guard_val = nm->mkNode(
-                      APPLY_CONSTRUCTOR,
-                      Node::fromExpr(cdt[anyc_cons_num_c].getConstructor()));
-                  Node exp = d_tds->getExplain()->getExplanationForEquality(
-                      children[c1], guard_val);
-                  sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq);
-                }
-                sbp_conj.push_back(sym_lem_deq);
-              }
-            }
-            
-            /*
-            // division by zero  TODO ?
-            if( nk==DIVISION || nk==DIVISION_TOTAL || nk==INTS_DIVISION || nk==INTS_DIVISION_TOTAL || 
-                nk==INTS_MODULUS || nk==INTS_MODULUS_TOTAL ){
-              Assert( children.size()==2 );
-              // do not consider non-constant denominators ?
-              sbp_conj.push_back( NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, children[1] ) );
-              // do not consider zero denominator
-              Node tzero = d_tds->getTypeValue( tnb, 0 );
-              int zero_arg = d_tds->getConstConsNum( children[1].getType(), tzero );
-              if( zero_arg!=-1 ){
-                
-              }else{
-                // semantic skolem for zero?
-              }
-            }else if( nk==BITVECTOR_UDIV_TOTAL || nk==BITVECTOR_UDIV || nk==BITVECTOR_SDIV || nk==BITVECTOR_UREM || nk==BITVECTOR_UREM_TOTAL ){
-
-            }
-            */
-            
-            Trace("sygus-sb-simple-debug") << "Process arguments for " << tn << " : " << nk << " : " << std::endl;
-            // singular arguments (e.g. 0 for mult) 
-            // redundant arguments (e.g. 0 for plus, 1 for mult)
-            // right-associativity
-            // simple rewrites
-            for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-              Node nc = children[j];
-              // if not already solved
-              if( children_solved.find( j )==children_solved.end() ){
-                TypeNode tnc = nc.getType();
-                int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc);
-                const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
-                for( unsigned k=0; k<cdt.getNumConstructors(); k++ ){
-                  Kind nck = d_tds->getConsNumKind(tnc, k);
-                  bool red = false;
-                  // check if the argument is redundant
-                  if (static_cast<int>(k) == anyc_cons_num)
-                  {
-                    // check if the any constant constructor is redundant at
-                    // this argument position
-                    // TODO
-                  }
-                  else 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{
-                      // defined function?
-                    }
-                  }
-                  if (red)
-                  {
-                    Trace("sygus-sb-simple-debug")
-                        << "  ...redundant." << std::endl;
-                    sbp_conj.push_back(
-                        DatatypesRewriter::mkTester(nc, k, cdt).negate());
-                  }
-                }
+                argDeq = true;
               }
             }
-          }else{
-            // defined function?
           }
-          // explicitly handle "any constant" constructors
-          // if this type admits any constant, then at least one of my children
-          // must not be the "any constant" constructor
-          unsigned dt_index_nargs = dt[tindex].getNumArgs();
-          if (dt.getSygusAllowConst() && dt_index_nargs > 0)
+          if (argDeq)
           {
-            std::vector<Node> exp_all_anyc;
-            bool success = true;
-            for (unsigned j = 0; j < dt_index_nargs; j++)
+            deq_child[0].push_back(0);
+            deq_child[1].push_back(1);
+          }
+        }
+        if (nk == ITE || nk == STRING_STRREPL)
+        {
+          deq_child[0].push_back(1);
+          deq_child[1].push_back(2);
+        }
+        if (nk == STRING_STRREPL)
+        {
+          deq_child[0].push_back(0);
+          deq_child[1].push_back(1);
+        }
+        // this code adds simple symmetry breaking predicates of the form
+        // d.i != d.j, for example if we are considering an ITE constructor,
+        // we enforce that d.1 != d.2 since otherwise the ITE can be
+        // simplified.
+        for (unsigned i = 0, size = deq_child[0].size(); i < size; i++)
+        {
+          unsigned c1 = deq_child[0][i];
+          unsigned c2 = deq_child[1][i];
+          TypeNode tnc = children[c1].getType();
+          if (tnc == children[c2].getType() && !tnc.getCardinality().isOne())
+          {
+            Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
+            // must guard if there are symbolic constructors
+            // the issue is that ite( C, _any_constant, _any_constant ) is
+            // a useful solution, since the two instances of _any_constant
+            // can be repaired to different values. Hence, below, we say
+            // e.g. d.i is a symbolic constructor, or it must be different
+            // from d.j.
+            int anyc_cons_num_c = d_tds->getAnyConstantConsNum(tnc);
+            if (anyc_cons_num_c != -1)
             {
-              TypeNode ctn = TypeNode::fromType(dt[tindex].getArgType(j));
-              int ctn_ac = d_tds->getAnyConstantConsNum(ctn);
-              if (ctn_ac == -1)
-              {
-                success = false;
-                break;
-              }
-              Node nc = children[j];
-              TypeNode tnc = nc.getType();
               const Datatype& cdt =
                   static_cast<DatatypeType>(tnc.toType()).getDatatype();
-              exp_all_anyc.push_back(
-                  DatatypesRewriter::mkTester(nc, ctn_ac, cdt));
-            }
-            if (success)
-            {
-              Node expaan = exp_all_anyc.size() == 1
-                                ? exp_all_anyc[0]
-                                : nm->mkNode(AND, exp_all_anyc);
-              expaan = expaan.negate();
-              Trace("sygus-sb-simple-debug")
-                  << "Ensure not all any constant: " << expaan << std::endl;
-              sbp_conj.push_back(expaan);
+              Node guard_val = nm->mkNode(
+                  APPLY_CONSTRUCTOR,
+                  Node::fromExpr(cdt[anyc_cons_num_c].getConstructor()));
+              Node exp = d_tds->getExplain()->getExplanationForEquality(
+                  children[c1], guard_val);
+              sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq);
             }
+            sbp_conj.push_back(sym_lem_deq);
           }
-        }else if( depth==2 ){
-          if( nk!=UNDEFINED_KIND ){
-            // commutative operators 
-            if( quantifiers::TermUtil::isComm( nk ) ){
-              if( children.size()==2 ){
-                if( children[0].getType()==children[1].getType() ){
-                  //chainable
-                  // TODO : this is depth 2
-                  if( children[0].getType()==tn ){
-                    Node child11 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), 1 ) ), children[0] );
-                    Assert( child11.getType()==children[1].getType() );
-                    Node order_pred_trans = NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( children[0], tindex, dt ).negate(),
-                                                                              getTermOrderPredicate( child11, children[1] ) );
+        }
 
-                    sbp_conj.push_back( order_pred_trans );
-                  }
+        Trace("sygus-sb-simple-debug") << "Process arguments for " << tn
+                                       << " : " << nk << " : " << std::endl;
+        // singular arguments (e.g. 0 for mult)
+        // redundant arguments (e.g. 0 for plus, 1 for mult)
+        // right-associativity
+        // simple rewrites
+        // explanation of why not all children of this are constant
+        std::vector<Node> exp_not_all_const;
+        // is the above explanation valid? This is set to false if
+        // one child does not have a constant, hence making the explanation
+        // false.
+        bool exp_not_all_const_valid = dt_index_nargs > 0;
+        // does the parent have an any constant constructor?
+        bool usingAnyConstCons =
+            usingSymCons && (d_tds->getAnyConstantConsNum(tn) != -1);
+        for (unsigned j = 0; j < dt_index_nargs; j++)
+        {
+          Node nc = children[j];
+          // if not already solved
+          if (children_solved.find(j) != children_solved.end())
+          {
+            continue;
+          }
+          TypeNode tnc = nc.getType();
+          int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc);
+          const Datatype& cdt =
+              static_cast<DatatypeType>(tnc.toType()).getDatatype();
+          std::vector<Node> exp_const;
+          for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++)
+          {
+            Kind nck = d_tds->getConsNumKind(tnc, k);
+            bool red = false;
+            Node tester = DatatypesRewriter::mkTester(nc, k, cdt);
+            // check if the argument is redundant
+            if (static_cast<int>(k) == anyc_cons_num)
+            {
+              exp_const.push_back(tester);
+            }
+            else 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);
+                if (usingAnyConstCons)
+                {
+                  // we only consider concrete constant constructors
+                  // of children if we have the "any constant" constructor
+                  // otherwise, we would disallow solutions for grammars
+                  // like the following:
+                  //   A -> B+B
+                  //   B -> 4 | 8 | 100
+                  // where A allows all constants but is not using the
+                  // any constant constructor.
+                  exp_const.push_back(tester);
                 }
               }
+              else
+              {
+                // defined function?
+              }
+            }
+            if (red)
+            {
+              Trace("sygus-sb-simple-debug") << "  ...redundant." << std::endl;
+              sbp_conj.push_back(tester.negate());
             }
           }
+          if (exp_const.empty())
+          {
+            exp_not_all_const_valid = false;
+          }
+          else
+          {
+            Node ecn = exp_const.size() == 1 ? exp_const[0]
+                                             : nm->mkNode(OR, exp_const);
+            exp_not_all_const.push_back(ecn.negate());
+          }
         }
+        // explicitly handle constants and "any constant" constructors
+        // if this type admits any constant, then at least one of my
+        // children must not be a constant or the "any constant" constructor
+        if (dt.getSygusAllowConst() && exp_not_all_const_valid)
+        {
+          Assert(!exp_not_all_const.empty());
+          Node expaan = exp_not_all_const.size() == 1
+                            ? exp_not_all_const[0]
+                            : nm->mkNode(OR, exp_not_all_const);
+          Trace("sygus-sb-simple-debug")
+              << "Ensure not all constant: " << expaan << std::endl;
+          sbp_conj.push_back(expaan);
+        }
+      }
+      else
+      {
+        // defined function?
       }
     }
-    
-    Node sb_pred;
-    if( !sbp_conj.empty() ){
-      sb_pred = sbp_conj.size()==1 ? sbp_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, sbp_conj );
-      Trace("sygus-sb-simple") << "Simple predicate for " << tn << " index " << tindex << " (" << nk << ") at depth " << depth << " : " << std::endl;
-      Trace("sygus-sb-simple") << "   " << sb_pred << std::endl;
-      sb_pred = NodeManager::currentNM()->mkNode( kind::OR, DatatypesRewriter::mkTester( n, tindex, dt ).negate(), sb_pred );
+    else if (depth == 2)
+    {
+      // commutative operators
+      if (quantifiers::TermUtil::isComm(nk) && children.size() == 2
+          && children[0].getType() == tn && children[1].getType() == tn)
+      {
+        // chainable
+        Node child11 = nm->mkNode(
+            APPLY_SELECTOR_TOTAL,
+            Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), 1)),
+            children[0]);
+        Assert(child11.getType() == children[1].getType());
+        Node order_pred_trans = nm->mkNode(
+            OR,
+            DatatypesRewriter::mkTester(children[0], tindex, dt).negate(),
+            getTermOrderPredicate(child11, children[1]));
+        sbp_conj.push_back(order_pred_trans);
+      }
     }
-    d_simple_sb_pred[tn][tindex][depth] = sb_pred;
-    return sb_pred;
-  }else{
-    return it->second;
   }
+
+  Node sb_pred;
+  if (!sbp_conj.empty())
+  {
+    sb_pred =
+        sbp_conj.size() == 1 ? sbp_conj[0] : nm->mkNode(kind::AND, sbp_conj);
+    Trace("sygus-sb-simple")
+        << "Simple predicate for " << tn << " index " << tindex << " (" << nk
+        << ") at depth " << depth << " : " << std::endl;
+    Trace("sygus-sb-simple") << "   " << sb_pred << std::endl;
+    sb_pred = nm->mkNode(
+        kind::OR, DatatypesRewriter::mkTester(n, tindex, dt).negate(), sb_pred);
+  }
+  d_simple_sb_pred[tn][tindex][usingSymCons][depth] = sb_pred;
+  return sb_pred;
 }
 
 TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index e0b29efd2..eaed2a866 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -388,10 +388,17 @@ private:
    *   is-C( t ) => F[t]
    * where t is a search term, see registerSearchTerm for definition of search
    * term.
+   *
+   * usingSymCons is whether we are using symbolic constructors for subterms in
+   * the type tn. This may affect the form of the predicate we construct.
    */
-  Node getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned depth );
+  Node getSimpleSymBreakPred(TypeNode tn,
+                             int tindex,
+                             unsigned depth,
+                             bool usingSymCons);
   /** Cache of the above function */
-  std::map<TypeNode, std::map<int, std::map<unsigned, Node>>> d_simple_sb_pred;
+  std::map<TypeNode, std::map<int, std::map<bool, std::map<unsigned, Node>>>>
+      d_simple_sb_pred;
   /**
    * For each search term, this stores the maximum depth for which we have added
    * a static symmetry breaking lemma.
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 121ee34f7..cd6c8bdec 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -881,37 +881,43 @@ bool TermDbSygus::isEnumerator(Node e) const
   return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
 }
 
-CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e)
+CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
 {
-  std::map<Node, CegConjecture*>::iterator itm = d_enum_to_conjecture.find(e);
+  std::map<Node, CegConjecture*>::const_iterator itm =
+      d_enum_to_conjecture.find(e);
   if (itm != d_enum_to_conjecture.end()) {
     return itm->second;
-  }else{
-    return NULL;
   }
+  return nullptr;
 }
 
-Node TermDbSygus::getSynthFunForEnumerator(Node e)
+Node TermDbSygus::getSynthFunForEnumerator(Node e) const
 {
-  std::map<Node, Node>::iterator itsf = d_enum_to_synth_fun.find(e);
+  std::map<Node, Node>::const_iterator itsf = d_enum_to_synth_fun.find(e);
   if (itsf != d_enum_to_synth_fun.end())
   {
     return itsf->second;
   }
-  else
-  {
-    return Node::null();
-  }
+  return Node::null();
 }
 
-Node TermDbSygus::getActiveGuardForEnumerator(Node e)
+Node TermDbSygus::getActiveGuardForEnumerator(Node e) const
 {
-  std::map<Node, Node>::iterator itag = d_enum_to_active_guard.find(e);
+  std::map<Node, Node>::const_iterator itag = d_enum_to_active_guard.find(e);
   if (itag != d_enum_to_active_guard.end()) {
     return itag->second;
-  }else{
-    return Node::null();
   }
+  return Node::null();
+}
+
+bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
+{
+  std::map<Node, bool>::const_iterator itus = d_enum_to_using_sym_cons.find(e);
+  if (itus != d_enum_to_using_sym_cons.end())
+  {
+    return itus->second;
+  }
+  return false;
 }
 
 void TermDbSygus::getEnumerators(std::vector<Node>& mts)
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 139e00794..163d65d19 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -79,11 +79,13 @@ class TermDbSygus {
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
-  CegConjecture* getConjectureForEnumerator(Node e);
+  CegConjecture* getConjectureForEnumerator(Node e) const;
   /** return the function-to-synthesize e is associated with */
-  Node getSynthFunForEnumerator(Node e);
+  Node getSynthFunForEnumerator(Node e) const;
   /** get active guard for e */
-  Node getActiveGuardForEnumerator(Node e);
+  Node getActiveGuardForEnumerator(Node e) const;
+  /** are we using symbolic constructors for enumerator e? */
+  bool usingSymbolicConsForEnumerator(Node e) const;
   /** get all registered enumerators */
   void getEnumerators(std::vector<Node>& mts);
   /** Register symmetry breaking lemma
@@ -242,6 +244,11 @@ class TermDbSygus {
    *   if G is true, then there are more values of e to enumerate".
    */
   std::map<Node, Node> d_enum_to_active_guard;
+  /**
+   * Mapping from enumerators to whether we allow symbolic constructors to
+   * appear as subterms of them.
+   */
+  std::map<Node, bool> d_enum_to_using_sym_cons;
   /** mapping from enumerators to symmetry breaking clauses for them */
   std::map<Node, std::vector<Node> > d_enum_to_sb_lemmas;
   /** mapping from symmetry breaking lemmas to type */