mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

solving regressions/smt2/b1.smt2

Browse source
This commit is contained in:
Lev Nachmanson 2024-11-17 14:32:04 -08:00 committed by Lev Nachmanson
parent 71c433908c
commit e4f3b5753f
3 changed files with 91 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -238,7 +238,7 @@ namespace lp {
unsigned m_max_number_of_iterations = 1000; unsigned m_max_number_of_iterations = 1000;
unsigned m_number_of_iterations; unsigned m_number_of_iterations;
struct branch { struct branch {
unsigned m_j; unsigned m_j = UINT_MAX;
mpq m_rs; mpq m_rs;
// if m_left is true, then the branch is interpreted // if m_left is true, then the branch is interpreted
// as x[j] <= m_rs // as x[j] <= m_rs
@ -275,8 +275,6 @@ namespace lp {
std_vector<variable_branch_stats> m_branch_stats; std_vector<variable_branch_stats> m_branch_stats;
std_vector<branch> m_branch_stack; std_vector<branch> m_branch_stack;
std_vector<unsigned> m_added_fixed;
std_vector<unsigned> m_added_fixed_sizes;
std_vector<constraint_index> m_explanation_of_branches; std_vector<constraint_index> m_explanation_of_branches;
public: public:
@ -712,7 +710,7 @@ namespace lp {
} }
} }
// returns true if there is a change in the bounds // returns true only on a conflict.
// m_indexed_work_vector contains the coefficients of the term // m_indexed_work_vector contains the coefficients of the term
// m_c contains the constant term // m_c contains the constant term
// m_tmp_l is the linear combination of the equations that removs the // m_tmp_l is the linear combination of the equations that removs the
@ -737,6 +735,7 @@ namespace lp {
return false; return false;
} }
// returns true only on a conflict
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper, bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper,
u_dependency* prev_dep) { u_dependency* prev_dep) {
// ub = (upper_bound(j) - m_c)/g. // ub = (upper_bound(j) - m_c)/g.
@ -768,12 +767,12 @@ namespace lp {
print_lar_term_L(lra.get_term(j), tout) << "\ndep:"; print_lar_term_L(lra.get_term(j), tout) << "\ndep:";
print_dep(tout, dep) << std::endl;); print_dep(tout, dep) << std::endl;);
lra.update_column_type_and_bound(j, kind, bound, dep); lra.update_column_type_and_bound(j, kind, bound, dep);
int st = (int)lra.find_feasible_solution(); lp_status st = lra.find_feasible_solution();
if (st >= (int)lp::lp_status::FEASIBLE) { if ((int)st >= (int)lp::lp_status::FEASIBLE) {
lra.get_infeasibility_explanation(m_infeas_explanation); return false;
return true;
} }
return false; lra.get_infeasibility_explanation(m_infeas_explanation);
return true;
} }
u_dependency* explain_fixed_in_meta_term(const lar_term& t) { u_dependency* explain_fixed_in_meta_term(const lar_term& t) {
@ -845,30 +844,21 @@ namespace lp {
} }
} }
void undo_fixed(unsigned j) { // returns true if the left and the right branches were explored
NOT_IMPLEMENTED_YET(); bool undo_last_branch() {
}
void undo_last_branch() {
unsigned h = m_branch_stack.size() - 1; unsigned h = m_branch_stack.size() - 1;
unsigned n_of_fixed_before = m_added_fixed_sizes[h];
while (m_added_fixed.size() > n_of_fixed_before) {
unsigned j = m_added_fixed.back();
m_added_fixed.pop_back();
undo_fixed(j);
}
if (m_branch_stack.back().m_fully_explored) { if (m_branch_stack.back().m_fully_explored) {
TRACE("dio_br", tout << "pop fully explored" << std::endl;); TRACE("dio_br", tout << "pop fully explored, m_branch_stack.size():" << m_branch_stack.size() << std::endl;);
m_branch_stack.pop_back(); m_branch_stack.pop_back();
m_added_fixed_sizes.pop_back(); return true;
NOT_IMPLEMENTED_YET();
} else { // exploring the other side of the branch
TRACE("dio_br", tout << "flipped branch" << std::endl;);
m_branch_stack.back().flip();
} }
// exploring the other side of the branch
TRACE("dio_br", tout << "flipped branch" << std::endl;);
m_branch_stack.back().flip();
return false;
} }
lia_move check_fixing(unsigned j) { lia_move check_fixing(unsigned j) const {
// do not change entry here // do not change entry here
unsigned ei = m_k2s[j]; // entry index unsigned ei = m_k2s[j]; // entry index
mpq g = mpq(0); // gcd mpq g = mpq(0); // gcd
@ -889,7 +879,6 @@ namespace lp {
if (g.is_one()) return lia_move::undef; if (g.is_one()) return lia_move::undef;
} }
if (!(c/g).is_int()) { if (!(c/g).is_int()) {
m_conflict_index = ei;
return lia_move::conflict; return lia_move::conflict;
} }
return lia_move::undef; return lia_move::undef;
@ -897,27 +886,35 @@ namespace lp {
// here j is a local variable // here j is a local variable
lia_move fix_var(unsigned j) { lia_move fix_var(unsigned j) {
SASSERT(is_fixed(local_to_lar_solver(j))); SASSERT(is_fixed(local_to_lar_solver(j)));
m_added_fixed.push_back(j);
/* /*
The only conflict we can get it is when j is substituted, and the entry m_k2s[j], the entry defining the substitution We only can get a conflict when j is substituted, and the entry m_k2s[j], the entry defining the substitution becomes infeaseable, that is the gcd of the monomial coeffitients does not dive the free coefficient. In other cases the gcd of the monomials will remain to be 1.
becomes infeaseable, that is the gcd of the monomial coeffitients does not dived the free coefficients.
*/ */
if (can_substitute(j)) { if (can_substitute(j)) {
TRACE("dio_br", TRACE("dio_br",
tout << "fixed j:" << j <<", was substited by "; print_entry(m_k2s[j], tout);); tout << "fixed j:" << j <<", was substited by "; print_entry(m_k2s[j], tout););
if (check_fixing(j) == lia_move::conflict) if (check_fixing(j) == lia_move::conflict) {
m_conflict_index = m_k2s[j];
return lia_move::conflict; return lia_move::conflict;
}
} }
NOT_IMPLEMENTED_YET(); return lia_move::undef;
} }
void undo_branching() { void undo_branching() {
NOT_IMPLEMENTED_YET(); while (m_lra_level --) {
lra.pop();
}
lra.find_feasible_solution();
SASSERT(lra.is_feasible());
} }
// Returns true if a branch is created, and false if not.
void push_branch() { // The latter case can happen if we have a sat.
m_branch_stack.push_back(create_branch()); bool push_branch() {
m_added_fixed_sizes.push_back(m_added_fixed.size()); branch br = create_branch();
if (br.m_j == UINT_MAX)
return false;
m_branch_stack.push_back(br);
return true;
} }
lia_move add_var_bound_for_branch(const branch* b) { lia_move add_var_bound_for_branch(const branch* b) {
@ -933,31 +930,46 @@ namespace lp {
return lia_move::undef; return lia_move::undef;
} }
unsigned n_deb_lra_level = 0; unsigned m_lra_level = 0;
void lra_push() { void lra_push() {
n_deb_lra_level++; m_lra_level++;
lra.push(); lra.push();
SASSERT(n_deb_lra_level == m_branch_stack.size()); SASSERT(m_lra_level == m_branch_stack.size());
} }
void lra_pop() { void lra_pop() {
n_deb_lra_level--; m_lra_level--;
lra.pop(); lra.pop();
lra.find_feasible_solution();
SASSERT(lra.is_feasible());
} }
lia_move process_undef() { lia_move process_undef() {
m_explanation_of_branches.clear(); m_explanation_of_branches.clear();
branch* b; branch* b;
bool need_create_branch = true; bool need_create_branch = true;
while (true) { m_number_of_iterations = 0;
while (++m_number_of_iterations < m_max_number_of_iterations) {
if (need_create_branch) { if (need_create_branch) {
push_branch(); if (!push_branch()) {
undo_branching();
return lia_move::sat;
}
need_create_branch = false; need_create_branch = false;
b = &m_branch_stack.back(); b = &m_branch_stack.back();
} }
lra_push(); // exploring a new branch lra_push(); // exploring a new branch
if (add_var_bound_for_branch(b) == lia_move::conflict) if (add_var_bound_for_branch(b) == lia_move::conflict) {
return lia_move::conflict; collect_evidence();
if (m_branch_stack.size() == 0)
return lia_move::conflict;
TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;
tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation););
if (undo_last_branch())
need_create_branch = true;
lra_pop();
continue;
}
int st = static_cast<int>(lra.find_feasible_solution()); int st = static_cast<int>(lra.find_feasible_solution());
if (st >= static_cast<int>(lp_status::FEASIBLE)) { if (st >= static_cast<int>(lp_status::FEASIBLE)) {
// have a feasible solution // have a feasible solution
@ -976,10 +988,12 @@ namespace lp {
return lia_move::conflict; return lia_move::conflict;
TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl; TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;
tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation);); tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation););
undo_last_branch(); if (undo_last_branch())
need_create_branch = true;
lra_pop(); lra_pop();
} }
} }
undo_branching();
return lia_move::undef; return lia_move::undef;
} }
@ -1011,7 +1025,7 @@ namespace lp {
} }
branch create_branch() { branch create_branch() {
unsigned bj; unsigned bj = UINT_MAX;
double score = std::numeric_limits<double>::infinity(); double score = std::numeric_limits<double>::infinity();
// looking for the minimal score // looking for the minimal score
unsigned n = 0; unsigned n = 0;
@ -1026,6 +1040,19 @@ namespace lp {
} }
} }
branch br; branch br;
if (bj == UINT_MAX) { // it a the case when we cannot create a branch
SASSERT(lra.is_feasible() &&
[&]() {
for (unsigned j = 0; j < lra.column_count(); ++j) {
if (lia.column_is_int_inf(j)) {
return false;
}
}
return true;
}());
return br; // to signal that we have no ii variables
}
br.m_j = bj; br.m_j = bj;
br.m_left = (lra.settings().random_next() % 2 == 0); br.m_left = (lra.settings().random_next() % 2 == 0);
br.m_rs = floor(lra.get_column_value(bj).x); br.m_rs = floor(lra.get_column_value(bj).x);
@ -1037,26 +1064,16 @@ namespace lp {
public: public:
lia_move check() { lia_move check() {
lra.settings().stats().m_dio_calls++;
init(); init();
lia_move ret; lia_move ret = iterate();
while (m_number_of_iterations++ < m_max_number_of_iterations) { if (ret == lia_move::branch || ret == lia_move::conflict)
ret = iterate(); return ret;
// decide on ret SASSERT(ret == lia_move::undef);
if (ret == lia_move::branch) { ret = process_undef();
process_branch(); if (ret == lia_move::sat || ret == lia_move::conflict)
} else if (ret == lia_move::conflict) { return ret;
process_conflict(); SASSERT(ret == lia_move::undef);
if (decide_on_conflict())
return lia_move::conflict;
} else {
SASSERT(ret == lia_move::undef);
ret = process_undef();
if (ret == lia_move::sat)
return ret;
if (ret == lia_move::conflict)
return ret;
}
}
return lia_move::undef; return lia_move::undef;
} }

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

@ -180,9 +180,7 @@ namespace lp {
m_dioph_eq_period = settings().m_dioph_eq_period; m_dioph_eq_period = settings().m_dioph_eq_period;
return lia_move::branch; return lia_move::branch;
} }
return r;
// m_dioph_eq_period *= 2;
return lia_move::undef;
} }
lp_settings& settings() { return lra.settings(); } lp_settings& settings() { return lra.settings(); }

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

@ -129,6 +129,7 @@ struct statistics {
unsigned m_offset_eqs = 0; unsigned m_offset_eqs = 0;
unsigned m_fixed_eqs = 0; unsigned m_fixed_eqs = 0;
unsigned m_dio_conflicts = 0; unsigned m_dio_conflicts = 0;
unsigned m_dio_calls = 0;
::statistics m_st = {}; ::statistics m_st = {};
void reset() { void reset() {
@ -161,7 +162,8 @@ struct statistics {
st.update("arith-nla-lemmas", m_nla_lemmas); st.update("arith-nla-lemmas", m_nla_lemmas);
st.update("arith-nra-calls", m_nra_calls); st.update("arith-nra-calls", m_nra_calls);
st.update("arith-bounds-improvements", m_nla_bounds_improvements); st.update("arith-bounds-improvements", m_nla_bounds_improvements);
st.update("arith-lp-dio-conflicts", m_dio_conflicts); st.update("arith-dio-calls", m_dio_calls);
st.update("arith-dio-conflicts", m_dio_conflicts);
st.copy(m_st); st.copy(m_st);
} }
}; };