mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix instantiations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9f5bd2feda
commit
d05d3bac4f
|
@ -604,8 +604,30 @@ struct datatype_decl_buffer {
|
|||
|
||||
#ifdef DATATYPE_V2
|
||||
sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
|
||||
UNREACHABLE();
|
||||
return 0;
|
||||
// TBD: copied
|
||||
SASSERT(n == m_num_params);
|
||||
sort * r = find(s);
|
||||
if (r)
|
||||
return r;
|
||||
buffer<parameter> ps;
|
||||
ps.push_back(parameter(m_name));
|
||||
for (unsigned i = 0; i < n; i++)
|
||||
ps.push_back(parameter(s[i]));
|
||||
datatype_util util(m.m());
|
||||
r = m.m().mk_sort(util.get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr());
|
||||
cache(m, s, r);
|
||||
m.save_info(r, this, n, s);
|
||||
if (m_num_params > 0 && util.is_declared(r)) {
|
||||
bool has_typevar = false;
|
||||
// crude check ..
|
||||
for (unsigned i = 0; !has_typevar && i < n; ++i) {
|
||||
has_typevar = s[i]->get_name().is_numerical();
|
||||
}
|
||||
if (!has_typevar) {
|
||||
m.notify_new_dt(r, this);
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
#else
|
||||
sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
|
||||
|
|
|
@ -917,7 +917,10 @@ namespace smt2 {
|
|||
pdatatype_decl * d = new_dt_decls[i];
|
||||
symbol duplicated;
|
||||
check_duplicate(d, line, pos);
|
||||
m_ctx.insert(d);
|
||||
if (!is_smt2_6) {
|
||||
// datatypes are inserted up front in SMT2.6 mode, so no need to re-insert them.
|
||||
m_ctx.insert(d);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n";
|
||||
|
|
Loading…
Reference in a new issue