summaryrefslogtreecommitdiff
path: root/src/options/options_handler.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-12-04 17:18:06 -0600
committerGitHub <noreply@github.com>2019-12-04 17:18:06 -0600
commitdd66d825a0e05b46690b0bb914da3b0aa2045654 (patch)
tree7648d3693578c2dbf8b74216fe335990784b3380 /src/options/options_handler.h
parent1741bb48e54f25ef4fd7776380deca1dd60a2201 (diff)
New grammar construction modes for SyGuS (#3486)
Diffstat (limited to 'src/options/options_handler.h')
-rw-r--r--src/options/options_handler.h3
1 files changed, 3 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback