mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

#7710

Browse source 
partial fix
This commit is contained in:
Nikolaj Bjorner 2025-07-01 14:23:23 -07:00
parent 97193b4a1d
commit 8de80e666b
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/datatype_decl_plugin.cpp
View file

@ -1070,6 +1070,10 @@ namespace datatype {
plugin().add_ast(con); plugin().add_ast(con);
plugin().m_vectors.push_back(res); plugin().m_vectors.push_back(res);
plugin().m_constructor2accessors.insert(con, res); plugin().m_constructor2accessors.insert(con, res);
if (con->get_arity() == 0)
// no accessors for nullary constructors
return res;
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& d = get_def(datatype); def const& d = get_def(datatype);
for (constructor const* c : d) { for (constructor const* c : d) {
@ -1101,6 +1105,10 @@ namespace datatype {
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& dd = get_def(datatype); def const& dd = get_def(datatype);
symbol r; symbol r;
// This should be fixed for perf.
// Option 1: hash-table in dd that maps to constructors instead of iterating over all constructors.
// initialize the hash-table lazily when dd is large.
// Option 2: initialize all calls to plugin() registration in a single pass.
for (constructor const* c : dd) for (constructor const* c : dd)
if (c->name() == con->get_name()) if (c->name() == con->get_name())
r = c->recognizer(); r = c->recognizer();