diff options
Diffstat (limited to 'src')
-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'; |