diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 07:43:19 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 07:43:19 -0600 |
| commit | c2757f0440c5d5b841e05c60d1fd93dc9ee3763a (patch) | |
| tree | dde6e588873a20c5bb9edf28f383f2eb00c39eb5 /src/parser | |
| parent | 0df0954069d56e3323a225ffa72c5913d0333ac2 (diff) | |
Add proper support for the declare-heap command for separation logic (#5405)
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.
This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.
Fixes #5343, fixes #4926.
Work towards CVC4/cvc4-wishues#22.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fe051f036..40c66eaa5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -895,7 +895,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; CVC4::api::Term e, e2; - CVC4::api::Sort t; + CVC4::api::Sort t, s; std::string name; std::vector<std::string> names; std::vector<CVC4::api::Term> terms; @@ -1073,9 +1073,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] } | 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()); } + sortSymbol[s, CHECK_DECLARED] + { cmd->reset(new DeclareHeapCommand(t, s)); } RPAREN_TOK | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new BlockModelCommand()); } |