New grammar construction modes for SyGuS (#3486)

14 files changed, 472 insertions, 36 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d4194d456..faf358573 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -569,6 +569,29 @@ auto (default) \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_sygusGrammarConsHelp =
+    "\
+Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\
+\n\
+simple (default) \n\
++ Use simple grammar construction (no symbolic terms or constants).\n\
+\n\
+any-const  \n\
++ Use symoblic constant constructors.\n\
+\n\
+any-term  \n\
++ When applicable, use constructors corresponding to any symbolic term.\n\
+This option enables a sum-of-monomials grammar for arithmetic. For all\n\
+other types, it enables symbolic constant constructors.\n\
+\n\
+any-term-concise  \n\
++ When applicable, use constructors corresponding to any symbolic term,\n\
+favoring conciseness over generality. This option is equivalent to any-term\n\
+but enables a polynomial grammar for arithmetic when not in a combined\n\
+theory.\n\
+\n\
+";
+
 const std::string OptionsHandler::s_macrosQuantHelp = "\
 Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 \n\
@@ -1085,6 +1108,38 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option,
                           + optarg + "'.  Try --sygus-inv-templ help.");
   }
 }
+theory::quantifiers::SygusGrammarConsMode
+OptionsHandler::stringToSygusGrammarConsMode(std::string option,
+                                             std::string optarg)
+{
+  if (optarg == "simple")
+  {
+    return theory::quantifiers::SYGUS_GCONS_SIMPLE;
+  }
+  else if (optarg == "any-const")
+  {
+    return theory::quantifiers::SYGUS_GCONS_ANY_CONST;
+  }
+  else if (optarg == "any-term")
+  {
+    return theory::quantifiers::SYGUS_GCONS_ANY_TERM;
+  }
+  else if (optarg == "any-term-concise")
+  {
+    return theory::quantifiers::SYGUS_GCONS_ANY_TERM_CONCISE;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusGrammarConsHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(
+        std::string("unknown option for --sygus-grammar-cons: `") + optarg
+        + "'.  Try --sygus-grammar-cons help.");
+  }
+}
 
 theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
     std::string option, std::string optarg)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 84b7002e3..eae61c5b2 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -122,6 +122,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
       std::string option, std::string optarg);
+  theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode(
+      std::string option, std::string optarg);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
       std::string option, std::string optarg);
   theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(
@@ -275,6 +277,7 @@ public:
   static const std::string s_sygusFilterSolHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_sygusActiveGenHelp;
+  static const std::string s_sygusGrammarConsHelp;
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
   static const std::string s_triggerSelModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 049cdef1c..9ff2ac196 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -292,6 +292,29 @@ enum SygusFilterSolMode
   SYGUS_FILTER_SOL_WEAK,
 };
 
+enum SygusGrammarConsMode
+{
+  /**
+   * Use simple default SyGuS grammar construction (no symbolic terms or
+   * constants).
+   */
+  SYGUS_GCONS_SIMPLE,
+  /** Use "any constant" constructors in default SyGuS grammar construction. */
+  SYGUS_GCONS_ANY_CONST,
+  /**
+   * When applicable, use constructors that encode any term using "any constant"
+   * constructors. This construction uses sum-of-monomials for arithmetic
+   * grammars.
+   */
+  SYGUS_GCONS_ANY_TERM,
+  /**
+   * When applicable, use constructors that encode any term using "any constant"
+   * constructors in a way that prefers conciseness over generality. This
+   * construction uses polynomials for arithmetic grammars.
+   */
+  SYGUS_GCONS_ANY_TERM_CONCISE,
+};
+
 enum MacrosQuantMode {
   /** infer all definitions */
   MACROS_QUANT_MODE_ALL,
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 019b052bc..171af1e47 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1077,6 +1077,16 @@ header = "options/quantifiers_options.h"
   help       = "embed sygus templates into grammars"
 
 [[option]]
+  name       = "sygusGrammarConsMode"
+  category   = "regular"
+  long       = "sygus-grammar-cons=MODE"
+  type       = "CVC4::theory::quantifiers::SygusGrammarConsMode"
+  default    = "CVC4::theory::quantifiers::SYGUS_GCONS_SIMPLE"
+  handler    = "stringToSygusGrammarConsMode"
+  includes   = ["options/quantifiers_modes.h"]
+  help       = "mode for SyGuS grammar construction"
+
+[[option]]
   name       = "sygusInvTemplMode"
   category   = "regular"
   long       = "sygus-inv-templ=MODE"
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index 5bf0ca036..43d23b523 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -125,8 +125,14 @@ Node mkSygusTerm(const Datatype& dt,
   Assert(i < dt.getNumConstructors());
   Assert(dt.isSygus());
   Assert(!dt[i].getSygusOp().isNull());
-  std::vector<Node> schildren;
   Node op = Node::fromExpr(dt[i].getSygusOp());
+  return mkSygusTerm(op, children, doBetaReduction);
+}
+
+Node mkSygusTerm(Node op,
+                 const std::vector<Node>& children,
+                 bool doBetaReduction)
+{
   Trace("dt-sygus-util") << "Operator is " << op << std::endl;
   if (children.empty())
   {
@@ -140,6 +146,7 @@ Node mkSygusTerm(const Datatype& dt,
     Assert(children.size() == 1);
     return children[0];
   }
+  std::vector<Node> schildren;
   // get the kind of the operator
   Kind ok = op.getKind();
   if (ok != BUILTIN)
diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index 2ac288c4c..5f74a4bee 100644
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -148,6 +148,13 @@ Node mkSygusTerm(const Datatype& dt,
                  const std::vector<Node>& children,
                  bool doBetaReduction = true);
 /**
+ * Same as above, but we already have the sygus operator op. The above method
+ * is syntax sugar for calling this method on dt[i].getSygusOp().
+ */
+Node mkSygusTerm(Node op,
+                 const std::vector<Node>& children,
+                 bool doBetaReduction = true);
+/**
  * n is a builtin term that is an application of operator op.
  *
  * This returns an n' such that (eval n args) is n', where n' is a instance of
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index c806bb1e7..7a9a9ca21 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -77,8 +77,11 @@ bool Cegis::processInitialize(Node conj,
   for (unsigned i = 0; i < csize; i++)
   {
     Trace("cegis") << "...register enumerator " << candidates[i];
+    // We use symbolic constants if we are doing repair constants or if the
+    // grammar construction was not simple.
     bool useSymCons = false;
-    if (options::sygusRepairConst())
+    if (options::sygusRepairConst()
+        || options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE)
     {
       TypeNode ctn = candidates[i].getType();
       d_tds->registerSygusType(ctn);
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index b1baed9cb..cf1993efb 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -189,8 +189,13 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
   TypeNode ntn = n.getType();
   if (!ntn.isDatatype())
   {
-    // sygus datatype fields that are not sygus datatypes are treated as
-    // abstractions only, hence we disregard this field
+    // SyGuS datatype fields that are not sygus datatypes are treated as
+    // abstractions only, hence we disregard this field. It is important
+    // that users of this method pay special attention to any constants,
+    // otherwise the explanation n.eqNode(vn) is necessary here. For example,
+    // any lemma schema that blocks the current value of an enumerator should
+    // not make any assumptions about the value of the arguments of its any
+    // constant constructors, since their explanation is not included here.
     return;
   }
   Assert(vn.getKind() == APPLY_CONSTRUCTOR);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d00df38c5..5e4513ff3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -20,6 +20,7 @@
 #include "options/quantifiers_options.h"
 #include "printer/sygus_print_callback.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
@@ -515,10 +516,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   std::map<TypeNode, TypeNode> sygus_to_builtin;
 
   std::vector<TypeNode> types;
-  // collect connected types for each of the variables
+  // Collect connected types for each of the variables.
   for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
   {
-    collectSygusGrammarTypesFor(sygus_vars[i].getType(), types);
+    TypeNode tni = sygus_vars[i].getType();
+    collectSygusGrammarTypesFor(tni, types);
   }
   // collect connected types to range
   collectSygusGrammarTypesFor(range, types);
@@ -534,6 +536,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   std::map<TypeNode, TypeNode> type_to_unres;
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator
       itc;
+  // maps types to the index of its "any term" grammar construction
+  std::map<TypeNode, unsigned> typeToGAnyTerm;
+  SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
     std::stringstream ss;
@@ -556,10 +561,40 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     type_to_unres[types[i]] = unres_t;
     sygus_to_builtin[unres_t] = types[i];
   }
-  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  // We ensure an ordering on types such that parametric types are processed
+  // before their consitituents. Since parametric types were added before their
+  // arguments in collectSygusGrammarTypesFor above, we will construct the
+  // sygus grammars by iterating on types in reverse order. This ensures
+  // that we know all constructors coming from other types (e.g. select(A,i))
+  // by the time we process the type.
+  for (int i = (types.size() - 1); i >= 0; --i)
   {
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     TypeNode unres_t = unres_types[i];
+    SygusGrammarConsMode tsgcm = sgcm;
+    if (tsgcm == SYGUS_GCONS_ANY_TERM || tsgcm == SYGUS_GCONS_ANY_TERM_CONCISE)
+    {
+      // If the type does not support any term, we do any constant instead.
+      // We also fall back on any constant construction if the type has no
+      // constructors at this point (e.g. it simply encodes all constants).
+      if (!types[i].isReal())
+      {
+        tsgcm = SYGUS_GCONS_ANY_CONST;
+      }
+      else
+      {
+        // Add a placeholder for the "any term" version of this datatype, to be
+        // constructed later.
+        typeToGAnyTerm[types[i]] = sdts.size();
+        std::stringstream ssat;
+        ssat << sdts[i].d_sdt.getName() << "_any_term";
+        sdts.push_back(SygusDatatypeGenerator(ssat.str()));
+        TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres);
+        unres_types.push_back(unresAnyTerm);
+      }
+    }
+    Trace("sygus-grammar-def")
+        << "Grammar constructor mode for this type is " << tsgcm << std::endl;
     //add variables
     for (const Node& sv : sygus_vars)
     {
@@ -592,29 +627,44 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       }
     }
     //add constants
-    std::vector< Node > consts;
-    mkSygusConstantsForType( types[i], consts );
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
-        itec = extra_cons.find(types[i]);
-    if( itec!=extra_cons.end() ){
-      for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
-               itec->second.begin();
-           set_it != itec->second.end();
-           ++set_it)
+    std::vector<Node> consts;
+    mkSygusConstantsForType(types[i], consts);
+    if (tsgcm == SYGUS_GCONS_ANY_CONST)
+    {
+      // Use the any constant constructor. Notice that for types that don't
+      // have constants (e.g. uninterpreted or function types), we don't add
+      // this constructor.
+      if (!consts.empty())
       {
-        if (std::find(consts.begin(), consts.end(), *set_it) == consts.end())
-        {
-          consts.push_back(*set_it);
-        }
+        sdts[i].d_sdt.addAnyConstantConstructor(types[i]);
       }
     }
-    for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
+    else
     {
-      std::stringstream ss;
-      ss << consts[j];
-      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
-      std::vector<TypeNode> cargsEmpty;
-      sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty);
+      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
+          itec = extra_cons.find(types[i]);
+      if (itec != extra_cons.end())
+      {
+        for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
+                 itec->second.begin();
+             set_it != itec->second.end();
+             ++set_it)
+        {
+          if (std::find(consts.begin(), consts.end(), *set_it) == consts.end())
+          {
+            consts.push_back(*set_it);
+          }
+        }
+      }
+      for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
+      {
+        std::stringstream ss;
+        ss << consts[j];
+        Trace("sygus-grammar-def")
+            << "...add for constant " << ss.str() << std::endl;
+        std::vector<TypeNode> cargsEmpty;
+        sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty);
+      }
     }
     // ITE
     Kind k = ITE;
@@ -641,12 +691,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         Trace("sygus-grammar-def")
             << "  ...create auxiliary Positive Integers grammar\n";
-        /* Creating type for positive integers */
+        // Creating type for positive integers. Notice we can't use the any
+        // constant constructor here, since it admits zero.
         std::stringstream ss;
         ss << fun << "_PosInt";
         std::string pos_int_name = ss.str();
         // make unresolved type
-        TypeNode unres_pos_int_t = mkUnresolvedType(pos_int_name, unres);
+        TypeNode unresPosInt = mkUnresolvedType(pos_int_name, unres);
+        unres_types.push_back(unresPosInt);
         // make data type for positive constant integers
         sdts.push_back(SygusDatatypeGenerator(pos_int_name));
         /* Add operator 1 */
@@ -657,8 +709,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         Kind k = PLUS;
         Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n";
         std::vector<TypeNode> cargsPlus;
-        cargsPlus.push_back(unres_pos_int_t);
-        cargsPlus.push_back(unres_pos_int_t);
+        cargsPlus.push_back(unresPosInt);
+        cargsPlus.push_back(unresPosInt);
         sdts.back().addConstructor(k, cargsPlus);
         sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true);
         Trace("sygus-grammar-def")
@@ -668,7 +720,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         Trace("sygus-grammar-def") << "\t...add for " << k << std::endl;
         std::vector<TypeNode> cargsDiv;
         cargsDiv.push_back(unres_t);
-        cargsDiv.push_back(unres_pos_int_t);
+        cargsDiv.push_back(unresPosInt);
         sdts[i].addConstructor(k, cargsDiv);
       }
     }
@@ -812,7 +864,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           << types[i] << std::endl;
     }
   }
-  // make datatypes
+  std::map<TypeNode, unsigned>::iterator itgat;
+  // initialize the datatypes
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
     sdts[i].d_sdt.initializeDatatype(types[i], bvl, true, true);
@@ -822,8 +875,227 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     if( types[i]==range ){
       startIndex = i;
     }
-  }
+    itgat = typeToGAnyTerm.find(types[i]);
+    if (itgat == typeToGAnyTerm.end())
+    {
+      // no any term datatype, we are done
+      continue;
+    }
+    Trace("sygus-grammar-def")
+        << "Build any-term datatype for " << types[i] << "..." << std::endl;
+    unsigned iat = itgat->second;
+    // for now, only real has any term construction
+    Assert(types[i].isReal());
+    // We have initialized the given type sdts[i], which should now contain
+    // a constructor for each relevant arithmetic term/variable. We now
+    // construct a sygus datatype of one of the following two forms.
+    //
+    // (1) The "sum of monomials" grammar:
+    //   I -> C*x1 | ... | C*xn | C | I + I | ite( B, I, I )
+    //   C -> any_constant
+    // where x1, ..., xn are the arithmetic terms/variables (non-arithmetic
+    // builtin operators) terms we have considered thus far.
+    //
+    // (2) The "polynomial" grammar:
+    //   I -> C*x1 + ... + C*xn + C | ite( B, I, I )
+    //   C -> any_constant
+    //
+    // The advantage of the first is that it allows for sums of terms
+    // constructible from other theories that share sorts with arithmetic, e.g.
+    //   c1*str.len(x) + c2*str.len(y)
+    // The advantage of the second is that there are fewer constructors, and
+    // hence may be more efficient.
 
+    // Before proceeding, we build the any constant datatype
+    Trace("sygus-grammar-def")
+        << "Build any-constant datatype for " << types[i] << std::endl;
+    std::stringstream ss;
+    ss << fun << "_AnyConst";
+    // Make sygus datatype for any constant.
+    TypeNode unresAnyConst = mkUnresolvedType(ss.str(), unres);
+    unres_types.push_back(unresAnyConst);
+    sdts.push_back(SygusDatatypeGenerator(ss.str()));
+    sdts.back().d_sdt.addAnyConstantConstructor(types[i]);
+    sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true);
+
+    // Now get the reference to the sygus datatype at position i (important that
+    // this comes after the modification to sdts above, which may modify
+    // the references).
+    const SygusDatatype& sdti = sdts[i].d_sdt;
+    // whether we will use the polynomial grammar
+    bool polynomialGrammar = sgcm == SYGUS_GCONS_ANY_TERM_CONCISE;
+    // A set of constructor indices that will be used in the overall sum we
+    // are constructing; indices of constructors corresponding to builtin
+    // arithmetic operators will be excluded from this set.
+    std::set<unsigned> useConstructor;
+    Trace("sygus-grammar-def")
+        << "Look at operators, num = " << sdti.getNumConstructors() << "..."
+        << std::endl;
+    for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++)
+    {
+      const SygusDatatypeConstructor& sdc = sdti.getConstructor(k);
+      Node sop = sdc.d_op;
+      bool isBuiltinArithOp = (sop.getKind() == CONST_RATIONAL);
+      bool hasExternalType = false;
+      for (unsigned j = 0, nargs = sdc.d_argTypes.size(); j < nargs; j++)
+      {
+        // Since we are accessing the fields of the sygus datatype, this
+        // already corresponds to the correct sygus datatype type.
+        TypeNode atype = sdc.d_argTypes[j];
+        if (atype == unres_types[i])
+        {
+          // It is recursive, thus is (likely) a builtin arithmetic operator
+          // as constructed above. It may also be an operator from another
+          // theory that has both an arithmetic return type and an arithmetic
+          // argument (e.g. str.indexof). In either case, we ignore it for the
+          // sake of well-foundedness.
+          isBuiltinArithOp = true;
+          break;
+        }
+        else if (atype != unres_bt)
+        {
+          // It is an external type. This is the case of an operator of another
+          // theory whose return type is arithmetic, e.g. select.
+          hasExternalType = true;
+        }
+      }
+      if (!isBuiltinArithOp)
+      {
+        useConstructor.insert(k);
+        if (hasExternalType)
+        {
+          // If we have an external term in the sum, e.g. select(A,i), we
+          // cannot use a fixed polynomial template. As mentioned above, we
+          // cannot use a polynomial grammar when external terms (those built
+          // from the symbols of other theories) are involved.
+          Trace("sygus-grammar-def")
+              << "Cannot use polynomial grammar due to " << sop << std::endl;
+          polynomialGrammar = false;
+        }
+      }
+    }
+    Trace("sygus-grammar-def")
+        << "Done look at operators, num = " << sdti.getNumConstructors()
+        << "..." << std::endl;
+    // we have now decided whether we will use sum-of-monomials or polynomial
+    // Now, extract the terms and set up the polynomial
+    std::vector<Node> sumChildren;
+    std::vector<TypeNode> cargsAnyTerm;
+    std::vector<Node> lambdaVars;
+    for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++)
+    {
+      Trace("sygus-grammar-def") << "Process #" << k << std::endl;
+      if (useConstructor.find(k) == useConstructor.end())
+      {
+        Trace("sygus-grammar-def") << "Skip variable #" << k << std::endl;
+        // builtin operator, as computed above, we skip
+        continue;
+      }
+      const SygusDatatypeConstructor& sdc = sdti.getConstructor(k);
+      Node sop = sdc.d_op;
+      Trace("sygus-grammar-def")
+          << "Monomial variable: #" << k << ": " << sop << std::endl;
+      unsigned nargs = sdc.d_argTypes.size();
+      std::vector<TypeNode> opCArgs;
+      std::vector<Node> opLArgs;
+      if (nargs > 0)
+      {
+        // Take its arguments. For example, if we are building a polynomial
+        // over str.len(s), then our any term constructor would include an
+        // argument of string type, e.g.:
+        //   (lambda s : String, c1, c2 : Int. c1*len(s) + c2)
+        for (unsigned j = 0; j < nargs; j++)
+        {
+          // this is already corresponds to the correct sygus datatype type
+          TypeNode atype = sdc.d_argTypes[j];
+          opCArgs.push_back(atype);
+          // get the builtin type
+          TypeNode btype = sygus_to_builtin[atype];
+          opLArgs.push_back(nm->mkBoundVar(btype));
+        }
+        // Do beta reduction on the operator so that its arguments match the
+        // fresh variables of the lambda (op) we are constructing below.
+        sop = datatypes::utils::mkSygusTerm(sop, opLArgs);
+        sop = Rewriter::rewrite(sop);
+      }
+      opCArgs.push_back(unresAnyConst);
+      Node coeff = nm->mkBoundVar(types[i]);
+      opLArgs.push_back(coeff);
+      Node monomial = nm->mkNode(MULT, coeff, sop);
+      if (polynomialGrammar)
+      {
+        // add the monomial c*t to the sum
+        sumChildren.push_back(monomial);
+        lambdaVars.insert(lambdaVars.end(), opLArgs.begin(), opLArgs.end());
+        cargsAnyTerm.insert(cargsAnyTerm.end(), opCArgs.begin(), opCArgs.end());
+      }
+      else
+      {
+        Node op =
+            nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial);
+        // use a print callback since we do not want to print the lambda
+        std::shared_ptr<SygusPrintCallback> spc;
+        std::vector<Expr> opLArgsExpr;
+        for (unsigned i = 0, nvars = opLArgs.size(); i < nvars; i++)
+        {
+          opLArgsExpr.push_back(opLArgs[i].toExpr());
+        }
+        spc = std::make_shared<printer::SygusExprPrintCallback>(
+            monomial.toExpr(), opLArgsExpr);
+        // add it as a constructor
+        std::stringstream ssop;
+        ssop << "monomial_" << sdc.d_name;
+        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc);
+      }
+    }
+    if (polynomialGrammar)
+    {
+      // add the constant
+      Node coeff = nm->mkBoundVar(types[i]);
+      lambdaVars.push_back(coeff);
+      cargsAnyTerm.push_back(unresAnyConst);
+      // make the sygus operator lambda X. c1*t1 + ... + cn*tn + c
+      Assert(sumChildren.size() > 1);
+      Node ops = nm->mkNode(PLUS, sumChildren);
+      Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops);
+      std::shared_ptr<SygusPrintCallback> spc;
+      std::vector<Expr> lambdaVarsExpr;
+      for (unsigned i = 0, nvars = lambdaVars.size(); i < nvars; i++)
+      {
+        lambdaVarsExpr.push_back(lambdaVars[i].toExpr());
+      }
+      spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(),
+                                                              lambdaVarsExpr);
+      Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
+      // make the any term datatype, add to back
+      // do not consider the exclusion criteria of the generator
+      sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc);
+    }
+    else
+    {
+      // add the any constant constructor as a separate constructor
+      sdts[iat].d_sdt.addAnyConstantConstructor(types[i]);
+      // add plus
+      std::vector<TypeNode> cargsPlus;
+      cargsPlus.push_back(unres_types[iat]);
+      cargsPlus.push_back(unres_types[iat]);
+      sdts[iat].d_sdt.addConstructor(PLUS, cargsPlus);
+    }
+    // add the ITE, regardless of sum-of-monomials vs polynomial
+    std::vector<TypeNode> cargsIte;
+    cargsIte.push_back(unres_bt);
+    cargsIte.push_back(unres_types[iat]);
+    cargsIte.push_back(unres_types[iat]);
+    sdts[iat].d_sdt.addConstructor(ITE, cargsIte);
+    sdts[iat].d_sdt.initializeDatatype(types[i], bvl, true, true);
+    Trace("sygus-grammar-def")
+        << "...built datatype " << sdts[iat].d_sdt.getDatatype() << std::endl;
+    // if the type is range, use it as the default type
+    if (types[i] == range)
+    {
+      startIndex = iat;
+    }
+  }
   //------ make Boolean type
   TypeNode btype = nm->booleanType();
   sdts.push_back(SygusDatatypeGenerator(dbname));
@@ -860,6 +1132,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       continue;
     }
+    unsigned iuse = i;
+    // use the any-term type if it exists
+    itgat = typeToGAnyTerm.find(types[i]);
+    if (itgat != typeToGAnyTerm.end())
+    {
+      iuse = itgat->second;
+    }
     Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
     //add equality per type
     Kind k = EQUAL;
@@ -867,8 +1146,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     std::stringstream ss;
     ss << kindToString(k) << "_" << types[i];
     std::vector<TypeNode> cargsBinary;
-    cargsBinary.push_back(unres_types[i]);
-    cargsBinary.push_back(unres_types[i]);
+    cargsBinary.push_back(unres_types[iuse]);
+    cargsBinary.push_back(unres_types[iuse]);
     sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargsBinary);
     // type specific predicates
     if (types[i].isReal())
@@ -889,7 +1168,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "...add for testers" << std::endl;
       const Datatype& dt = types[i].getDatatype();
       std::vector<TypeNode> cargsTester;
-      cargsTester.push_back(unres_types[i]);
+      cargsTester.push_back(unres_types[iuse]);
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
         Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cf06d2e90..7d3fb2d5c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1713,6 +1713,7 @@ set(regress_1_tests
   regress1/sygus/icfp_14_12_diff_types.sy
   regress1/sygus/icfp_28_10.sy
   regress1/sygus/icfp_easy-ite.sy
+  regress1/sygus/int-any-const.sy
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
@@ -1750,6 +1751,7 @@ set(regress_1_tests
   regress1/sygus/process-10-vars.sy
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
+  regress1/sygus/real-any-const.sy
   regress1/sygus/real-grammar.sy
   regress1/sygus/rec-fun-swap.sy
   regress1/sygus/rec-fun-sygus.sy
@@ -1760,6 +1762,7 @@ set(regress_1_tests
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
+  regress1/sygus/strings-any-term1.sy
   regress1/sygus/strings-no-syntax.sy
   regress1/sygus/strings-concat-3-args.sy
   regress1/sygus/strings-double-rec.sy
@@ -1924,6 +1927,7 @@ set(regress_3_tests
   regress3/pp-regfile.smtv1.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
   regress3/sixfuncs.sy
+  regress3/strings-any-term.sy
   regress3/strings/extf_d_perf.smt2
 )
 
diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy
new file mode 100644
index 000000000..b5de57533
--- /dev/null
+++ b/test/regress/regress1/sygus/int-any-const.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+
+(set-logic LIA)
+(synth-fun f ((x Int) (y Int)) Int)
+(constraint (= (f 1 7) 15))
+(constraint (= (f 0 27) 27))
+(constraint (= (f 2 27) 43))
+; this example does not fit the polynomial solution to the above example, thus, we expect to construct an ITE
+(constraint (= (f 3 27) 43))
+(check-synth)
diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy
new file mode 100644
index 000000000..2b59b7301
--- /dev/null
+++ b/test/regress/regress1/sygus/real-any-const.sy
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+
+(set-logic LRA)
+(synth-fun f ((x Real) (y Real)) Real)
+(constraint (= (f 1.5 7.5) 59.7))
+(constraint (= (f 0.5 27.5) 174.9))
+(constraint (= (f 0.8 20.0) 131.04))
+(check-synth)
diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy
new file mode 100644
index 000000000..3d8fd7530
--- /dev/null
+++ b/test/regress/regress1/sygus/strings-any-term1.sy
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
+(set-logic ALL)
+(synth-fun f ((x String) (y String)) Int)
+(declare-var x String)
+(constraint (= (f "A" "BC") 11))
+(constraint (= (f "BB" "CC") 18))
+(constraint (= (f "BCB" "") 25))
+(constraint (= (f "BCBD" "") 32))
+(check-synth)
diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy
new file mode 100644
index 000000000..88b30b208
--- /dev/null
+++ b/test/regress/regress3/strings-any-term.sy
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
+(set-logic ALL)
+(synth-fun f ((x String) (y String)) Int)
+(declare-var x String)
+(constraint (= (f "A" "BC") 207))
+(constraint (= (f "BB" "CC") 214))
+(constraint (= (f "BCB" "") 21))
+(constraint (= (f "BCBD" "") 28))
+(check-synth)