mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 10:56:16 +00:00
Code Activity

add simple sign lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-08 12:42:45 -08:00
parent 34137cfa0a
commit 45ea23be21
1 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2281,6 +2281,19 @@ struct solver::imp {
return false; return false;
} }
void generate_simple_sign_lemma(const rational& sign, const monomial& m) {
SASSERT(sign == rat_sign(product_value(m)));
for (lpvar j : m) {
if (vvr(j).is_pos()) {
mk_ineq(j, llc::LE, current_lemma());
} else {
SASSERT(vvr(j).is_neg());
mk_ineq(j, llc::GE, current_lemma());
}
}
mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma());
}
bool generate_simple_tangent_lemma(const rooted_mon* rm) { bool generate_simple_tangent_lemma(const rooted_mon* rm) {
add_empty_lemma_and_explanation(); add_empty_lemma_and_explanation();
unsigned i_mon = rm->orig_index(); unsigned i_mon = rm->orig_index();
@ -2290,7 +2303,10 @@ struct solver::imp {
SASSERT(mv != v); SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero()); SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(rat_sign(mv)); rational sign = rational(rat_sign(mv));
SASSERT(sign == rat_sign(v)); if (sign != rat_sign(v)) {
generate_simple_sign_lemma(sign, m);
return true;
}
bool gt = abs(mv) > abs(v); bool gt = abs(mv) > abs(v);
if (gt) { if (gt) {
for (lpvar j : m) { for (lpvar j : m) {