Non-linear performance of declare_datatype in CLI #7709
Description
I have a simple file with this single command:
(declare-datatype Element ( (a1) (a2) (a3) ... ))
It takes 4 seconds to run it when the datatype has 50.000 constructors and 14 seconds for 100.000 constructors, using the Z3 command line interface and Z3 v.4.15.2.
By contrast, the creation of the datatype through the (Rust) API only takes 300 ms for 100.000 constructors.
I can try to create a PR if I get some hints on what the root cause is.
#[macro_use]
extern crate timeit;
use z3::*;
fn main() {
timeit!({
let cfg = Config::new();
let ctx = Context::new(&cfg);
let mut element = DatatypeBuilder::new(&ctx, "Element");
for i in 1..100000 {
element = element.variant(format!("a{i}").as_str(), vec![]);
}
element.finish();
})
}