mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

reimplement lemmas on rooted monomials

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-26 15:54:52 -08:00 • committed by Lev Nachmanson
parent cc6dc9e7d4
commit 7e03e900b8
1 changed files with 11 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -653,18 +653,19 @@ struct solver::imp {
// use the fact // use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x // 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basic_lemma_for_mon_neutral_from_factors_to_monomial(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_neutral_from_factors_to_monomial(const rooted_mon& rm, const factorization& f) {
int sign = 1; rational sign = rm.m_orig.m_sign;
lpvar not_one_j = -1; lpvar not_one_j = -1;
for (lpvar j : f){ for (lpvar j : f){
if (vvr(j) == rational(1)) { if (vvr(j) == rational(1)) {
continue; continue;
} }
if (vvr(j) == -rational(1)) { if (vvr(j) == -rational(1)) {
sign = - sign; sign = - sign;
continue; continue;
} }
if (not_one_j == static_cast<lpvar>(-1)) { if (not_one_j == static_cast<lpvar>(-1)) {
not_one_j = j; not_one_j = j;
continue; continue;
@ -673,38 +674,27 @@ struct solver::imp {
// if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma // if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma
return false; return false;
} }
/*
expl_set e; expl_set e;
add_explanation_of_factorization_and_set_explanation(rm, f, e); add_explanation_of_factorization_and_set_explanation(rm, f, e);
if (not_one_j == static_cast<lpvar>(-1)) {
// we can derive that the value of the monomial is equal to sign
for (lpvar j : f){ for (lpvar j : f){
if (vvr(j) == rational(1)) { if (vvr(j) == rational(1)) {
mk_ineq(j, lp::lconstraint_kind::NE, rational(1)); mk_ineq(j, lp::lconstraint_kind::NE, rational(1));
} else if (vvr(j) == -rational(1)) { } else if (vvr(j) == -rational(1)) {
mk_ineq(j, lp::lconstraint_kind::NE, -rational(1)); mk_ineq(j, lp::lconstraint_kind::NE, -rational(1));
} }
} }
mk_ineq(m_monomials[i_mon].var(), lp::lconstraint_kind::EQ, rational(sign));
if (not_one_j == static_cast<lpvar>(-1)) {
mk_ineq(m_monomials[rm.orig_index()].var(), lp::lconstraint_kind::EQ, rational(sign));
} else {
mk_ineq(m_monomials[rm.orig_index()].var(), -rational(sign), not_one_j, lp::lconstraint_kind::EQ);
}
TRACE("nla_solver", print_lemma(tout);); TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
for (lpvar j : f){
if (vvr(j) == rational(1)) {
mk_ineq(j, lp::lconstraint_kind::NE, rational(1));
} else if (vvr(j) == -rational(1)) {
mk_ineq(j, lp::lconstraint_kind::NE, -rational(1));
}
}
mk_ineq(m_monomials[i_mon].var(), -rational(sign), not_one_j,lp::lconstraint_kind::EQ);
TRACE("nla_solver", print_lemma(tout););
return true;*/
return false;
}
bool basic_lemma_for_mon_neutral(const rooted_mon& rm, const factorization& factorization) { bool basic_lemma_for_mon_neutral(const rooted_mon& rm, const factorization& factorization) {
return return
basic_lemma_for_mon_neutral_monomial_to_factor(rm, factorization) || basic_lemma_for_mon_neutral_monomial_to_factor(rm, factorization) ||