diff options
| author | makaimann <makaim@stanford.edu> | 2020-06-04 18:21:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-04 18:21:37 -0700 |
| commit | a2fc412f22552ae0e8f9c36650d1de2d362638dd (patch) | |
| tree | 5f66f0f8128a826e6099845191ccbe5efdd0f3c3 /src/parser | |
| parent | 67678d6c8a28e71483d8171311725e9e1a86775c (diff) | |
Add a method for retrieving base of a constant array through API (#4494)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 62bf7e974..ec3e874df 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1990,7 +1990,7 @@ qualIdentifier[CVC4::ParseOp& p] | LPAREN_TOK AS_TOK ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { - p.d_kind = api::STORE_ALL; + p.d_kind = api::CONST_ARRAY; PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 608e47a6b..3f25e3776 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1535,7 +1535,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type << std::endl; // (as const (Array T1 T2)) - if (p.d_kind == api::STORE_ALL) + if (p.d_kind == api::CONST_ARRAY) { if (!type.isArray()) { @@ -1701,7 +1701,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // Second phase: apply the arguments to the parse op const Options& opts = d_solver->getExprManager()->getOptions(); // handle special cases - if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) + if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { if (args.size() != 1) { |