From 5c9f4dc4d78187f582cee37ee5682536c92e9276 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 72d39290e..b528bad82 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<constructor> plugin::get_constructors(symbol const& s) const {
+ ptr_vector<constructor> result;
+ for (auto [k, d] : m_defs)
+ for (auto* c : *d)
+ if (c->name() == s)
+ result.push_back(c);
+ return result;
+ }
+
+ ptr_vector<accessor> plugin::get_accessors(symbol const& s) const {
+ ptr_vector<accessor> 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 90d49e449..68e7e3c9a 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<constructor> get_constructors(symbol const& s) const;
+ ptr_vector<accessor> 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 2133a1c00..bd76220b4 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<sort> 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 4b669e559..4f9d80a8d 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -425,6 +425,7 @@ public:
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);