From 5c9f4dc4d78187f582cee37ee5682536c92e9276 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Aug 2021 16:43:36 -0700 Subject: [PATCH] #5486 - improve type elaboration by epsilon to make common cases parse without type annotation --- src/ast/datatype_decl_plugin.cpp | 22 +++++++++++-- src/ast/datatype_decl_plugin.h | 2 ++ src/cmd_context/cmd_context.cpp | 55 ++++++++++++++++++++++++++++++-- src/cmd_context/cmd_context.h | 1 + 4 files changed, 76 insertions(+), 4 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 72d39290e3d..b528bad82dd 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -367,6 +367,25 @@ namespace datatype { return m.mk_func_decl(name, arity, domain, range, info); } + ptr_vector plugin::get_constructors(symbol const& s) const { + ptr_vector result; + for (auto [k, d] : m_defs) + for (auto* c : *d) + if (c->name() == s) + result.push_back(c); + return result; + } + + ptr_vector plugin::get_accessors(symbol const& s) const { + ptr_vector result; + for (auto [k, d] : m_defs) + for (auto* c : *d) + for (auto* a : *c) + if (a->name() == s) + result.push_back(a); + return result; + } + func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) { ast_manager& m = *m_manager; @@ -556,9 +575,8 @@ namespace datatype { void plugin::remove(symbol const& s) { def* d = nullptr; - if (m_defs.find(s, d)) { + if (m_defs.find(s, d)) dealloc(d); - } m_defs.remove(s); } diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 90d49e44906..68e7e3c9abe 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -248,6 +248,8 @@ namespace datatype { def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } def& get_def(symbol const& s) { return *(m_defs[s]); } + ptr_vector get_constructors(symbol const& s) const; + ptr_vector get_accessors(symbol const& s) const; bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; } util & u() const; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2133a1c005a..bd76220b4bc 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1194,6 +1194,55 @@ bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * c return false; } +bool cmd_context::try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const { + sort_ref_vector binding(m()); + auto match = [&](sort* s, sort* ps) { + if (ps == s) + return true; + if (m().is_uninterp(ps) && ps->get_name().is_numerical()) { + int index = ps->get_name().get_num(); + binding.reserve(index + 1); + binding[index] = s; + return true; + } + // Other matching is TBD + return false; + }; + datatype::util dt(m()); + func_decl_ref fn(m()); + for (auto* c : dt.plugin().get_constructors(s)) { + if (c->accessors().size() != num_args) + continue; + binding.reset(); + unsigned i = 0; + for (auto* a : *c) + if (!match(args[i++]->get_sort(), a->range())) + goto match_failure; + if (binding.size() != c->get_def().params().size()) + goto match_failure; + for (auto* b : binding) + if (!b) + goto match_failure; + + fn = c->instantiate(binding); + r = m().mk_app(fn, num_args, args); + return true; + match_failure: + ; + } + if (num_args != 1) + return false; + + for (auto* a : dt.plugin().get_accessors(s)) { + fn = a->instantiate(args[0]->get_sort()); + r = m().mk_app(fn, num_args, args); + return true; + } + + return false; +} + + void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, expr_ref & result) const { @@ -1206,7 +1255,9 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg return; if (try_mk_builtin_app(s, num_args, args, num_indices, indices, range, result)) return; - + if (!range && try_mk_pdecl_app(s, num_args, args, num_indices, indices, result)) + return; + std::ostringstream buffer; buffer << "unknown constant " << s; if (num_args > 0) { @@ -1899,7 +1950,7 @@ void cmd_context::complete_model(model_ref& md) const { SASSERT(!v->has_var_params()); IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; ); ptr_vector param_sorts(v->get_num_params(), m().mk_bool_sort()); - sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.data()); + sort * srt = v->instantiate(pm(), param_sorts.size(), param_sorts.data()); if (!md->has_uninterpreted_sort(srt)) { expr * singleton = m().get_some_value(srt); md->register_usort(srt, 1, &singleton); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 4b669e5596f..4f9d80a8d6e 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -425,6 +425,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_ bool try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, func_decls& fs, expr_ref & result) const; + bool try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const; void erase_cmd(symbol const & s); void erase_func_decl(symbol const & s); void erase_func_decl(symbol const & s, func_decl * f);