mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

remove the generate_simple_tangent_lemma()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-19 21:55:46 -07:00
parent f20a028f7b
commit 58c8f3f118
3 changed files with 0 additions and 146 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

103
src/util/lp/nla_core.cpp
View file

@ -1632,109 +1632,6 @@ rational core::val(const factorization& f) const {
return r;
}
void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
add_empty_lemma();
SASSERT(sign == nla::rat_sign(product_value(m.vars())));
for (lpvar j : m.vars()) {
if (val(j).is_pos()) {
mk_ineq(j, llc::LE);
} else {
SASSERT(val(j).is_neg());
mk_ineq(j, llc::GE);
}
}
mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT));
TRACE("nla_solver", print_lemma(tout););
}
void core::generate_simple_tangent_lemma(const rooted_mon* rm) {
if (rm->size() != 2)
return;
TRACE("nla_solver", tout << "rm:"; print_rooted_monomial_with_vars(*rm, tout) << std::endl;);
add_empty_lemma();
unsigned i_mon = rm->orig_index();
const monomial & m = m_monomials[i_mon];
const rational v = product_value(m);
const rational& mv = vvr(m);
SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(nla::rat_sign(mv));
if (sign != nla::rat_sign(v)) {
generate_simple_sign_lemma(-sign, m);
return;
}
bool gt = abs(mv) > abs(v);
if (gt) {
for (lpvar j : m) {
const rational & jv = vvr(j);
rational js = rational(nla::rat_sign(jv));
mk_ineq(js, j, llc::LT);
mk_ineq(js, j, llc::GT, jv);
}
mk_ineq(sign, i_mon, llc::LT);
mk_ineq(sign, i_mon, llc::LE, v);
} else {
for (lpvar j : m) {
const rational & jv = vvr(j);
rational js = rational(nla::rat_sign(jv));
mk_ineq(js, j, llc::LT);
mk_ineq(js, j, llc::LT, jv);
}
mk_ineq(sign, m.var(), llc::LT);
mk_ineq(sign, m.var(), llc::GE, v);
}
TRACE("nla_solver", print_lemma(tout););
}
void core::tangent_lemma() {
bfc bf;
lpvar j;
rational sign;
const rooted_mon* rm = nullptr;
if (find_bfc_to_refine(bf, j, sign, rm)) {
tangent_lemma_bf(bf, j, sign, rm);
} else {
TRACE("nla_solver", tout << "cannot find a bfc to refine\n"; );
if (rm != nullptr)
generate_simple_tangent_lemma(rm);
}
}
void core::generate_explanations_of_tang_lemma(const rooted_mon& rm, const bfc& bf, lp::explanation& exp) {
// here we repeat the same explanation for each lemma
explain(rm, exp);
explain(bf.m_x, exp);
explain(bf.m_y, exp);
}
void core::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const rooted_mon* rm){
point a, b;
point xy (vvr(bf.m_x), vvr(bf.m_y));
rational correct_mult_val = xy.x * xy.y;
rational val = vvr(j) * sign;
bool below = val < correct_mult_val;
TRACE("nla_solver", tout << "rm = " << rm << ", below = " << below << std::endl; );
get_tang_points(a, b, below, val, xy);
TRACE("nla_solver", tout << "sign = " << sign << ", tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;);
unsigned lemmas_size_was = m_lemma_vec->size();
generate_two_tang_lines(bf, xy, sign, j);
generate_tang_plane(a.x, a.y, bf.m_x, bf.m_y, below, j, sign);
generate_tang_plane(b.x, b.y, bf.m_x, bf.m_y, below, j, sign);
// if rm == nullptr there is no need to explain equivs since we work on a monomial and not on a rooted monomial
if (rm != nullptr) {
lp::explanation expl;
generate_explanations_of_tang_lemma(*rm, bf, expl);
for (unsigned i = lemmas_size_was; i < m_lemma_vec->size(); i++) {
auto &l = (*m_lemma_vec)[i];
l.expl().add(expl);
}
}
TRACE("nla_solver",
for (unsigned i = lemmas_size_was; i < m_lemma_vec->size(); i++)
print_specific_lemma((*m_lemma_vec)[i], tout); );
}
void core::add_empty_lemma() {
m_lemma_vec->push_back(lemma());
}

1
src/util/lp/nla_core.h
View file

@ -326,7 +326,6 @@ public:
bool find_bfc_to_refine_on_monomial(const monomial&, factorization & bf);
bool find_bfc_to_refine(const monomial* & m, factorization& bf);
void generate_simple_sign_lemma(const rational& sign, const monomial& m);
void negate_relation(unsigned j, const rational& a);
bool conflict_found() const;

42
src/util/lp/nla_tangent_lemmas.cpp
View file

@ -82,7 +82,6 @@ void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){
TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;);
unsigned lemmas_size_was = c().m_lemma_vec->size();
rational sign(1);
generate_simple_tangent_lemma(m, bf);
generate_two_tang_lines(bf, xy, j);
generate_tang_plane(a.x, a.y, bf[0], bf[1], below, j);
generate_tang_plane(b.x, b.y, bf[0], bf[1], below, j);
@ -100,47 +99,6 @@ void tangents::tangent_lemma_bf(const monomial& m, const factorization& bf){
c().print_specific_lemma((*c().m_lemma_vec)[i], tout); );
}
// using a fact that
// a != 0 & b != 0 & |a|*|b| = c & |a'| ~ |a| & |b'| ~ |b| => |a'|*|b'| ~ c,
// where ~ is < or >.
void tangents::generate_simple_tangent_lemma(const monomial& m, const factorization& bf) {
TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
rational v = c().product_value(m.vars());
const rational mv = val(m);
SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(nla::rat_sign(mv));
if (sign != nla::rat_sign(v)) {
c().generate_simple_sign_lemma(-sign, m);
return;
}
c().add_empty_lemma();
v = val(bf);
SASSERT(rat_sign(v) == rat_sign(mv));
bool gt = abs(mv) > abs(v);
unsigned j;
if (gt) {
for (const factor& f : bf) {
j = var(f);
const rational jv = val(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LE);
c().mk_ineq(js, j, llc::GT, abs(jv));
}
c().mk_ineq(sign, m.var(), llc::LT);
c().mk_ineq(sign, m.var(), llc::LE, abs(v));
} else {
for (const factor& f : bf) {
j = var(f);
const rational jv = val(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT, abs(jv));
}
c().mk_ineq(sign, m.var(), llc::LT);
c().mk_ineq(sign, m.var(), llc::GE, abs(v));
}
TRACE("nla_solver", c().print_lemma(tout););
}
void tangents::generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j) {
add_empty_lemma();