diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-05 14:05:26 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-05 14:05:26 -0800 |
| commit | d51c8347a3c6bf7857c474bd3493377f9fed58e5 (patch) | |
| tree | 56da229cd8fcbe6988937514820c13c3894f2558 /src/parser/smt2 | |
| parent | d1aa4ae101987093a06208650e2ea4878f7437ca (diff) | |
Add support for check-sat-assuming. (#1637)
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b9a2a8805..889352299 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -431,7 +431,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } | /* check-sat */ - CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support check-sat command."); } @@ -446,6 +446,16 @@ command [std::unique_ptr<CVC4::Command>* cmd] | { expr = MK_CONST(bool(true)); } ) { cmd->reset(new CheckSatCommand(expr)); } + | /* check-sat-assuming */ + CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); } + ( LPAREN_TOK termList[terms,expr] RPAREN_TOK + { cmd->reset(new CheckSatAssumingCommand(terms)); } + | ~LPAREN_TOK + { PARSER_STATE->parseError("The check-sat-assuming command expects a " + "list of terms. Perhaps you forgot a pair of " + "parentheses?"); + } + ) | /* get-assertions */ GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetAssertionsCommand()); } @@ -1276,7 +1286,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] } cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); } - // CHECK_SAT_ASSUMING still being discussed // GET_UNSAT_ASSUMPTIONS ; @@ -1713,7 +1722,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] // } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } - | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK + | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK + | 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 @@ -3064,7 +3074,8 @@ selector[CVC4::DatatypeConstructor& ctor] // Base SMT-LIB tokens ASSERT_TOK : 'assert'; -CHECKSAT_TOK : 'check-sat'; +CHECK_SAT_TOK : 'check-sat'; +CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; |