mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-10 16:01:11 +00:00
Code Activity

manual edits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-08 14:55:09 -07:00
parent d0d79aa13c
commit 69430bd164
5 changed files with 57 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lar_solver.cpp
View file

@ -1338,6 +1338,10 @@ namespace lp {
return false;
}
}
bool lar_solver::is_int_feasible() const {
return is_feasible() && model_is_int_feasible();
}
numeric_pair<mpq> lar_solver::get_basic_var_value_from_row(unsigned i) {
numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();

1
src/math/lp/lar_solver.h
View file

@ -185,6 +185,7 @@ public:
std::function<std::string(lpvar)> var_str = [](lpvar j) { return std::string("j") + T_to_string(j); }) const;
// this function just looks at the status
bool is_feasible() const;
bool is_int_feasible() const;
const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_int() const;
const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_real() const;

28
src/math/lp/monomial_bounds.cpp
View file

@ -1138,18 +1138,8 @@ namespace nla {
m_bounds_optimization_enabled = false;
auto& lra = c().lra;
if (!lra.is_feasible())
if (!lra.is_int_feasible())
return false;
SASSERT(lra.model_is_int_feasible());
auto check_model = [&]() {
SASSERT(lra.is_feasible());
SASSERT(lra.model_is_int_feasible());
};
auto status = lra.find_feasible_solution();
SASSERT(status != lp::lp_status::INFEASIBLE);
if (status == lp::lp_status::INFEASIBLE)
return false;
check_model();
// Gather the candidate columns: every non-fixed leaf variable that
// participates in a monomial (mirrors solver=2's max_min_nl_vars).
@ -1186,12 +1176,10 @@ namespace nla {
struct improved_bound { lpvar j; lp::lconstraint_kind kind; rational bound; u_dependency* dep; };
vector<improved_bound> improvements;
for (lpvar j : cands) {
if (!lra.is_feasible())
break;
for (bool is_lower : { true, false }) {
rational bound;
u_dependency* dep = improve_bound(j, is_lower, bound);
check_model();
SASSERT(lra.is_int_feasible());
if (!dep)
continue;
auto kind = is_lower ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
@ -1199,19 +1187,11 @@ namespace nla {
}
}
if (improvements.empty()) {
// The exploratory simplex walk in improve_bound/mm_optimize mutated the
// LP model even though no bound was tightened. Restore a clean feasible
// model so downstream lemma passes see a feasible integral assignment.
lra.find_feasible_solution();
check_model();
return true;
}
for (auto const& ib : improvements)
lra.update_column_type_and_bound(ib.j, ib.kind, ib.bound, ib.dep);
lra.find_feasible_solution();
check_model();
SASSERT(lra.is_int_feasible());
lra.get_rid_of_inf_eps();
return true;
}

91
src/math/lp/nla_core.cpp
View file

@ -642,8 +642,7 @@ void core::init_to_refine() {
// violates it. optimize_nl_bounds() re-solves the LP and re-introduces
// delta components, so they are dropped here rather than only on entry to
// check().
if (lra.is_feasible())
lra.get_rid_of_inf_eps();
SASSERT(lra.is_feasible());
m_to_refine.reset();
unsigned r = random(), sz = m_emons.number_of_monics();
for (unsigned k = 0; k < sz; ++k) {
@ -1168,18 +1167,18 @@ bool core::to_refine_is_correct() const {
return true;
}
bool core::patch_monomial(lpvar j) {
m_patched_monic =& (emon(j));
void core::patch_monomial(lpvar j) {
m_patched_monic = &(emon(j));
m_patched_var = j;
TRACE(nla_solver, tout << "m = "; print_monic(*m_patched_monic, tout) << "\n";);
rational v = mul_val(*m_patched_monic);
if (val(j) == v) {
erase_from_to_refine(j);
return false;
return;
}
if (!var_breaks_correct_monic(j) && try_to_patch(v)) {
SASSERT(to_refine_is_correct());
return true;
return;
}
// We could not patch j, now we try patching the factor variables.
@ -1191,11 +1190,11 @@ bool core::patch_monomial(lpvar j) {
m_patched_var = (*m_patched_monic).vars()[0];
if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) {
TRACE(nla_solver, tout << "patched square\n";);
return true;
return;
}
}
TRACE(nla_solver, tout << " cannot patch\n";);
return false;
return;
}
// We have v != abc, but we need to have v = abc.
@ -1212,14 +1211,14 @@ bool core::patch_monomial(lpvar j) {
TRACE(nla_solver, tout << "patched " << m_patched_var << "\n";);
SASSERT(mul_val((*m_patched_monic)) == val(j));
erase_from_to_refine(j);
return true;
return;
}
}
}
return false;
return;
}
bool core::patch_monomials_on_to_refine() {
void core::patch_monomials_on_to_refine() {
// the rest of the function might change m_to_refine, so have to copy
unsigned_vector to_refine;
for (unsigned j : m_to_refine)
@ -1228,18 +1227,17 @@ bool core::patch_monomials_on_to_refine() {
unsigned sz = to_refine.size();
unsigned start = random();
bool patched = false;
for (unsigned i = 0; i < sz && !m_to_refine.empty(); ++i)
patched |= patch_monomial(to_refine[(start + i) % sz]);
patch_monomial(to_refine[(start + i) % sz]);
TRACE(nla_solver, tout << "sz = " << sz << ", m_to_refine = " << m_to_refine.size() <<
(sz > m_to_refine.size()? " less" : " same" ) << "\n";);
return patched;
}
bool core::patch_monomials() {
void core::patch_monomials() {
m_cautious_patching = true;
return patch_monomials_on_to_refine();
patch_monomials_on_to_refine();
}
/**
@ -1299,44 +1297,38 @@ void core::add_bounds() {
lbool core::check(unsigned level) {
lp_settings().stats().m_nla_calls++;
TRACE(nla_solver, tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
lra.get_rid_of_inf_eps();
if (!(lra.get_status() == lp::lp_status::OPTIMAL ||
lra.get_status() == lp::lp_status::FEASIBLE)) {
if (!lra.is_feasible()) {
TRACE(nla_solver, tout << "unknown because of the lra.m_status = " << lra.get_status() << "\n";);
return l_undef;
}
if (!lra.is_int_feasible())
return l_false;
lra.get_rid_of_inf_eps();
set_use_nra_model(false);
init_to_refine();
if (m_to_refine.empty())
return l_true;
bool patched = patch_monomials();
if (m_to_refine.empty()) {
SASSERT(patched);
patch_monomials();
if (m_to_refine.empty())
return l_false;
}
init_search();
if (m_monomial_bounds.optimize_nl_bounds()) {
init_to_refine();
if (m_to_refine.empty())
return l_false;
}
m_monomial_bounds.optimize_nl_bounds();
SASSERT(lra.is_int_feasible());
init_to_refine();
if (m_to_refine.empty())
return l_false;
lbool ret = l_undef;
bool run_grobner = need_run_grobner();
bool run_horner = need_run_horner();
bool run_bounds = params().arith_nl_branching();
auto no_effect = [&]() { return ret == l_undef && !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
if (no_effect())
m_monomial_bounds.generate_lemmas();
if (no_effect() && refine_pseudo_linear())
return l_false;
if (no_effect()) {
unsigned old_idx = m_strategy_idx;
trail().push(value_trail(m_strategy_idx));
@ -1345,20 +1337,27 @@ lbool core::check(unsigned level) {
case 0:
propagate();
break;
case 1:
if (run_horner)
m_horner.horner_lemmas();
case 1:
m_monomial_bounds.generate_lemmas();
break;
case 2:
if (run_grobner)
m_grobner();
if (refine_pseudo_linear())
return l_false;
break;
case 3:
if (run_bounds)
if (need_run_horner())
m_horner.horner_lemmas();
break;
case 4:
if (need_run_grobner())
m_grobner();
break;
case 5:
if (params().arith_nl_branching())
add_bounds();
break;
}
m_strategy_idx = (m_strategy_idx + 1) % 4;
m_strategy_idx = (m_strategy_idx + 1) % 6;
if (lp_settings().get_cancel_flag())
return l_undef;
if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)

6
src/math/lp/nla_core.h
View file

@ -431,9 +431,9 @@ public:
bool is_nl_var(lpvar) const;
bool is_used_in_monic(lpvar) const;
bool patch_monomials();
bool patch_monomials_on_to_refine();
bool patch_monomial(lpvar);
void patch_monomials();
void patch_monomials_on_to_refine();
void patch_monomial(lpvar);
bool var_breaks_correct_monic(lpvar) const;
bool var_breaks_correct_monic_as_factor(lpvar, const monic&) const;
void update_to_refine_of_var(lpvar j);