diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-16 14:55:28 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-16 14:55:28 -0600 |
commit | c603a047ac534ed4caafb128b5d333e05e1fd191 (patch) | |
tree | b24999a8050d82df3cbcb0a8ade4ba7990af56c8 /src/parser/smt2 | |
parent | 80daa7fd5917526513a510261fd3901f03949dfa (diff) |
Public interface for quantifier elimination. Minor changes to datatypes rewriter.
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'; |