mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

add systematic way to combine lia_move results

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-16 10:24:44 -07:00 • committed by Lev Nachmanson
parent 00277ba3cf
commit ff5ae4d1ed
2 changed files with 40 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/math/lp/dioph_eq.cpp
View file

@ -1247,6 +1247,7 @@ namespace lp {
[k](const auto& c) {
return c.var() == k;
});
SASSERT(it != e_row.end());
const mpq& k_coeff_in_e = it->coeff();
bool is_one = k_coeff_in_e.is_one();
SASSERT(is_one || k_coeff_in_e.is_minus_one());
@ -1281,7 +1282,8 @@ namespace lp {
lia_move subs_front_with_S_and_fresh(protected_queue& q, unsigned j) {
process_fixed_in_espace();
auto r = tighten_on_espace(j);
if (r == lia_move::conflict) return lia_move::conflict;
if (r == lia_move::conflict)
return lia_move::conflict;
unsigned k = q.pop_front();
if (!m_espace.has(k))
return lia_move::undef;
@ -1289,16 +1291,11 @@ namespace lp {
SASSERT(can_substitute(k));
lia_move ret;
if (is_substituted_by_fresh(k)) {
if (is_substituted_by_fresh(k))
ret = subs_qfront_by_fresh(k, q, j);
}
else {
else
ret = subs_qfront_by_S(k, q, j);
}
if (ret == lia_move::conflict)
return lia_move::conflict;
if (r == lia_move::continue_with_check) return r;
return ret;
return join(ret, r);
}
lar_term l_term_from_row(unsigned k) const {
@ -1369,11 +1366,9 @@ namespace lp {
lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) {
lia_move r = lia_move::undef;
while (!q.empty()) {
while (!q.empty() && r != lia_move::conflict) {
lia_move ret = subs_front_with_S_and_fresh(q, j);
if (ret == lia_move::conflict) return lia_move::conflict;
if (ret == lia_move::continue_with_check)
r = ret;
r = join(ret, r);
}
return r;
}
@ -1423,15 +1418,10 @@ namespace lp {
);
for (unsigned j : sorted_changed_terms) {
m_terms_to_tighten.remove(j);
auto r0 = tighten_bounds_for_term_column(j);
if (r0 == lia_move::conflict) {
r = r0;
auto ret = tighten_bounds_for_term_column(j);
r = join(ret, r);
if (r == lia_move::conflict)
break;
}
else if (r0 == lia_move::continue_with_check)
r = r0;
else if (r0 == lia_move::branch && r == lia_move::undef)
r = r0;
}
for (unsigned j : processed_terms)
m_terms_to_tighten.remove(j);
@ -1783,14 +1773,13 @@ namespace lp {
lia_move r;
do {
r = rewrite_eqs(f_vector);
if (lra.settings().get_cancel_flag()) {
if (lra.settings().get_cancel_flag())
return lia_move::undef;
}
if (r == lia_move::conflict || r == lia_move::undef) {
if (r == lia_move::conflict || r == lia_move::undef)
break;
}
SASSERT(m_changed_columns.size() == 0);
} while (f_vector.size());
}
while (f_vector.size());
if (r == lia_move::conflict) {
if (m_conflict_index != UINT_MAX) {

25
src/math/lp/lia_move.h
View file

@ -53,6 +53,31 @@ namespace lp {
return "strange";
}
inline lia_move join(lia_move r1, lia_move r2) {
if (r1 == r2)
return r1;
if (r1 == lia_move::undef)
return r2;
if (r2 == lia_move::undef)
return r1;
if (r1 == lia_move::conflict || r2 == lia_move::conflict)
return lia_move::conflict;
if (r1 == lia_move::unsat || r2 == lia_move::unsat)
return lia_move::unsat;
if (r1 == lia_move::cancelled || r2 == lia_move::cancelled)
return lia_move::cancelled;
if (r1 == lia_move::sat || r2 == lia_move::sat)
return lia_move::sat;
if (r1 == lia_move::continue_with_check || r2 == lia_move::continue_with_check)
return lia_move::continue_with_check;
if (r1 == lia_move::cut || r2 == lia_move::cut)
return lia_move::cut;
if (r1 == lia_move::branch || r2 == lia_move::branch)
return lia_move::branch;
UNREACHABLE();
return r1;
}
inline std::ostream& operator<<(std::ostream& out, lia_move const& m) {
return out << lia_move_to_string(m);
}