diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-06-30 04:50:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-30 08:50:40 -0300 |
commit | 724d8cf23ae74158b36b408643298c49c3b20833 (patch) | |
tree | 737db246271ec879aaae7e62e49b858faf473e35 /src/parser/smt2 | |
parent | 6303c25fc375f33b27398f9b8c4b70901785a5f1 (diff) |
Interpolation step 1 (#4638)
This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The first step creates the API framework, while omits the implementation for getting interpolation.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3e8234a86..703696cf5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1136,6 +1136,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType())); } + | GET_INTERPOL_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType())); + } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] @@ -2315,6 +2326,7 @@ INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; +GET_INTERPOL_TOK : 'get-interpol'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands |