mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 23:27:53 +00:00
Code Activity

update case split strategy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-12-31 13:40:42 -08:00
parent 9b8558ed92
commit dd0ccce612
2 changed files with 50 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

71
src/math/lp/nla_stellensatz.cpp
View file

@ -162,8 +162,10 @@ namespace nla {
auto sz = src.number_of_vars(); auto sz = src.number_of_vars();
m_lower.reset(); m_lower.reset();
m_upper.reset(); m_upper.reset();
m_split_count.reset();
m_lower.reserve(sz, UINT_MAX); m_lower.reserve(sz, UINT_MAX);
m_upper.reserve(sz, UINT_MAX); m_upper.reserve(sz, UINT_MAX);
m_split_count.reserve(sz, 0);
for (unsigned v = 0; v < sz; ++v) { for (unsigned v = 0; v < sz; ++v) {
m_values.push_back(c().val(v)); m_values.push_back(c().val(v));
if (!m_coi.vars().contains(v)) if (!m_coi.vars().contains(v))
@ -411,14 +413,18 @@ namespace nla {
bool g_strict = other_k == lp::lconstraint_kind::GT; bool g_strict = other_k == lp::lconstraint_kind::GT;
bool f_strict = k == lp::lconstraint_kind::GT; bool f_strict = k == lp::lconstraint_kind::GT;
if (g_p.is_val()) if (g_p.is_val() && f_p.is_val() && g_p.val() == -f_p.val())
ci_a = ci;
else if (g_p.is_val())
ci_a = multiply(ci, pddm.mk_val(g_p.val())); ci_a = multiply(ci, pddm.mk_val(g_p.val()));
else if (!sign_f) else if (!sign_f)
ci_a = multiply(ci, assume(g_p, f_strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE)); ci_a = multiply(ci, assume(g_p, f_strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE));
else else
ci_a = multiply(ci, assume(g_p, f_strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE)); ci_a = multiply(ci, assume(g_p, f_strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE));
if (f_p.is_val()) if (g_p.is_val() && f_p.is_val() && g_p.val() == -f_p.val())
ci_b = other_ci;
else if (f_p.is_val())
ci_b = multiply(other_ci, pddm.mk_val(f_p.val())); ci_b = multiply(other_ci, pddm.mk_val(f_p.val()));
else if (sign_f) else if (sign_f)
ci_b = multiply(other_ci, assume(f_p, g_strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE)); ci_b = multiply(other_ci, assume(f_p, g_strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE));
@ -1234,6 +1240,7 @@ namespace nla {
bool stellensatz::decide() { bool stellensatz::decide() {
rational value; rational value;
lp::lconstraint_kind k; lp::lconstraint_kind k;
lpvar w;
unsigned num_fixed = 0; unsigned num_fixed = 0;
unsigned num_levels = m_level2var.size(); unsigned num_levels = m_level2var.size();
@ -1241,7 +1248,7 @@ namespace nla {
unsigned max_rounds = num_levels * 5; unsigned max_rounds = num_levels * 5;
m_tabu.reset(); m_tabu.reset();
for (unsigned level = 0; level < num_levels && c().reslim().inc() && num_rounds < max_rounds; ++level) { for (unsigned level = 0; level < num_levels && c().reslim().inc() && num_rounds < max_rounds; ++level) {
auto w = m_level2var[level]; w = m_level2var[level];
++num_rounds; ++num_rounds;
lp::constraint_index conflict = repair_variable(w); lp::constraint_index conflict = repair_variable(w);
TRACE(arith, display_constraint(tout << "repair lvl:" << level << " v" << w << ": ", conflict) TRACE(arith, display_constraint(tout << "repair lvl:" << level << " v" << w << ": ", conflict)
@ -1276,14 +1283,15 @@ namespace nla {
++num_fixed; ++num_fixed;
--level; --level;
continue; continue;
} }
// TODO: figure out when to apply splits. // variable wasn't repaired.
// they can be deferred to after repair has finished and some // Repair other variables, and then case split on variables that occur in non-repaired constraints.
// constraint remains false. //
find_split(w, value, k, conflict); }
if (is_fixed(w))
continue;
if (find_split(w, value, k)) {
SASSERT(k == lp::lconstraint_kind::LE || k == lp::lconstraint_kind::GE); SASSERT(k == lp::lconstraint_kind::LE || k == lp::lconstraint_kind::GE);
bool is_upper = k == lp::lconstraint_kind::LE; bool is_upper = k == lp::lconstraint_kind::LE;
SASSERT(!is_upper || !has_lo(w) || lo_val(w) <= value); SASSERT(!is_upper || !has_lo(w) || lo_val(w) <= value);
@ -1303,6 +1311,7 @@ namespace nla {
++c().lp_settings().stats().m_stellensatz.m_num_decisions; ++c().lp_settings().stats().m_stellensatz.m_num_decisions;
return true; return true;
} }
return false; return false;
} }
@ -1688,13 +1697,24 @@ namespace nla {
return c().random(2) == 0 ? sup : inf; return c().random(2) == 0 ? sup : inf;
} }
void stellensatz::find_split(lpvar & v, rational & r, lp::lconstraint_kind & k, lp::constraint_index ci) { bool stellensatz::find_split(lpvar &v, rational &r, lp::lconstraint_kind &k) {
uint_set tried;
bool found = false;
unsigned n = 0; unsigned n = 0;
for (auto w : m_constraints[ci].p.free_vars()) { for (auto ci : m_constraints) {
TRACE(arith, display_var(tout << "v" << w << " is-fixed " << is_fixed(w) << "\n", w) << "\n"); if (!constraint_is_false(ci))
if (is_fixed(w))
continue; continue;
if (c().random(++n) == 0) { auto const &vars = ci.p.free_vars();
for (auto w : vars) {
if (tried.contains(w))
continue;
tried.insert(w);
if (is_fixed(w))
continue;
if (m_split_count[w] > m_config.max_splits_per_var)
continue;
if (c().random(++n) != 0)
continue;
r = m_values[w]; r = m_values[w];
CTRACE(arith, !in_bounds(w), tout << "value not in bounds v" << w << " := " << r << "\n"; CTRACE(arith, !in_bounds(w), tout << "value not in bounds v" << w << " := " << r << "\n";
display(tout);); display(tout););
@ -1707,17 +1727,20 @@ namespace nla {
r = (lo_val(w) + hi_val(w)) / 2; r = (lo_val(w) + hi_val(w)) / 2;
k = lp::lconstraint_kind::GE; k = lp::lconstraint_kind::GE;
} }
else if (!has_lo(w)) else if (!has_lo(w))
k = lp::lconstraint_kind::GE; k = lp::lconstraint_kind::GE;
else if (!has_hi(w)) else if (!has_hi(w))
k = lp::lconstraint_kind::LE; k = lp::lconstraint_kind::LE;
else else
k = c().random(2) == 0 ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE; k = c().random(2) == 0 ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
v = w; v = w;
found = true;
} }
} }
TRACE(arith, tout << "find split v" << v << " " << k << " " << r << "\n"); CTRACE(arith, found, tout << "split v" << v << " " << k << " " << r << "\n");
TRACE(arith, display(tout)); if (found)
++m_split_count[v];
return found;
} }
void stellensatz::set_in_bounds(lpvar v) { void stellensatz::set_in_bounds(lpvar v) {

4
src/math/lp/nla_stellensatz.h
View file

@ -131,6 +131,7 @@ namespace nla {
unsigned max_conflicts = UINT_MAX; unsigned max_conflicts = UINT_MAX;
unsigned max_constraints = UINT_MAX; unsigned max_constraints = UINT_MAX;
unsigned strategy = 0; unsigned strategy = 0;
unsigned max_splits_per_var = 2;
}; };
struct constraint_key { struct constraint_key {
@ -203,6 +204,7 @@ namespace nla {
// //
unsigned_vector m_lower, m_upper; // var -> index into m_bounds unsigned_vector m_lower, m_upper; // var -> index into m_bounds
vector<bound_info> m_bounds; // bound index -> bound meta-data vector<bound_info> m_bounds; // bound index -> bound meta-data
unsigned_vector m_split_count; // var -> number of times variable has been split
unsigned m_prop_qhead = 0; // head into propagation queue unsigned m_prop_qhead = 0; // head into propagation queue
lp::constraint_index m_conflict = lp::null_ci; lp::constraint_index m_conflict = lp::null_ci;
@ -302,7 +304,7 @@ namespace nla {
repair_var_info find_bounds(lpvar v); repair_var_info find_bounds(lpvar v);
unsigned max_level(constraint const &c) const; unsigned max_level(constraint const &c) const;
lp::constraint_index repair_variable(lpvar v); lp::constraint_index repair_variable(lpvar v);
void find_split(lpvar& v, rational& r, lp::lconstraint_kind& k, lp::constraint_index ci); bool find_split(lpvar &v, rational &r, lp::lconstraint_kind &k);
void set_in_bounds(lpvar v); void set_in_bounds(lpvar v);
bool in_bounds(lpvar v) { return in_bounds(v, m_values[v]); } bool in_bounds(lpvar v) { return in_bounds(v, m_values[v]); }
bool in_bounds(lpvar v, rational const &value) const; bool in_bounds(lpvar v, rational const &value) const;