mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
use fixed vars to explain tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
24aeaed50a
commit
472306c0b2
3 changed files with 56 additions and 42 deletions
|
|
@ -372,6 +372,7 @@ namespace lp {
|
|||
|
||||
void subs_front_in_indexed_vector(std::queue<unsigned> & q) {
|
||||
unsigned k = pop_front(q);
|
||||
if (m_indexed_work_vector[k].is_zero()) return;
|
||||
const eprime_entry& e = entry_for_subs(k);
|
||||
TRACE("dioph_eq", tout << "k:" << k << ", in "; print_term_o(create_term_from_ind_c(), tout) << std::endl;
|
||||
tout << "subs with e:"; print_eprime_entry(e, tout) << std::endl;);
|
||||
|
|
@ -557,7 +558,15 @@ namespace lp {
|
|||
return false;
|
||||
}
|
||||
// g is not trivial, trying to tighten the bounds
|
||||
return tighten_bounds_for_term(g, j);
|
||||
// by using bitwise to explore both bounds
|
||||
return tighten_bounds_for_term(g, j, true) | tighten_bounds_for_term(g, j, false);
|
||||
}
|
||||
|
||||
void get_expl_from_meta_term(const lar_term& t, explanation& ex) {
|
||||
for (const auto& p: t) {
|
||||
const auto& l = lra.get_term(p.j());
|
||||
get_expl_from_lar_term(l, ex);
|
||||
}
|
||||
}
|
||||
|
||||
void get_expl_from_lar_term(const lar_term & l, explanation& ex) {
|
||||
|
|
@ -580,13 +589,13 @@ namespace lp {
|
|||
u_dependency *b_dep = nullptr;
|
||||
if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
|
||||
if (m_c > rs || (is_strict && m_c == rs)) {
|
||||
get_expl_from_lar_term(m_tmp_l, m_infeas_explanation);
|
||||
get_expl_from_meta_term(m_tmp_l, m_infeas_explanation);
|
||||
return;
|
||||
}
|
||||
}
|
||||
if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
|
||||
if (m_c < rs || (is_strict && m_c == rs)) {
|
||||
get_expl_from_lar_term(m_tmp_l, m_infeas_explanation);
|
||||
get_expl_from_meta_term(m_tmp_l, m_infeas_explanation);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -595,36 +604,25 @@ namespace lp {
|
|||
// m_indexed_work_vector contains the coefficients of the term
|
||||
// m_c contains the constant term
|
||||
// m_tmp_l is the linear combination of the equations that removs the substituted variablse
|
||||
bool tighten_bounds_for_term(const mpq& g, unsigned j) {
|
||||
bool tighten_bounds_for_term(const mpq& g, unsigned j, bool is_upper) {
|
||||
mpq rs;
|
||||
bool is_strict;
|
||||
bool change = false;
|
||||
u_dependency *b_dep = nullptr;
|
||||
SASSERT(!g.is_zero());
|
||||
|
||||
if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
|
||||
if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) {
|
||||
TRACE("dioph_eq", tout << "current upper bound for x:" << j << ":" << rs << std::endl;);
|
||||
rs = (rs - m_c) / g;
|
||||
TRACE("dioph_eq", tout << "(rs - m_c) / g:" << rs << std::endl;);
|
||||
if (!rs.is_int()) {
|
||||
tighten_bound_for_term_for_bound_kind(g, j, rs, true);
|
||||
change = true;
|
||||
tighten_bound_for_term_for_bound_kind(g, j, rs, is_upper, b_dep);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
|
||||
TRACE("dioph_eq", tout << "current lower bound for x" << j << ":" << rs << std::endl;);
|
||||
rs = (rs - m_c) / g;
|
||||
TRACE("dioph_eq", tout << "(rs - m_c) / g:" << rs << std::endl;);
|
||||
if (!rs.is_int()) {
|
||||
tighten_bound_for_term_for_bound_kind(g, j, rs, false);
|
||||
change = true;
|
||||
}
|
||||
}
|
||||
return change;
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void tighten_bound_for_term_for_bound_kind( const mpq& g, unsigned j, const mpq & ub, bool upper) {
|
||||
void tighten_bound_for_term_for_bound_kind( const mpq& g, unsigned j, const mpq & ub, bool upper, u_dependency* prev_dep) {
|
||||
// ub = (upper_bound(j) - m_c)/g.
|
||||
// we have x[j] = t = g*t_+ m_c <= upper_bound(j), then
|
||||
// t_ <= floor((upper_bound(j) - m_c)/g) = floor(ub)
|
||||
|
|
@ -638,14 +636,29 @@ namespace lp {
|
|||
|
||||
SASSERT(upper && bound < lra.get_upper_bound(j).x || !upper && bound > lra.get_lower_bound(j).x);
|
||||
lconstraint_kind kind = upper? lconstraint_kind::LE: lconstraint_kind::GE;
|
||||
u_dependency* dep = collect_explanation_from_indexed_vector(upper);
|
||||
dep = lra.mk_join(dep, explain_fixed(m_tmp_l));
|
||||
u_dependency* dep = prev_dep;
|
||||
dep = lra.mk_join(dep, explain_fixed_in_meta_term(m_tmp_l));
|
||||
u_dependency* j_bound_dep = upper? lra.get_column_upper_bound_witness(j): lra.get_column_lower_bound_witness(j);
|
||||
dep = lra.mk_join(dep, j_bound_dep);
|
||||
TRACE("dioph_eq", tout << "jterm:"; print_lar_term_L(lra.get_term(j), tout) << "\ndep:"; print_dep(tout, dep) << std::endl;);
|
||||
lra.update_column_type_and_bound(j, kind, bound, dep);
|
||||
}
|
||||
|
||||
u_dependency* explain_fixed_in_meta_term(const lar_term& t) {
|
||||
u_dependency* dep = nullptr;
|
||||
|
||||
for (const auto& p: t) {
|
||||
lar_term const& term = lra.get_term(p.j());
|
||||
for (const auto& q: term) {
|
||||
if (is_fixed(q.j())) {
|
||||
u_dependency* bound_dep = lra.get_bound_constraint_witnesses_for_column(q.j());
|
||||
dep = lra.mk_join(dep, bound_dep);
|
||||
}
|
||||
}
|
||||
}
|
||||
return dep;
|
||||
}
|
||||
|
||||
u_dependency* explain_fixed(const lar_term& t) {
|
||||
u_dependency* dep = nullptr;
|
||||
for (const auto& p: t) {
|
||||
|
|
@ -657,23 +670,6 @@ namespace lp {
|
|||
return dep;
|
||||
}
|
||||
|
||||
u_dependency* collect_explanation_from_indexed_vector(bool upper) {
|
||||
TRACE("dioph_eq",
|
||||
tout << (upper?"upper":"lower") << std::endl;
|
||||
tout << "indexed_vec:"; print_term_o(create_term_from_ind_c(), tout);
|
||||
);
|
||||
|
||||
term_o t = remove_fresh_vars(create_term_from_ind_c());
|
||||
|
||||
u_dependency* dep = nullptr;
|
||||
int bound_sign = upper? 1: -1;
|
||||
for (const auto& p: t) {
|
||||
int var_bound_sign = p.coeff().is_pos()? bound_sign: -bound_sign;
|
||||
u_dependency* bound_dep = (var_bound_sign == 1? lra.get_column_upper_bound_witness(p.var()): lra.get_column_lower_bound_witness(p.var()));
|
||||
dep = lra.mk_join(dep, bound_dep);
|
||||
}
|
||||
return dep;
|
||||
}
|
||||
public:
|
||||
lia_move check() {
|
||||
init();
|
||||
|
|
@ -916,7 +912,17 @@ public:
|
|||
out << "\tm_l:{"; print_lar_term_L(e.m_l, out) << "}, ";
|
||||
print_ml(e.m_l, out<< " \topened m_l:") << "\n";
|
||||
}
|
||||
out << "}\n";
|
||||
switch (e.m_entry_status)
|
||||
{
|
||||
case entry_status::F:
|
||||
out << "\tF\n";
|
||||
break;
|
||||
case entry_status::S:
|
||||
out << "\tS\n";
|
||||
break;
|
||||
default:
|
||||
out << "\tNOSF\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1060,7 +1060,13 @@ namespace lp {
|
|||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
bool lar_solver::has_bound_of_type(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict, bool is_upper) const {
|
||||
if (is_upper) {
|
||||
return has_upper_bound(var, ci, value, is_strict);
|
||||
} else {
|
||||
return has_lower_bound(var, ci, value, is_strict);
|
||||
}
|
||||
}
|
||||
bool lar_solver::has_lower_bound(lpvar var, u_dependency*& dep, mpq& value, bool& is_strict) const {
|
||||
|
||||
if (var >= m_columns.size()) {
|
||||
|
|
|
|||
|
|
@ -510,7 +510,7 @@ public:
|
|||
u_dependency_manager& dep_manager() { return m_dependencies; }
|
||||
|
||||
inline u_dependency* get_column_upper_bound_witness(unsigned j) const {
|
||||
return m_columns[j].upper_bound_witness();
|
||||
return m_columns[j].upper_bound_witness();
|
||||
}
|
||||
|
||||
inline const impq& get_upper_bound(lpvar j) const {
|
||||
|
|
@ -527,6 +527,8 @@ public:
|
|||
|
||||
bool has_lower_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const;
|
||||
bool has_upper_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const;
|
||||
bool has_bound_of_type(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict, bool is_upper) const;
|
||||
|
||||
bool has_value(lpvar var, mpq& value) const;
|
||||
bool fetch_normalized_term_column(const lar_term& t, std::pair<mpq, lpvar>&) const;
|
||||
bool column_is_fixed(unsigned j) const;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue