mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

lemma_for_proportional_factors_on_vars_le

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-26 15:01:56 -07:00 • committed by Lev Nachmanson
parent 51e08188f5
commit f8e4f5c5c6
1 changed files with 47 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1107,7 +1107,7 @@ struct solver::imp {
} }
}; };
// we derive a lemma from |x| >= 1 || |y| = 0 => |xy| >= |y| // we derive a lemma from |x| >= 1 || y = 0 => |xy| >= |y|
bool lemma_for_proportional_factors_on_vars_ge(lpvar i, lpvar j, lpvar k) { bool lemma_for_proportional_factors_on_vars_ge(lpvar i, lpvar j, lpvar k) {
if (!(abs(vvr(j)) >= rational(1) || vvr(k).is_zero())) if (!(abs(vvr(j)) >= rational(1) || vvr(k).is_zero()))
return false; return false;
@ -1118,25 +1118,51 @@ struct solver::imp {
} }
return false; return false;
} }
// here xy
// we derive a lemma from |x| <= 1 || |y| = 0 => |xy| <= |y| // we derive a lemma from |x| <= 1 || y = 0 => |xy| <= |y|
bool lemma_for_proportional_factors_on_vars_le(lpvar i, lpvar j, lpvar k) { bool lemma_for_proportional_factors_on_vars_le(lpvar xy, lpvar x, lpvar y) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "i="; tout << "xy=";
print_var(i, tout); print_var(xy, tout);
tout << "j="; tout << "x=";
print_var(j, tout); print_var(x, tout);
tout << "k="; tout << "y=";
print_var(k, tout);); print_var(y, tout););
const rational & _x = vvr(x);
if (!(abs(vvr(j)) <= rational(1) || vvr(k).is_zero())) const rational & _y = vvr(y);
if (!(abs(_x) <= rational(1) || _y.is_zero()))
return false; return false;
// the precondition holds // the precondition holds
if (! (abs(vvr(i)) <= abs(vvr(k)))) { const rational & _xy = vvr(xy);
SASSERT(false); // create here if (abs(_xy) <= abs(_y))
return true; return false;
} // adding x != val(x);
return false; lp::lar_term t;
t.add_coeff_var(rational(1), x);
m_lemma->push_back(ineq(lp::lconstraint_kind::NE, t, _x));
t.clear();
t.add_coeff_var(rational(1), y);
int y_sign;
if (_y.is_pos()) {
y_sign = 1;
m_lemma->push_back(ineq(lp::lconstraint_kind::LE, t, rational::zero()));
} else if (_y.is_neg()) {
y_sign = -1;
m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t, rational::zero()));
} else {
SASSERT(_y.is_zero());
y_sign = 1;
m_lemma->push_back(ineq(lp::lconstraint_kind::NE, t, rational::zero()));
}
int xy_sign = _xy.is_pos()? 1: -1;
t.clear(); // abs(xy) - abs(y) <= 0
t.add_coeff_var(rational(xy_sign), xy);
t.add_coeff_var(rational(-y_sign), y);
m_lemma->push_back(ineq(lp::lconstraint_kind::LE, t, rational::zero()));
TRACE("nla_solver", tout<< "lemma: ";print_lemma(*m_lemma, tout););
return true;
} }
@ -1153,13 +1179,10 @@ struct solver::imp {
tout << "*"; tout << "*";
print_var(f.m_k, tout); print_var(f.m_k, tout);
); );
if (lemma_for_proportional_factors_on_vars_ge(var_of_mon, f.m_j, f.m_k) return lemma_for_proportional_factors_on_vars_ge(var_of_mon, f.m_j, f.m_k)
|| lemma_for_proportional_factors_on_vars_ge(var_of_mon, f.m_k, f.m_j)) || lemma_for_proportional_factors_on_vars_ge(var_of_mon, f.m_k, f.m_j)
return true; || lemma_for_proportional_factors_on_vars_le(var_of_mon, f.m_j, f.m_k)
if (lemma_for_proportional_factors_on_vars_le(var_of_mon, f.m_j, f.m_k) || lemma_for_proportional_factors_on_vars_le(var_of_mon, f.m_k, f.m_j);
|| lemma_for_proportional_factors_on_vars_le(var_of_mon, f.m_k, f.m_j))
return true;
return false;
} }
// we derive a lemma from |xy| >= |y| => |x| >= 1 || |y| = 0 // we derive a lemma from |xy| >= |y| => |x| >= 1 || |y| = 0
bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) { bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) {