diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /src/parser | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 16 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
2 files changed, 16 insertions, 7 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d72188c6c..a95689f1c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1529,8 +1529,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } - | DECLARE_HEAP LPAREN_TOK - sortSymbol[t,CHECK_DECLARED] + | GET_ABDUCT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetAbductCommand(name,e, t)); + } + | DECLARE_HEAP LPAREN_TOK + sortSymbol[t,CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] // We currently do nothing with the type information declared for the heap. { cmd->reset(new EmptyCommand()); } @@ -3055,6 +3066,7 @@ SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; +GET_ABDUCT_TOK : 'get-abduct'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 278f2bdfd..752bf58b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -674,11 +674,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } // get unlocked copy, modify, copy and relock LogicInfo log(d_logic.getUnlockedCopy()); - log.enableQuantifiers(); - log.enableTheory(theory::THEORY_UF); - log.enableTheory(theory::THEORY_DATATYPES); - log.enableIntegers(); - log.enableHigherOrder(); + // enable everything needed for sygus + log.enableSygus(); d_logic = log; d_logic.lock(); } |