mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

reduce leaks for sorts

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-07 11:30:33 -07:00
parent ff7e22c055
commit 334f4fa32b
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/polymorphism_inst.cpp
View file

@ -57,9 +57,11 @@ namespace polymorphism {
m_assertions.push_back(e); m_assertions.push_back(e);
t.push(push_back_vector(m_assertions)); t.push(push_back_vector(m_assertions));
u.collect_type_vars(e, inst.m_tvs); u.collect_type_vars(e, inst.m_tvs);
auto* init = alloc(substitution, m);
inst.m_subst = alloc(substitutions); inst.m_subst = alloc(substitutions);
inst.m_subst->insert(alloc(substitution, m)); inst.m_subst->insert(init);
m_instances.insert(e, inst); m_instances.insert(e, inst);
t.push(new_obj_trail(init));
t.push(new_obj_trail(inst.m_subst)); t.push(new_obj_trail(inst.m_subst));
t.push(insert_map(m_instances, e)); t.push(insert_map(m_instances, e));
} }

6
src/cmd_context/tptp_frontend.cpp
View file

@ -553,8 +553,10 @@ class tptp_parser {
// Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried). // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried).
sort* get_ho_sort(ptr_vector<sort> const& domain, sort* range) { sort* get_ho_sort(ptr_vector<sort> const& domain, sort* range) {
sort* s = range; sort* s = range;
for (int i = (int)domain.size() - 1; i >= 0; --i) for (int i = (int)domain.size() - 1; i >= 0; --i) {
s = m_array.mk_array_sort(domain[i], s); s = m_array.mk_array_sort(domain[i], s);
m_pinned_sorts.push_back(s);
}
return s; return s;
} }
@ -1369,6 +1371,7 @@ class tptp_parser {
sort* arg_sort = arg->get_sort(); sort* arg_sort = arg->get_sort();
sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ;
sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort);
m_pinned_sorts.push_back(arr_sort);
e = coerce_arg(e, arr_sort); e = coerce_arg(e, arr_sort);
} else { } else {
// Array but domain may not match arg sort — coerce arg // Array but domain may not match arg sort — coerce arg
@ -2217,6 +2220,7 @@ class tptp_parser {
// If arg is Bool-sorted, result is likely Bool too (modal/connective application) // If arg is Bool-sorted, result is likely Bool too (modal/connective application)
sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ;
sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort);
m_pinned_sorts.push_back(arr_sort);
e = coerce_arg(e, arr_sort); e = coerce_arg(e, arr_sort);
} else { } else {
// Array but domain may not match arg sort — coerce arg // Array but domain may not match arg sort — coerce arg