diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-19 21:34:45 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-19 21:34:45 -0500 |
commit | 45dd1c4f1695663ce0350ce71d72ec4b1850f043 (patch) | |
tree | bd521109d1ba4795e1714c4b7c04eb5c6da20fe6 /src/parser | |
parent | 6c47289737ca3c9a1345d4bf5666eaed4011edcc (diff) |
Support sygus standard command syntax set-feature (#7040)
This currently has no effect other than giving an unsupported warning.
In the future, set-feature will be implemented via the appropriate call to Solver::setOption if necessary.
Fixes #6182.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f56fc3c90..577aeb0a9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -585,10 +585,24 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd] } | /* check-synth */ CHECK_SYNTH_TOK - { PARSER_STATE->checkThatLogicIsSet(); } { + PARSER_STATE->checkThatLogicIsSet(); cmd.reset(new CheckSynthCommand()); } + | /* set-feature */ + SET_FEATURE_TOK keyword[name] symbolicExpr[expr] + { + PARSER_STATE->checkThatLogicIsSet(); + // ":grammars" is defined in the SyGuS version 2.1 standard and is by + // default supported, all other features are not. + if (name != ":grammars") + { + std::stringstream ss; + ss << "SyGuS feature " << name << " not currently supported"; + PARSER_STATE->warning(ss.str()); + } + cmd.reset(new EmptyCommand()); + } | command[&cmd] ; @@ -2270,7 +2284,7 @@ CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth'; DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var'; CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint'; INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint'; -SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options'; +SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature'; SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant'; SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; |