mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

hook up generate_simple_tangent_lemma()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-16 13:58:42 -07:00
parent b2b4193afa
commit f20a028f7b
4 changed files with 30 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1624,6 +1624,14 @@ bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
return false; return false;
} }
rational core::val(const factorization& f) const {
rational r(1);
for (const factor &p : f) {
r *= val(p);
}
return r;
}
void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) { void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
add_empty_lemma(); add_empty_lemma();
SASSERT(sign == nla::rat_sign(product_value(m.vars()))); SASSERT(sign == nla::rat_sign(product_value(m.vars())));

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

@ -108,6 +108,8 @@ public:
rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); } rational val(const factor& f) const { return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
rational val(const factorization&) const;
lpvar var(const factor& f) const { return f.var(); } lpvar var(const factor& f) const { return f.var(); }
svector<lpvar> sorted_rvars(const factor& f) const; svector<lpvar> sorted_rvars(const factor& f) const;

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

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

2
src/util/lp/nla_tangent_lemmas.h
View file

@ -54,7 +54,7 @@ public:
private: private:
lpvar find_binomial_to_refine(); lpvar find_binomial_to_refine();
void generate_explanations_of_tang_lemma(const monomial& m, const factorization& bf, lp::explanation& exp); void generate_explanations_of_tang_lemma(const monomial& m, const factorization& bf, lp::explanation& exp);
void generate_simple_tangent_lemma(const monomial& m); void generate_simple_tangent_lemma(const monomial& m, const factorization&);
void tangent_lemma_bf(const monomial& m,const factorization& bf); void tangent_lemma_bf(const monomial& m,const factorization& bf);
void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j); void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j);