mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-02 05:59:29 +00:00
Code Activity

turn on max of sums transformation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-20 00:55:37 -07:00
parent 3256d1cc8b
commit 9876e85a45
1 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/opt/opt_context.cpp
View file

@ -871,7 +871,7 @@ namespace opt {
m_model_converter = nullptr; m_model_converter = nullptr;
to_fmls(fmls); to_fmls(fmls);
simplify_fmls(fmls, asms); simplify_fmls(fmls, asms);
while (false && asms.empty() && simplify_min_max_of_sums(fmls)) while (asms.empty() && simplify_min_max_of_sums(fmls))
simplify_fmls(fmls, asms); simplify_fmls(fmls, asms);
from_fmls(fmls); from_fmls(fmls);
} }
@ -995,7 +995,7 @@ namespace opt {
bool is_min = !is_max && is_minimize(fml, term, orig_term, index); bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
if (!is_max && !is_min) if (!is_max && !is_min)
return false; return false;
if (!is_uninterp(term)) if (!is_uninterp(term)) // this can be generalized to summations
return false; return false;
ptr_vector<expr> _fmls(fmls.size(), fmls.data()); ptr_vector<expr> _fmls(fmls.size(), fmls.data());
expr_mark mark; expr_mark mark;
@ -1023,9 +1023,9 @@ namespace opt {
return false; return false;
if (!is_zo && !all_of(*to_app(y), is_zero_one)) if (!is_zo && !all_of(*to_app(y), is_zero_one))
return false; return false;
cardinalities.push_back(y); cardinalities.push_back(y);
max_cardinality = std::max(max_cardinality, is_zo ? 1 : to_app(y)->get_num_args()); max_cardinality = std::max(max_cardinality, is_zo ? 1 : to_app(y)->get_num_args());
min_cardinality = std::min(min_cardinality, is_zo ? 1 : to_app(y)->get_num_args()); min_cardinality = std::min(min_cardinality, is_zo ? 1 : to_app(y)->get_num_args());
return true; return true;
}; };
auto is_upper_bound = [&](expr *f) { auto is_upper_bound = [&](expr *f) {
@ -1057,18 +1057,19 @@ namespace opt {
} }
expr_ref_vector new_fmls(m); expr_ref_vector new_fmls(m);
expr_ref_vector soft(m); expr_ref_vector soft(m);
for (unsigned k = 1; k <= max_cardinality; ++k) { for (unsigned k = 1; k <= min_cardinality; ++k) {
auto p_k = m.mk_fresh_const("p", m.mk_bool_sort()); auto p_k = m.mk_fresh_const("p", m.mk_bool_sort());
soft.push_back(m.mk_ite(p_k, a.mk_int(1), a.mk_int(0))); soft.push_back(m.mk_ite(p_k, a.mk_int(1), a.mk_int(0)));
for (auto c : cardinalities) for (auto c : cardinalities)
// p_k => c >= k // p_k => c >= k
if (is_max) if (is_max)
new_fmls.push_back(m.mk_implies(p_k, a.mk_ge(c, a.mk_int(k)))); new_fmls.push_back(m.mk_implies(p_k, a.mk_ge(c, a.mk_int(k))));
// c >= k => p_k
else else
new_fmls.push_back(m.mk_implies(a.mk_ge(c, a.mk_int(k)), p_k)); new_fmls.push_back(m.mk_implies(a.mk_ge(c, a.mk_int(k)), p_k));
} }
// min x | x >= c, min sum p_k : c >= k => p_k // min x | x >= c_i, min sum p_k : /\_i c_i >= k => p_k
// max x | x <= c, max sum p_k : p_k => c >= k // max x | x <= c_i, max sum p_k : /\_i p_k => c_i >= k
app_ref sum(a.mk_add(soft.size(), soft.data()), m); app_ref sum(a.mk_add(soft.size(), soft.data()), m);
if (is_max) if (is_max)
new_fmls.push_back(mk_maximize(index, sum)); new_fmls.push_back(mk_maximize(index, sum));