mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

#5486 - improve type elaboration by epsilon to make common cases parse without type annotation

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-17 16:43:36 -07:00
parent 7f88cfe727
commit 5c9f4dc4d7
4 changed files with 76 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/ast/datatype_decl_plugin.cpp
View file

@ -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);
}

2
src/ast/datatype_decl_plugin.h
View file

@ -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;

55
src/cmd_context/cmd_context.cpp
View file

@ -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);

1
src/cmd_context/cmd_context.h
View file

@ -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);