diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-09 11:40:59 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-09 11:40:59 -0800 |
| commit | c6085d9b70beb9a2be5a26a3c085b4f1a1758410 (patch) | |
| tree | 71f9fc4d9df2264994f34dabf77fd16de90ea851 /src/parser | |
| parent | 6330388f2606e82c4348de9ba6c62c4de7861cd9 (diff) | |
Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 889352299..2c26c824f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -462,6 +462,9 @@ command [std::unique_ptr<CVC4::Command>* cmd] | /* get-proof */ GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetProofCommand()); } + | /* get-unsat-assumptions */ + GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { cmd->reset(new GetUnsatAssumptionsCommand); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetUnsatCoreCommand); } @@ -1286,7 +1289,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] } cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); } - // GET_UNSAT_ASSUMPTIONS ; extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @@ -1726,7 +1728,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK - | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK + | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK + | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK @@ -3086,6 +3089,7 @@ GET_VALUE_TOK : 'get-value'; GET_ASSIGNMENT_TOK : 'get-assignment'; GET_ASSERTIONS_TOK : 'get-assertions'; GET_PROOF_TOK : 'get-proof'; +GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset'; |