mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
detect more variable equivalances
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
65b950ec4f
commit
649d47d92c
|
|
@ -510,6 +510,11 @@ struct solver::imp {
|
|||
}
|
||||
|
||||
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs, lemma& l) {
|
||||
if (cmp == llc::NE) {
|
||||
mk_ineq(t, llc::LT, rs, l);
|
||||
mk_ineq(t, llc::GT, rs, l);
|
||||
return;
|
||||
}
|
||||
TRACE("nla_solver_details", m_lar_solver.print_term(t, tout << "t = "););
|
||||
if (explain_ineq(t, cmp, rs)) {
|
||||
return;
|
||||
|
|
@ -578,62 +583,6 @@ struct solver::imp {
|
|||
return cmp;
|
||||
}
|
||||
|
||||
// bool explain(lpvar j, llc cmp, const rational& rs, lp::explanation & exp) {
|
||||
// unsigned lc, uc; // indices for the lower and upper bounds
|
||||
// m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
|
||||
// switch(cmp) {
|
||||
// case llc::LE: {
|
||||
// if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
|
||||
// return false;
|
||||
// exp.add(uc);
|
||||
// return true;
|
||||
// }
|
||||
// case llc::LT: {
|
||||
// if (uc + 1 == 0 || m_lar_solver.column_upper_bound(j) >= rs)
|
||||
// return false;
|
||||
// exp.add(uc);
|
||||
// return true;
|
||||
// }
|
||||
// case llc::GE: {
|
||||
// if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs)
|
||||
// return false;
|
||||
// exp.add(lc);
|
||||
// return true;
|
||||
// }
|
||||
// case llc::GT: {
|
||||
// if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) <= rs)
|
||||
// return false;
|
||||
// exp.add(lc);
|
||||
// return true;
|
||||
// }
|
||||
// case llc::EQ:
|
||||
// {
|
||||
// if (lc + 1 == 0 || m_lar_solver.column_lower_bound(j) < rs
|
||||
// ||
|
||||
// uc + 1 == 0 || m_lar_solver.column_upper_bound(j) > rs)
|
||||
// return false;
|
||||
// exp.add(lc);
|
||||
// exp.add(uc);
|
||||
// return true;
|
||||
// }
|
||||
// case llc::NE: {
|
||||
// if (uc + 1 && m_lar_solver.column_upper_bound(j) < rs) {
|
||||
// exp.add(uc);
|
||||
// return true;
|
||||
// }
|
||||
// if (lc + 1 && m_lar_solver.column_lower_bound(j) > rs) {
|
||||
// exp.add(lc);
|
||||
// return true;
|
||||
// }
|
||||
// return false;
|
||||
// };
|
||||
// default:
|
||||
// SASSERT(false);
|
||||
// };
|
||||
// SASSERT(false);
|
||||
// return false;
|
||||
// }
|
||||
|
||||
void mk_ineq(const rational& a, lpvar j, llc cmp, lemma& l) {
|
||||
mk_ineq(a, j, cmp, rational::zero(), l);
|
||||
}
|
||||
|
|
@ -843,10 +792,6 @@ struct solver::imp {
|
|||
return zero_j;
|
||||
}
|
||||
|
||||
static bool is_set(unsigned j) {
|
||||
return static_cast<int>(j) != -1;
|
||||
}
|
||||
|
||||
bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
|
||||
SASSERT(sign);
|
||||
if (has_lower_bound(j) && get_lower_bound(j) >= rational(0))
|
||||
|
|
@ -941,14 +886,12 @@ struct solver::imp {
|
|||
return m_vars_equivalence.eq_vars(j);
|
||||
}
|
||||
|
||||
bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
|
||||
void basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
|
||||
TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n= "; print_monomial_with_vars(n, tout); );
|
||||
rational contr_sign;
|
||||
if (sign_contradiction(m, n, contr_sign)) {
|
||||
generate_sign_lemma(m, n, sign);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void init_abs_val_table() {
|
||||
|
|
@ -1024,9 +967,9 @@ struct solver::imp {
|
|||
for (index_with_sign i_s : mons_to_explore) {
|
||||
unsigned n = i_s.index();
|
||||
if (n == i) continue;
|
||||
if (basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign()))
|
||||
if(done())
|
||||
return true;
|
||||
basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign());
|
||||
if(done())
|
||||
return true;
|
||||
}
|
||||
TRACE("nla_solver",);
|
||||
return false;
|
||||
|
|
@ -1036,16 +979,18 @@ struct solver::imp {
|
|||
* \brief <generate lemma by using the fact that -ab = (-a)b) and
|
||||
-ab = a(-b)
|
||||
*/
|
||||
bool basic_sign_lemma(bool derived) {
|
||||
if (!derived)
|
||||
return basic_sign_lemma_model_based();
|
||||
|
||||
std::unordered_set<unsigned> explored;
|
||||
for (unsigned i : m_to_refine){
|
||||
if (basic_sign_lemma_on_mon(i, explored))
|
||||
return true;
|
||||
void basic_sign_lemma(bool derived) {
|
||||
if (!derived) {
|
||||
basic_sign_lemma_model_based();
|
||||
} else {
|
||||
std::unordered_set<unsigned> explored;
|
||||
for (unsigned i : m_to_refine){
|
||||
basic_sign_lemma_on_mon(i, explored);
|
||||
if (done())
|
||||
return;
|
||||
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool var_is_fixed_to_zero(lpvar j) const {
|
||||
|
|
@ -1715,11 +1660,10 @@ struct solver::imp {
|
|||
unsigned random() {return settings().random_next();}
|
||||
|
||||
// use basic multiplication properties to create a lemma
|
||||
bool basic_lemma(bool derived) {
|
||||
if (basic_sign_lemma(derived))
|
||||
return true;
|
||||
void basic_lemma(bool derived) {
|
||||
basic_sign_lemma(derived);
|
||||
if (derived)
|
||||
return false;
|
||||
return;
|
||||
init_rm_to_refine();
|
||||
const auto& rm_ref = m_rm_table.to_refine();
|
||||
TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
|
||||
|
|
@ -1733,8 +1677,6 @@ struct solver::imp {
|
|||
i = 0;
|
||||
}
|
||||
} while(i != start && !done());
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void map_monomial_vars_to_monomial_indices(unsigned i) {
|
||||
|
|
@ -1765,7 +1707,8 @@ struct solver::imp {
|
|||
// we look for octagon constraints here, with a left part +-x +- y
|
||||
void collect_equivs() {
|
||||
const lp::lar_solver& s = m_lar_solver;
|
||||
|
||||
|
||||
|
||||
for (unsigned i = 0; i < s.terms().size(); i++) {
|
||||
unsigned ti = i + s.terms_start_index();
|
||||
if (!s.term_is_used_as_row(ti))
|
||||
|
|
@ -1776,6 +1719,27 @@ struct solver::imp {
|
|||
add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
|
||||
}
|
||||
}
|
||||
|
||||
std::unordered_map<rational, lpvar> fixed_vars;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
if (!var_is_fixed_to_zero(j)) continue;
|
||||
rational v = abs(vvr(j));
|
||||
auto it = fixed_vars.find(v);
|
||||
if (it == fixed_vars.end()){
|
||||
fixed_vars[v] = j;
|
||||
} else {
|
||||
lpvar k = it->second;
|
||||
TRACE("nla_solver", tout << "fixed vars eq: " << k << ", " << j << ", fixed to " << vvr(j) << "\n";);
|
||||
add_equivalence_of_two_vars(k, j,
|
||||
s.get_column_upper_bound_witness(k),
|
||||
s.get_column_lower_bound_witness(k),
|
||||
s.get_column_upper_bound_witness(j),
|
||||
s.get_column_lower_bound_witness(j));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) {
|
||||
|
|
@ -1802,6 +1766,11 @@ struct solver::imp {
|
|||
rational sign((seen_minus && seen_plus)? 1 : -1);
|
||||
m_vars_equivalence.add_equiv(i, j, sign, c0, c1);
|
||||
}
|
||||
void add_equivalence_of_two_vars(lpvar k, lpvar j, lpci c0, lpci c1, lpci c2, lpci c3) {
|
||||
SASSERT(abs(vvr(k)) == abs(vvr(j)));
|
||||
rational sign(vvr(k) == vvr(j)? 1 : -1);
|
||||
m_vars_equivalence.add_equiv(k, j, sign, c0, c1, c2, c3);
|
||||
}
|
||||
|
||||
// x is equivalent to y if x = +- y
|
||||
void init_vars_equivalence() {
|
||||
|
|
@ -2825,7 +2794,7 @@ struct solver::imp {
|
|||
if (search_level == 0) {
|
||||
basic_lemma(derived);
|
||||
if (!m_lemma_vec->empty())
|
||||
return l_false;
|
||||
return l_false;
|
||||
} else if (search_level == 1) {
|
||||
order_lemma(derived);
|
||||
} else { // search_level == 2
|
||||
|
|
|
|||
|
|
@ -19,6 +19,8 @@
|
|||
--*/
|
||||
|
||||
namespace nla {
|
||||
bool is_set(unsigned j) { return static_cast<int>(j) != -1; }
|
||||
|
||||
|
||||
typedef lp::constraint_index lpci;
|
||||
typedef lp::explanation expl_set;
|
||||
|
|
@ -39,15 +41,24 @@ struct vars_equivalence {
|
|||
rational m_sign;
|
||||
lpci m_c0;
|
||||
lpci m_c1;
|
||||
|
||||
equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) :
|
||||
lpci m_c2;
|
||||
lpci m_c3;
|
||||
equiv(lpvar i, lpvar j, rational const& sign,
|
||||
lpci c0,
|
||||
lpci c1,
|
||||
lpci c2,
|
||||
lpci c3
|
||||
) :
|
||||
m_i(i),
|
||||
m_j(j),
|
||||
m_sign(sign),
|
||||
m_c0(c0),
|
||||
m_c1(c1) {
|
||||
m_c1(c1),
|
||||
m_c2(c2),
|
||||
m_c3(c3) {
|
||||
SASSERT(m_i != m_j);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
struct node {
|
||||
|
|
@ -139,9 +150,13 @@ struct vars_equivalence {
|
|||
}
|
||||
|
||||
void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) {
|
||||
m_equivs.push_back(equiv(i, j, sign, c0, c1));
|
||||
m_equivs.push_back(equiv(i, j, sign, c0, c1, -1, -1));
|
||||
}
|
||||
|
||||
|
||||
void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1, lpci c2, lpci c3) {
|
||||
m_equivs.push_back(equiv(i, j, sign, c0, c1, c2, c3));
|
||||
}
|
||||
|
||||
void connect_equiv_to_tree(unsigned k) {
|
||||
// m_tree is the tree with the edges formed by m_equivs
|
||||
const equiv &e = m_equivs[k];
|
||||
|
|
@ -247,8 +262,14 @@ struct vars_equivalence {
|
|||
if (it->second.m_parent == static_cast<unsigned>(-1))
|
||||
return;
|
||||
const equiv & e = m_equivs[it->second.m_parent];
|
||||
exp.add(e.m_c0);
|
||||
exp.add(e.m_c1);
|
||||
if (is_set(e.m_c0))
|
||||
exp.add(e.m_c0);
|
||||
if (is_set(e.m_c1))
|
||||
exp.add(e.m_c1);
|
||||
if (is_set(e.m_c2))
|
||||
exp.add(e.m_c2);
|
||||
if (is_set(e.m_c3))
|
||||
exp.add(e.m_c3);
|
||||
j = get_parent_node(j, e);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue