diff options
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fb3b5ec5e..9d2392715 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1302,6 +1302,12 @@ extendedCommand[CVC4::Command*& cmd] | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] { cmd = new SimplifyCommand(e); } + | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); } + term[e,e2] + { cmd = new GetQuantifierEliminationCommand(e, true); } + | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + term[e,e2] + { cmd = new GetQuantifierEliminationCommand(e, false); } ; @@ -2562,6 +2568,8 @@ DECLARE_CONST_TOK : 'declare-const'; DEFINE_CONST_TOK : 'define-const'; SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; +GET_QE_TOK : 'get-qe'; +GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; // SyGuS commands SYNTH_FUN_TOK : 'synth-fun'; |