diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-22 00:28:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-22 00:28:22 -0500 |
commit | f66cbabd6b67462ebbf9bbba5d3ccfb08b69ff25 (patch) | |
tree | 56d541e543a812e81cc1a7e7c3d248541460716a /src/parser/smt2/smt2.cpp | |
parent | 636012f559ff6df9f3ee774baba1b0805f4269c8 (diff) |
Minimal fixing version for tuple update parsing (#7228)
This takes the essential changes from #7218 so that the current ANTLR issues are avoided.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 42 |
1 files changed, 22 insertions, 20 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2fd4a5596..40716d908 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators() { Parser::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); + addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); } } @@ -382,25 +383,15 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, return api::Term(); } -api::Op Smt2::mkIndexedOp(const std::string& name, - const std::vector<uint64_t>& numerals) +api::Kind Smt2::getIndexedOpKind(const std::string& name) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) { - api::Kind k = (*kIt).second; - if (numerals.size() == 1) - { - return d_solver->mkOp(k, numerals[0]); - } - else if (numerals.size() == 2) - { - return d_solver->mkOp(k, numerals[0], numerals[1]); - } + return (*kIt).second; } - parseError(std::string("Unknown indexed function `") + name + "'"); - return api::Op(); + return api::UNDEFINED_KIND; } api::Term Smt2::bindDefineFunRec( @@ -1037,22 +1028,24 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return store all " << ret << std::endl; return ret; } - else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) + else if ((p.d_kind == api::APPLY_SELECTOR || p.d_kind == api::APPLY_UPDATER) + && !p.d_expr.isNull()) { // tuple selector case if (!p.d_expr.isUInt64Value()) { - parseError("index of tupSel is larger than size of uint64_t"); + parseError( + "index of tuple select or update is larger than size of uint64_t"); } uint64_t n = p.d_expr.getUInt64Value(); - if (args.size() != 1) + if (args.size() != (p.d_kind == api::APPLY_SELECTOR ? 1 : 2)) { - parseError("tupSel should only be applied to one tuple argument"); + parseError("wrong number of arguments for tuple select or update"); } api::Sort t = args[0].getSort(); if (!t.isTuple()) { - parseError("tupSel applied to non-tuple"); + parseError("tuple select or update applied to non-tuple"); } size_t length = t.getTupleLength(); if (n >= length) @@ -1062,8 +1055,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError(ss.str()); } const api::Datatype& dt = t.getDatatype(); - api::Term ret = d_solver->mkTerm( - api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); + api::Term ret; + if (p.d_kind == api::APPLY_SELECTOR) + { + ret = d_solver->mkTerm( + api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); + } + else + { + ret = d_solver->mkTerm( + api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]); + } Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } |