mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

add explanations of factorizations

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-16 10:13:55 -07:00 • committed by Lev Nachmanson
parent 94448f36bb
commit c20a04ea84
1 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/util/lp/nla_solver.cpp
View file

@ -394,8 +394,7 @@ struct solver::imp {
mk_ineq(j, lp::lconstraint_kind::EQ); mk_ineq(j, lp::lconstraint_kind::EQ);
} }
expl_set e; expl_set e;
add_explanation_of_factorization(i_mon, f, e); add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
set_expl(e);
return true; return true;
} }
@ -411,6 +410,11 @@ struct solver::imp {
add_explanation_of_reducing_to_rooted_monomial(m_monomials[i_mon], e); add_explanation_of_reducing_to_rooted_monomial(m_monomials[i_mon], e);
} }
void add_explanation_of_factorization_and_set_explanation(unsigned i_mon, const factorization& f, expl_set& e){
add_explanation_of_factorization(i_mon, f, e);
set_expl(e);
}
// x = 0 or y = 0 -> xy = 0 // x = 0 or y = 0 -> xy = 0
bool basic_lemma_for_mon_zero_from_factors_to_monomial(unsigned i_mon, const factorization& f) { bool basic_lemma_for_mon_zero_from_factors_to_monomial(unsigned i_mon, const factorization& f) {
if (vvr(m_monomials[i_mon].var()).is_zero()) if (vvr(m_monomials[i_mon].var()).is_zero())
@ -431,8 +435,7 @@ struct solver::imp {
mk_ineq(m_monomials[i_mon].var(), lp::lconstraint_kind::EQ); mk_ineq(m_monomials[i_mon].var(), lp::lconstraint_kind::EQ);
expl_set e; expl_set e;
add_explanation_of_factorization(i_mon, f, e); add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
set_expl(e);
return true; return true;
} }
@ -489,7 +492,9 @@ struct solver::imp {
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, rational(1)); mk_ineq(not_one_j, lp::lconstraint_kind::EQ, rational(1));
// not_one_j = -1 // not_one_j = -1
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1)); mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1));
expl_set e;
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
return true; return true;
} }
@ -516,6 +521,9 @@ struct solver::imp {
return false; return false;
} }
expl_set e;
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
if (not_one_j == static_cast<lpvar>(-1)) { if (not_one_j == static_cast<lpvar>(-1)) {
// we can derive that the value of the monomial is equal to sign // we can derive that the value of the monomial is equal to sign
for (lpvar j : f){ for (lpvar j : f){
@ -644,7 +652,6 @@ struct solver::imp {
} }
void register_key_mono_in_min_monomials(monomial_coeff const& mc, unsigned i) { void register_key_mono_in_min_monomials(monomial_coeff const& mc, unsigned i) {
mono_index_with_sign ms(i, mc.coeff()); mono_index_with_sign ms(i, mc.coeff());
auto it = m_rooted_monomials.find(mc.vars()); auto it = m_rooted_monomials.find(mc.vars());
if (it == m_rooted_monomials.end()) { if (it == m_rooted_monomials.end()) {