mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Merge branch 'master' into copilot/remove-new-settings

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-07 12:51:06 -07:00 • committed by GitHub
commit 0a77ac00f5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 9 additions and 3 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);
t.push(push_back_vector(m_assertions));
u.collect_type_vars(e, inst.m_tvs);
auto* init = alloc(substitution, m);
inst.m_subst = alloc(substitutions);
inst.m_subst->insert(alloc(substitution, m));
inst.m_subst->insert(init);
m_instances.insert(e, inst);
t.push(new_obj_trail(init));
t.push(new_obj_trail(inst.m_subst));
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).
sort* get_ho_sort(ptr_vector<sort> const& domain, sort* 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);
m_pinned_sorts.push_back(s);
}
return s;
}
@ -1369,6 +1371,7 @@ class tptp_parser {
sort* arg_sort = arg->get_sort();
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);
m_pinned_sorts.push_back(arr_sort);
e = coerce_arg(e, arr_sort);
} else {
// 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)
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);
m_pinned_sorts.push_back(arr_sort);
e = coerce_arg(e, arr_sort);
} else {
// Array but domain may not match arg sort — coerce arg

2
src/math/lp/lp_params_helper.pyg
View file

@ -14,6 +14,6 @@ def_module_params(module_name='lp',
('lcube', BOOL, True, 'use the largest cube test for integer feasibility'),
('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
))