New grammar construction modes for SyGuS (#3486)

4 files changed, 91 insertions, 0 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"