mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

prevent re-declaration of enumeration sort names

Browse source 
preventing redeclaration of all ADT cases is not part of this update.
This commit is contained in:
Nikolaj Bjorner 2022-11-19 19:46:34 +07:00
parent c3c45f495a
commit 86f3702403
3 changed files with 28 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_datatype.cpp
View file

@ -102,6 +102,13 @@ extern "C" {
sort* e;
ptr_vector<constructor_decl> constrs;
symbol sname = to_symbol(name);
if (mk_c(c)->get_dt_plugin()->is_declared(sname)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
}
for (unsigned i = 0; i < n; ++i) {
symbol e_name(to_symbol(enum_names[i]));
std::string recognizer_s("is_");
@ -112,8 +119,9 @@ extern "C" {
}
{
datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, n, constrs.data());
datatype_decl * dt = mk_datatype_decl(dt_util, sname, 0, nullptr, n, constrs.data());
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts);
del_datatype_decl(dt);

31
src/ast/datatype_decl_plugin.cpp
View file

@ -832,6 +832,10 @@ namespace datatype {
bool util::is_declared(sort* s) const {
return plugin().is_declared(s);
}
bool util::is_declared(symbol const& n) const {
return plugin().is_declared(n);
}
void util::compute_datatype_size_functions(svector<symbol> const& names) {
map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
@ -1087,11 +1091,9 @@ namespace datatype {
sort * datatype = con->get_range();
def const& dd = get_def(datatype);
symbol r;
for (constructor const* c : dd) {
if (c->name() == con->get_name()) {
r = c->recognizer();
}
}
for (constructor const* c : dd)
if (c->name() == con->get_name())
r = c->recognizer();
parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d);
@ -1142,17 +1144,15 @@ namespace datatype {
}
bool util::is_enum_sort(sort* s) {
if (!is_datatype(s)) {
return false;
}
if (!is_datatype(s))
return false;
bool r = false;
if (m_is_enum.find(s, r))
return r;
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
r = true;
for (unsigned i = 0; r && i < cnstrs.size(); ++i) {
r = cnstrs[i]->get_arity() == 0;
}
for (unsigned i = 0; r && i < cnstrs.size(); ++i)
r = cnstrs[i]->get_arity() == 0;
m_is_enum.insert(s, r);
m_asts.push_back(s);
return r;
@ -1284,11 +1284,14 @@ namespace datatype {
unsigned idx = 0;
def const& d = get_def(f->get_range());
for (constructor* c : d) {
if (c->name() == f->get_name()) {
return idx;
}
if (c->name() == f->get_name())
return idx;
++idx;
}
IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n");
for (constructor* c : d)
IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n");
SASSERT(false);
UNREACHABLE();
return 0;
}

2
src/ast/datatype_decl_plugin.h
View file

@ -253,6 +253,7 @@ namespace datatype {
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)); }
bool is_declared(symbol const& n) const { return m_defs.contains(n); }
unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
util & u() const;
@ -375,6 +376,7 @@ namespace datatype {
bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f);
void reset();
bool is_declared(sort* s) const;
bool is_declared(symbol const& n) const;
void display_datatype(sort *s, std::ostream& strm);
bool is_fully_interp(sort * s) const;
sort_ref_vector datatype_params(sort * s) const;