From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 May 2018 01:27:32 +0000 (-0500)
Subject: Repair constants using symbolic constructors (#1960)
X-Git-Tag: cvc5-1.0.0~5022
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ac3d0bf2c00edbbd04033815f10ba0207010f77;p=cvc5.git

Repair constants using symbolic constructors (#1960)
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 107f3896f..4a7004821 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -989,7 +989,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-repair-const"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "use approach to repair constants in sygus candidate solutions"
 
 [[option]]
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 15c071431..d4a21ea2f 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -408,6 +408,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
     //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
@@ -480,13 +481,37 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
             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; i<deq_child[0].size(); i++ ){
               unsigned c1 = deq_child[0][i];
               unsigned c2 = deq_child[1][i];
-              if( children[c1].getType()==children[c2].getType() ){
-                if( !children[c1].getType().getCardinality().isOne() ){
-                  sbp_conj.push_back( children[c1].eqNode( children[c2] ).negate() );
+              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)
+                {
+                  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);
               }
             }
             
@@ -520,12 +545,19 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
               // 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 (nck != UNDEFINED_KIND)
+                  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
@@ -558,6 +590,42 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
           }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();
+          int tn_ac = d_tds->getAnyConstantConsNum(tn);
+          if (tn_ac != -1 && dt_index_nargs > 0)
+          {
+            std::vector<Node> exp_all_anyc;
+            bool success = true;
+            for (unsigned j = 0; j < dt_index_nargs; j++)
+            {
+              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);
+            }
+          }
         }else if( depth==2 ){
           if( nk!=UNDEFINED_KIND ){
             // commutative operators 
@@ -845,12 +913,17 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, st
 void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) {
   Assert( t.getType()==tn );
   Assert( !a.isNull() );
+  Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
+                           << " " << a << std::endl;
   std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn );
   if( its != d_cache[a].d_sb_lemmas.end() ){
     TNode x = getFreeVar( tn );
     //get symmetry breaking lemmas for this term 
     unsigned csz = getSearchSizeForAnchor( a );
     int max_sz = ((int)csz) - ((int)d);
+    Trace("sygus-sb-debug2")
+        << "add lemmas up to size " << max_sz << ", which is (search_size) "
+        << csz << " - (depth) " << d << std::endl;
     for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){
       if( (int)it->first<=max_sz ){
         for( unsigned k=0; k<it->second.size(); k++ ){
@@ -860,6 +933,7 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
       }
     }
   }
+  Trace("sygus-sb-debug2") << "...finished." << std::endl;
 }
 
 void SygusSymBreakNew::addSymBreakLemma(Node lem,
@@ -1047,16 +1121,22 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   {
     for (const Node& a : anchors)
     {
-      std::vector<Node> sbl;
-      d_tds->getSymBreakLemmas(a, sbl);
-      for (const Node& lem : sbl)
+      // is this a registered enumerator?
+      if (d_register_st.find(a) != d_register_st.end())
       {
-        TypeNode tn = d_tds->getTypeForSymBreakLemma(lem);
-        unsigned sz = d_tds->getSizeForSymBreakLemma(lem);
-        registerSymBreakLemma(tn, lem, sz, a, lemmas);
+        // symmetry breaking lemmas should only be for enumerators
+        Assert(d_register_st[a]);
+        std::vector<Node> sbl;
+        d_tds->getSymBreakLemmas(a, sbl);
+        for (const Node& lem : sbl)
+        {
+          TypeNode tn = d_tds->getTypeForSymBreakLemma(lem);
+          unsigned sz = d_tds->getSizeForSymBreakLemma(lem);
+          registerSymBreakLemma(tn, lem, sz, a, lemmas);
+        }
+        d_tds->clearSymBreakLemmas(a);
       }
     }
-    d_tds->clearSymBreakLemmas();
     if (!lemmas.empty())
     {
       return;
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index b1da66d18..e7deb6a1a 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -23,11 +23,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-namespace arith {
-  class TheoryArith;
-}
-
 namespace quantifiers {
 
 class CegqiOutput {
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 6f5709fc2..f66a97ce8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -258,28 +258,6 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> candidate_values;
   bool constructed_cand = false;
 
-  if (options::sygusRepairConst())
-  {
-    // have we tried to repair the previous solution?
-    // if not, call the repair constant utility
-    unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
-    if (d_repair_index < ninst)
-    {
-      std::vector<Node> fail_cvs;
-      for (const Node& cprog : d_candidates)
-      {
-        Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
-        fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
-      }
-      d_repair_index++;
-      if (d_sygus_rconst->repairSolution(
-              d_candidates, fail_cvs, candidate_values))
-      {
-        constructed_cand = true;
-      }
-    }
-  }
-
   // get the model value of the relevant terms from the master module
   std::vector<Node> enum_values;
   getModelValues(terms, enum_values);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index fc41c7561..92ed41f3d 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -29,7 +29,7 @@ namespace theory {
 namespace quantifiers {
 
 Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
-    : SygusModule(qe, p), d_eval_unfold(nullptr)
+    : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
 {
   if (options::sygusEvalUnfold())
   {
@@ -66,10 +66,27 @@ bool Cegis::processInitialize(Node n,
                               const std::vector<Node>& candidates,
                               std::vector<Node>& lemmas)
 {
+  Trace("cegis") << "Initialize cegis..." << std::endl;
   // initialize an enumerator for each candidate
   for (unsigned i = 0; i < candidates.size(); i++)
   {
-    d_tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+    Trace("cegis") << "...register enumerator " << candidates[i];
+    bool do_repair_const = false;
+    if (options::sygusRepairConst())
+    {
+      TypeNode ctn = candidates[i].getType();
+      d_tds->registerSygusType(ctn);
+      if (d_tds->hasSubtermSymbolicCons(ctn))
+      {
+        do_repair_const = true;
+        // remember that we are doing grammar-based repair
+        d_using_gr_repair = true;
+        Trace("cegis") << " (using repair)";
+      }
+    }
+    Trace("cegis") << std::endl;
+    d_tds->registerEnumerator(
+        candidates[i], candidates[i], d_parent, false, do_repair_const);
   }
   return true;
 }
@@ -156,6 +173,46 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
       Trace("cegis") << ss.str() << std::endl;
     }
   }
+  // if we are using grammar-based repair
+  if (d_using_gr_repair)
+  {
+    SygusRepairConst* src = d_parent->getRepairConst();
+    Assert(src != nullptr);
+    // check if any enum_values have symbolic terms that must be repaired
+    bool mustRepair = false;
+    for (const Node& c : enum_values)
+    {
+      if (SygusRepairConst::mustRepair(c))
+      {
+        mustRepair = true;
+        break;
+      }
+    }
+    Trace("cegis") << "...must repair is: " << mustRepair << std::endl;
+    // if the solution contains a subterm that must be repaired
+    if (mustRepair)
+    {
+      std::vector<Node> fail_cvs = enum_values;
+      Assert(candidates.size() == fail_cvs.size());
+      if (src->repairSolution(candidates, fail_cvs, candidate_values))
+      {
+        return true;
+      }
+      // repair solution didn't work, exclude this solution
+      std::vector<Node> exp;
+      for (unsigned i = 0, size = enums.size(); i < size; i++)
+      {
+        d_tds->getExplain()->getExplanationForEquality(
+            enums[i], enum_values[i], exp);
+      }
+      Assert(!exp.empty());
+      Node expn =
+          exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp);
+      lems.push_back(expn.negate());
+      return false;
+    }
+  }
+
   // evaluate on refinement lemmas
   bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
 
@@ -197,14 +254,6 @@ bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
         candidate_values.end(), enum_values.begin(), enum_values.end());
     return true;
   }
-  SygusRepairConst* src = d_parent->getRepairConst();
-  if (src != nullptr)
-  {
-    // it may be repairable
-    std::vector<Node> fail_cvs = enum_values;
-    Assert(candidates.size() == fail_cvs.size());
-    return src->repairSolution(candidates, fail_cvs, candidate_values);
-  }
   return false;
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 70f3ce8b6..ca27a2281 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -79,7 +79,7 @@ class Cegis : public SygusModule
   virtual bool processInitialize(Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& lemmas);
-  /** do cegis-implementation-specific construct candidate
+  /** do cegis-implementation-specific post-processing for construct candidate
    *
    * satisfiedRl is whether all refinement lemmas are satisfied under the
    * substitution { enums -> enum_values }.
@@ -164,6 +164,16 @@ class Cegis : public SygusModule
    * added as refinement lemmas.
    */
   std::unordered_set<unsigned> d_cegis_sample_refine;
+
+  //---------------------------------for sygus repair
+  /** are we using grammar-based repair?
+   *
+   * This flag is set ot true if at least one of the enumerators allocated
+   * by this class has been configured to allow model values with symbolic
+   * constructors, such as the "any constant" constructor.
+   */
+  bool d_using_gr_repair;
+  //---------------------------------end for sygus repair
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 73311b0bd..a468e1383 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -20,6 +20,7 @@
 #include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -104,6 +105,33 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
                 sygus_norm->d_sygus_vars.toExpr(),
                 dt.getSygusAllowConst(),
                 dt.getSygusAllowAll());
+  if (dt.getSygusAllowConst())
+  {
+    TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
+    // must be handled by counterexample-guided instantiation
+    // don't do it for Boolean (not worth the trouble, since it has only
+    // minimal gain (1 any constant vs 2 constructors for true/false), and
+    // we need to do a lot of special symmetry breaking, e.g. for ensuring
+    // any constant constructors are not the 1st children of ITEs.
+    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
+        && !sygus_type.isBoolean())
+    {
+      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
+      // add an "any constant" proxy variable
+      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
+      // mark that it represents any constant
+      SygusAnyConstAttribute saca;
+      av.setAttribute(saca, true);
+      std::stringstream ss;
+      ss << d_unres_tn << "_any_constant";
+      std::string cname(ss.str());
+      std::vector<Type> empty_arg_types;
+      // we add this constructor first since we use left associative chains
+      // and our symmetry breaking should group any constants together
+      // beneath the same application
+      d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types);
+    }
+  }
   for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
   {
     d_dt.addSygusConstructor(d_ops[i].toExpr(),
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index f72a83e5a..47cc19377 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -36,6 +36,12 @@ namespace quantifiers {
 
 class SygusGrammarNorm;
 
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
 /** Operator position trie class
  *
  * This data structure stores an unresolved type corresponding to the
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index f9208599f..77930fb42 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -20,6 +20,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4::kind;
@@ -83,7 +84,8 @@ void SygusRepairConst::registerSygusType(TypeNode tn,
 
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
-                                      std::vector<Node>& repair_cv)
+                                      std::vector<Node>& repair_cv,
+                                      bool useConstantsAsHoles)
 {
   Assert(candidates.size() == candidate_values.size());
 
@@ -106,7 +108,6 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
     Trace("sygus-repair-const")
         << "Getting candidate skeletons : " << std::endl;
   }
-  NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> candidate_skeletons;
   std::map<TypeNode, int> free_var_count;
   std::vector<Node> sk_vars;
@@ -114,7 +115,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   for (unsigned i = 0, size = candidates.size(); i < size; i++)
   {
     Node cv = candidate_values[i];
-    Node skeleton = getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs);
+    Node skeleton =
+        getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
     if (Trace.isOn("sygus-repair-const"))
     {
       Printer* p = Printer::getPrinter(options::outputLanguage());
@@ -143,6 +145,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
     return false;
   }
 
+  NodeManager* nm = NodeManager::currentNM();
   Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
   Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars);
 
@@ -215,6 +218,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
     std::vector<Node> sk_sygus_m;
     for (const Node& v : sk_vars)
     {
+      Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
       Node fov = d_sk_to_fo[v];
       Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr()));
       Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
@@ -251,7 +255,35 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   return false;
 }
 
-bool SygusRepairConst::isRepairableConstant(Node n)
+bool SygusRepairConst::mustRepair(Node n)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
+      if (isRepairable(cur, false))
+      {
+        return true;
+      }
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+
+  return false;
+}
+
+bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
 {
   if (n.getKind() != APPLY_CONSTRUCTOR)
   {
@@ -261,17 +293,24 @@ bool SygusRepairConst::isRepairableConstant(Node n)
   Assert(tn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   Assert(dt.isSygus());
-  if (dt.getSygusAllowConst())
+  Node op = n.getOperator();
+  unsigned cindex = Datatype::indexOf(op.toExpr());
+  if (dt[cindex].getNumArgs() > 0)
   {
-    Node op = n.getOperator();
-    unsigned cindex = Datatype::indexOf(op.toExpr());
-    if (dt[cindex].getNumArgs() == 0)
+    return false;
+  }
+  Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+  if (sygusOp.getAttribute(SygusAnyConstAttribute()))
+  {
+    // if it represents "any constant" then it is repairable
+    return true;
+  }
+  if (useConstantsAsHoles && dt.getSygusAllowConst())
+  {
+    if (sygusOp.isConst())
     {
-      Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
-      if (sygusOp.isConst())
-      {
-        return true;
-      }
+      // if a constant, it is repairable
+      return true;
     }
   }
   return false;
@@ -280,9 +319,10 @@ bool SygusRepairConst::isRepairableConstant(Node n)
 Node SygusRepairConst::getSkeleton(Node n,
                                    std::map<TypeNode, int>& free_var_count,
                                    std::vector<Node>& sk_vars,
-                                   std::map<Node, Node>& sk_vars_to_subs)
+                                   std::map<Node, Node>& sk_vars_to_subs,
+                                   bool useConstantsAsHoles)
 {
-  if (isRepairableConstant(n))
+  if (isRepairable(n, useConstantsAsHoles))
   {
     Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
     sk_vars.push_back(sk_var);
@@ -325,8 +365,8 @@ Node SygusRepairConst::getSkeleton(Node n,
       for (const Node& cn : cur)
       {
         Node child;
-        // if it is a constant over a type that allows all constants
-        if (isRepairableConstant(cn))
+        // if it is repairable
+        if (isRepairable(cn, useConstantsAsHoles))
         {
           // replace it by the next free variable
           child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
@@ -375,6 +415,19 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
   Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
 
   Trace("sygus-repair-const") << "  Introduce first-order vars..." << std::endl;
+  for (const Node& v : sk_vars)
+  {
+    std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
+    if (itf == d_sk_to_fo.end())
+    {
+      TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
+      Node sk_fov = nm->mkSkolem("k", builtinType);
+      d_sk_to_fo[v] = sk_fov;
+      d_fo_to_sk[sk_fov] = v;
+      Trace("sygus-repair-const-debug")
+          << "Map " << v << " -> " << sk_fov << std::endl;
+    }
+  }
   // now, we must replace all terms of the form eval( z_i, t1...tn ) with
   // a fresh first-order variable w_i, where z_i is a variable introduced in
   // the skeleton inference step (z_i is a variable in sk_vars).
@@ -398,19 +451,8 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
         if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
         {
           std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
-          if (itf == d_sk_to_fo.end())
-          {
-            Node sk_fov = nm->mkSkolem("k", cur.getType());
-            d_sk_to_fo[v] = sk_fov;
-            d_fo_to_sk[sk_fov] = v;
-            visited[cur] = sk_fov;
-            Trace("sygus-repair-const-debug")
-                << "Map " << v << " -> " << sk_fov << std::endl;
-          }
-          else
-          {
-            visited[cur] = itf->second;
-          }
+          Assert(itf != d_sk_to_fo.end());
+          visited[cur] = itf->second;
         }
       }
       if (visited[cur].isNull())
@@ -515,15 +557,20 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
     if (it == visited.end())
     {
       visited.insert(cur);
-      if (restrictLA && cur.getKind() == NONLINEAR_MULT)
+      Kind ck = cur.getKind();
+      if (restrictLA && (ck == NONLINEAR_MULT || ck == DIVISION))
       {
-        for (const Node& ccur : cur)
+        for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
         {
+          Node ccur = cur[j];
           std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
           if (itf != d_fo_to_sk.end())
           {
-            exvar = itf->second;
-            return true;
+            if (ck == NONLINEAR_MULT || (ck == DIVISION && j == 1))
+            {
+              exvar = itf->second;
+              return true;
+            }
           }
         }
         return false;
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index b2a0d888d..ba1295988 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -33,9 +33,9 @@ class CegConjecture;
  * This module is used to repair portions of candidate solutions. In particular,
  * given a synthesis conjecture:
  *   exists f. forall x. P( f, x )
- * and a candidate solution f = \x. t[x,c] where c are constants, this function
- * checks whether there exists a term of the form \x. t[x,c'] for some constants
- * c' such that:
+ * and a candidate solution f = \x. t[x,r] where r are repairable terms, this
+ * function checks whether there exists a term of the form \x. t[x,c'] for some
+ * constants c' such that:
  *   forall x. P( (\x. t[x,c']), x )  [***]
  * is satisfiable, where notice that the above formula after beta-reduction may
  * be one in pure first-order logic in a decidable theory (say linear
@@ -68,10 +68,22 @@ class SygusRepairConst
    * is a solution for the synthesis conjecture associated with this class.
    * Moreover, it is the case that
    *    repair_cv[j] != candidate_values[j], for at least one j.
+   * We always consider applications of the "any constant" constructors in
+   * candidate_values to be repairable. In addition, if the flag
+   * useConstantsAsHoles is true, we consider all constants whose (sygus) type
+   * admit alls constants to be repairable.
    */
   bool repairSolution(const std::vector<Node>& candidates,
                       const std::vector<Node>& candidate_values,
-                      std::vector<Node>& repair_cv);
+                      std::vector<Node>& repair_cv,
+                      bool useConstantsAsHoles = false);
+  /** must repair?
+   *
+   * This returns true if n must be repaired for it to be a valid solution.
+   * This corresponds to whether n contains a subterm that is a symbolic
+   * constructor like the "any constant" constructor.
+   */
+  static bool mustRepair(Node n);
 
  private:
   /** reference to quantifier engine */
@@ -100,26 +112,30 @@ class SygusRepairConst
    * already registered types.
    */
   void registerSygusType(TypeNode tn, std::map<TypeNode, bool>& tprocessed);
-  /**
-   * Returns true if n is a term of a sygus datatype type that allows all
-   * constants, and n encodes a constant. The term n must have a sygus datatype
-   * type.
+  /** is repairable?
+   *
+   * This returns true if n can be repaired by this class. In particular, we
+   * return true if n is an "any constant" constructor, or it is a constructor
+   * for a constant in a type that allows all constants and useConstantsAsHoles
+   * is true.
    */
-  bool isRepairableConstant(Node n);
+  static bool isRepairable(Node n, bool useConstantsAsHoles);
   /** get skeleton
    *
-   * Returns a skeleton for n, where the subterms of n that are repairable
-   * constants are replaced by free variables. Since we are interested in
+   * Returns a skeleton for sygus datatype value n, where the subterms of n that
+   * are repairable are replaced by free variables. Since we are interested in
    * returning canonical skeletons, the free variables we use in this
    * replacement are taken from TermDbSygus, where we track indices
    * in free_var_count. Variables we introduce in this way are added to sk_vars.
    * The mapping sk_vars_to_subs contains entries v -> c, where v is a
-   * variable in sk_vars, and c is the term in n that it replaced.
+   * variable in sk_vars, and c is the term in n that it replaced. The flag
+   * useConstantsAsHoles affects which terms we consider to be repairable.
    */
   Node getSkeleton(Node n,
                    std::map<TypeNode, int>& free_var_count,
                    std::vector<Node>& sk_vars,
-                   std::map<Node, Node>& sk_vars_to_subs);
+                   std::map<Node, Node>& sk_vars_to_subs,
+                   bool useConstantsAsHoles);
   /** get first-order query
    *
    * This function returns a formula that is equivalent to the negation of the
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 37a8ae382..126f01136 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -18,14 +18,12 @@
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory::inst;
 
 namespace CVC4 {
 namespace theory {
@@ -184,6 +182,12 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
   return mkGeneric(dt, c, var_count, pre);
 }
 
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
+{
+  std::map<int, Node> pre;
+  return mkGeneric(dt, c, pre);
+}
+
 struct SygusToBuiltinAttributeId
 {
 };
@@ -191,32 +195,48 @@ typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
     SygusToBuiltinAttribute;
 
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
+  std::map<TypeNode, int> var_count;
+  return sygusToBuiltin(n, tn, var_count);
+}
+
+Node TermDbSygus::sygusToBuiltin(Node n,
+                                 TypeNode tn,
+                                 std::map<TypeNode, int>& var_count)
+{
   Assert( n.getType()==tn );
   Assert( tn.isDatatype() );
 
   // has it already been computed?
-  if (n.hasAttribute(SygusToBuiltinAttribute()))
+  if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute()))
   {
     return n.getAttribute(SygusToBuiltinAttribute());
   }
-
   Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
                           << ", type = " << tn << std::endl;
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   if (n.getKind() == APPLY_CONSTRUCTOR)
   {
+    bool var_count_empty = var_count.empty();
     unsigned i = Datatype::indexOf(n.getOperator().toExpr());
     Assert(n.getNumChildren() == dt[i].getNumArgs());
-    std::map<TypeNode, int> var_count;
     std::map<int, Node> pre;
     for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
     {
-      pre[j] = sygusToBuiltin(n[j], getArgType(dt[i], j));
+      // if the child is a symbolic constructor, do not include it
+      if (!isSymbolicConsApp(n[j]))
+      {
+        pre[j] = sygusToBuiltin(
+            n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count);
+      }
     }
     Node ret = mkGeneric(dt, i, var_count, pre);
     Trace("sygus-db-debug")
         << "SygusToBuiltin : Generic is " << ret << std::endl;
-    n.setAttribute(SygusToBuiltinAttribute(), ret);
+    // cache if we had a fresh variable count
+    if (var_count_empty)
+    {
+      n.setAttribute(SygusToBuiltinAttribute(), ret);
+    }
     return ret;
   }
   if (n.hasAttribute(SygusPrintProxyAttribute()))
@@ -691,7 +711,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
         {
           for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
           {
-            registerSygusType(getArgType(dt[i], j));
+            TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+            registerSygusType(ctn);
+            // carry type attributes
+            if (d_has_subterm_sym_cons.find(ctn)
+                != d_has_subterm_sym_cons.end())
+            {
+              d_has_subterm_sym_cons[tn] = true;
+            }
           }
         }
         //iterate over constructors
@@ -725,6 +752,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
                   << std::endl;
             }
           }
+          // symbolic constructors
+          if (n.getAttribute(SygusAnyConstAttribute()))
+          {
+            d_sym_cons_any_constant[tn] = i;
+            d_has_subterm_sym_cons[tn] = true;
+          }
           // TODO (as part of #1170): we still do not properly catch type
           // errors in sygus grammars for arguments of builtin operators.
           // The challenge is that we easily ask for expected argument types of
@@ -736,13 +769,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
           // ensure that terms that this constructor encodes are
           // of the type specified in the datatype. This will fail if
           // e.g. bitvector-and is a constructor of an integer grammar.
-          std::map<int, Node> pre;
-          Node g = mkGeneric(dt, i, pre);
+          Node g = mkGeneric(dt, i);
           TypeNode gtn = g.getType();
           CVC4_CHECK(gtn.isSubtypeOf(btn))
               << "Sygus datatype " << dt.getName()
               << " encodes terms that are not of type " << btn << std::endl;
         }
+        // compute min type depth information
+        computeMinTypeDepthInternal(tn, tn, 0);
       }
     }
   }
@@ -751,7 +785,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
 void TermDbSygus::registerEnumerator(Node e,
                                      Node f,
                                      CegConjecture* conj,
-                                     bool mkActiveGuard)
+                                     bool mkActiveGuard,
+                                     bool useSymbolicCons)
 {
   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
   {
@@ -760,21 +795,81 @@ void TermDbSygus::registerEnumerator(Node e,
   }
   Trace("sygus-db") << "Register enumerator : " << e << std::endl;
   // register its type
-  registerSygusType(e.getType());
+  TypeNode et = e.getType();
+  registerSygusType(et);
   d_enum_to_conjecture[e] = conj;
   d_enum_to_synth_fun[e] = f;
+  NodeManager* nm = NodeManager::currentNM();
   if( mkActiveGuard ){
     // make the guard
-    Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
+    Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType()));
     eg = d_quantEngine->getValuation().ensureLiteral( eg );
     AlwaysAssert( !eg.isNull() );
     d_quantEngine->getOutputChannel().requirePhase( eg, true );
     //add immediate lemma
-    Node lem = NodeManager::currentNM()->mkNode( OR, eg, eg.negate() );
+    Node lem = nm->mkNode(OR, eg, eg.negate());
     Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
     d_quantEngine->getOutputChannel().lemma( lem );
     d_enum_to_active_guard[e] = eg;
   }
+
+  // depending on if we are using symbolic constructors, introduce symmetry
+  // breaking lemma templates for each relevant subtype of the grammar
+  std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
+      d_min_type_depth.find(et);
+  Assert(it != d_min_type_depth.end());
+  // for each type of subterm of this enumerator
+  for (const std::pair<const TypeNode, unsigned>& st : it->second)
+  {
+    std::vector<unsigned> rm_indices;
+    TypeNode stn = st.first;
+    Assert(stn.isDatatype());
+    const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype();
+    std::map<TypeNode, unsigned>::iterator itsa =
+        d_sym_cons_any_constant.find(stn);
+    if (itsa != d_sym_cons_any_constant.end())
+    {
+      if (!useSymbolicCons)
+      {
+        // do not use the symbolic constructor
+        rm_indices.push_back(itsa->second);
+      }
+      else
+      {
+        // can remove all other concrete constant constructors
+        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+        {
+          if (i != itsa->second)
+          {
+            Node c_op = getConsNumConst(stn, i);
+            if (!c_op.isNull())
+            {
+              rm_indices.push_back(i);
+            }
+          }
+        }
+      }
+    }
+    for (unsigned& rindex : rm_indices)
+    {
+      // make the apply-constructor corresponding to an application of the
+      // "any constant" constructor
+      Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR,
+                                Node::fromExpr(dt[rindex].getConstructor()));
+      // should not include the constuctor in any subterm
+      Node x = getFreeVar(stn, 0);
+      Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
+                        << " == " << exc_val << std::endl;
+      Node lem = getExplain()->getExplanationForEquality(x, exc_val);
+      lem = lem.negate();
+      Trace("cegqi-lemma")
+          << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
+          << std::endl;
+      // the size of the subterm we are blocking is the weight of the
+      // constructor (usually zero)
+      registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
+    }
+  }
 }
 
 bool TermDbSygus::isEnumerator(Node e) const
@@ -870,14 +965,10 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
   return it->second;
 }
 
-void TermDbSygus::clearSymBreakLemmas()
-{
-  d_enum_to_sb_lemmas.clear();
-  d_sb_lemma_to_type.clear();
-  d_sb_lemma_to_size.clear();
-}
+void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
 
-bool TermDbSygus::isRegistered( TypeNode tn ) {
+bool TermDbSygus::isRegistered(TypeNode tn) const
+{
   return d_register.find( tn )!=d_register.end();
 }
 
@@ -904,7 +995,6 @@ void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, un
 unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){
   std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
   if( it==d_min_type_depth[root_tn].end() ){
-    computeMinTypeDepthInternal( root_tn, root_tn, 0 );
     Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() );  
     return d_min_type_depth[root_tn][tn];
   }else{
@@ -1107,6 +1197,38 @@ bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeCons
   }
 }
 
+int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const
+{
+  Assert(isRegistered(tn));
+  std::map<TypeNode, unsigned>::const_iterator itt =
+      d_sym_cons_any_constant.find(tn);
+  if (itt != d_sym_cons_any_constant.end())
+  {
+    return static_cast<int>(itt->second);
+  }
+  return -1;
+}
+
+bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
+{
+  return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
+}
+
+bool TermDbSygus::isSymbolicConsApp(Node n) const
+{
+  if (n.getKind() != APPLY_CONSTRUCTOR)
+  {
+    return false;
+  }
+  TypeNode tn = n.getType();
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+  Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+  // it is symbolic if it represents "any constant"
+  return sygusOp.getAttribute(SygusAnyConstAttribute());
+}
+
 Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
   if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
       ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
@@ -1338,8 +1460,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod
       cc.insert( cc.end(), args.begin(), args.end() );
       pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
     }
-    std::map< TypeNode, int > var_count; 
-    Node ret = mkGeneric( dt, i, var_count, pre );
+    Node ret = mkGeneric(dt, i, pre);
     // if it is a variable, apply the substitution
     if( ret.getKind()==kind::BOUND_VARIABLE ){
       Assert( ret.hasAttribute(SygusVarNumAttribute()) );
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 9f370cd15..139e00794 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -63,7 +63,9 @@ class TermDbSygus {
    * conj : the conjecture that the enumeration of e is for.
    * f : the synth-fun that the enumeration of e is for.
    * mkActiveGuard : whether we want to make an active guard for e
-   * (see d_enum_to_active_guard).
+   * (see d_enum_to_active_guard),
+   * useSymbolicCons : whether we want model values for e to include symbolic
+   * constructors like the "any constant" variable.
    *
    * Notice that enumerator e may not be one-to-one with f in
    * synthesis-through-unification approaches (e.g. decision tree construction
@@ -72,7 +74,8 @@ class TermDbSygus {
   void registerEnumerator(Node e,
                           Node f,
                           CegConjecture* conj,
-                          bool mkActiveGuard = false);
+                          bool mkActiveGuard = false,
+                          bool useSymbolicCons = false);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
@@ -109,8 +112,8 @@ class TermDbSygus {
   TypeNode getTypeForSymBreakLemma(Node lem) const;
   /** Get the minimum size of terms symmetry breaking lemma lem applies to */
   unsigned getSizeForSymBreakLemma(Node lem) const;
-  /** Clear information about symmetry breaking lemmas */
-  void clearSymBreakLemmas();
+  /** Clear information about symmetry breaking lemmas for enumerator e */
+  void clearSymBreakLemmas(Node e);
   //------------------------------end enumerators
 
   //-----------------------------conversion from sygus to builtin
@@ -161,12 +164,19 @@ class TermDbSygus {
                  std::map<int, Node>& pre);
   /** same as above, but with empty var_count */
   Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+  /** same as above, but with empty pre */
+  Node mkGeneric(const Datatype& dt, int c);
   /** sygus to builtin
    *
    * Given a sygus datatype term n of type tn, this function returns its analog,
    * that is, the term that n encodes.
+   *
+   * Notice that each occurrence of a symbolic constructor application is
+   * replaced by a unique variable. To track counters for introducing unique
+   * variables, we use the var_count map.
    */
   Node sygusToBuiltin(Node n, TypeNode tn);
+  Node sygusToBuiltin(Node n, TypeNode tn, std::map<TypeNode, int>& var_count);
   /** same as above, but without tn */
   Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
   /** evaluate builtin
@@ -265,7 +275,8 @@ class TermDbSygus {
   Node d_true;
   Node d_false;
 
-private:
+ private:
+  /** computes the map d_min_type_depth */
   void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
   bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
 
@@ -282,6 +293,14 @@ private:
   std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
   // grammar information
   // root -> type -> _
+  /**
+   * For each sygus type t1, this maps datatype types t2 to the smallest size of
+   * a term of type t1 that includes t2 as a subterm. For example, for grammar:
+   *   A -> B+B | 0 | B-D
+   *   B -> C+C
+   *   ...
+   * we have that d_min_type_depth[A] = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+   */
   std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
   // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
   // d_consider_const;
@@ -290,9 +309,20 @@ private:
   std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
   /** a cache for getSelectorWeight */
   std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
+  /**
+   * For each sygus type, the index of the "any constant" constructor, if it
+   * has one.
+   */
+  std::map<TypeNode, unsigned> d_sym_cons_any_constant;
+  /**
+   * Whether any subterm of this type contains a symbolic constructor. This
+   * corresponds to whether sygus repair techniques will ever have any effect
+   * for this type.
+   */
+  std::map<TypeNode, bool> d_has_subterm_sym_cons;
 
  public:  // general sygus utilities
-  bool isRegistered( TypeNode tn );
+  bool isRegistered(TypeNode tn) const;
   // get the minimum depth of type in its parent grammar
   unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );
   // get the minimum size for a constructor term
@@ -319,6 +349,18 @@ private:
   int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
   /** is type match */
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
+  /**
+   * Get the index of the "any constant" constructor of type tn if it has one,
+   * or returns -1 otherwise.
+   */
+  int getAnyConstantConsNum(TypeNode tn) const;
+  /** has subterm symbolic constructor
+   *
+   * Returns true if any subterm of type tn can be a symbolic constructor.
+   */
+  bool hasSubtermSymbolicCons(TypeNode tn) const;
+  /** return whether n is an application of a symbolic constructor */
+  bool isSymbolicConsApp(Node n) const;
 
   TypeNode getSygusTypeForVar( Node v );
   Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index ed2390fe5..4324171a8 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -406,7 +406,6 @@ REG0_TESTS = \
 	regress0/expect/scrub.03.smt2 \
 	regress0/expect/scrub.04.smt2 \
 	regress0/expect/scrub.06.cvc \
-	regress0/expect/scrub.07.sy \
 	regress0/expect/scrub.08.sy \
 	regress0/expect/scrub.09.p \
 	regress0/flet.smt \
@@ -1974,7 +1973,6 @@ TESTS_EXPECT = \
 	regress0/decision/wchains010ue.smt.expect \
 	regress0/expect/scrub.01.smt.expect \
 	regress0/expect/scrub.03.smt2.expect \
-	regress0/expect/scrub.07.sy.expect \
 	regress0/quantifiers/bug291.smt2.expect \
 	regress0/uflia/check02.smt2.expect \
 	regress0/uflia/check03.smt2.expect \
diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy
deleted file mode 100644
index 79b917c7a..000000000
--- a/test/regress/regress0/expect/scrub.07.sy
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
-(set-logic LIA)
-(declare-var n Int)
-
-(synth-fun f ((n Int)) Int)
-(constraint (= (/ n n) 1))
-(check-synth)
diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect
deleted file mode 100644
index 4c5aa1491..000000000
--- a/test/regress/regress0/expect/scrub.07.sy.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
-% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
-% EXPECT: The fact in question: TERM
-% EXPECT: ")
-% EXIT: 1
diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy
index 61b08a838..c19b2ff42 100644
--- a/test/regress/regress2/sygus/ex23.sy
+++ b/test/regress/regress2/sygus/ex23.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const
 (set-logic LIA)
 
 (synth-inv inv-f ((y Int) (z Int) (c Int)))
@@ -20,4 +20,6 @@
 
 (inv-constraint inv-f pre-f trans-f post-f)
 
+; needs --sygus-repair-const, since easy solution involves the constant 4608
+
 (check-synth)