mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
operate with sign as a boolean
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
6d5fd5d980
commit
495161fe5c
|
|
@ -280,7 +280,6 @@ void emonomials::do_canonize(monomial & m) const {
|
|||
|
||||
bool emonomials::is_canonized(const monomial & m) const {
|
||||
monomial mm(m);
|
||||
do_canonize(mm);
|
||||
return mm.rvars() == m.rvars();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -61,8 +61,7 @@ public:
|
|||
unsigned visited() const { return m_visited; }
|
||||
unsigned& visited() { return m_visited; }
|
||||
svector<lpvar> const& rvars() const { return m_rvars; }
|
||||
bool sign() const { return m_rsign; }
|
||||
rational rsign() const { return rational(m_rsign ? -1 : 1); }
|
||||
bool rsign() const { return m_rsign; }
|
||||
void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
|
||||
void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
|
||||
void sort_rvars() {
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ basics::basics(core * c) : common(c) {}
|
|||
// Monomials m and n vars have the same values, up to "sign"
|
||||
// Generate a lemma if values of m.var() and n.var() are not the same up to sign
|
||||
bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n) {
|
||||
const rational& sign = m.rsign() * n.rsign();
|
||||
const rational sign = sign_to_rat(m.rsign() ^ n.rsign());
|
||||
if (val(m) == val(n) * sign)
|
||||
return false;
|
||||
TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";);
|
||||
|
|
@ -478,14 +478,25 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
|
|||
explain(rm);
|
||||
}
|
||||
TRACE("nla_solver", c().print_lemma(tout); );
|
||||
}
|
||||
}
|
||||
|
||||
bool basics::is_separated_from_zero(const factorization& f) const {
|
||||
for (const factor& fc: f) {
|
||||
lpvar j = var(fc);
|
||||
if (!(c().var_has_positive_lower_bound(j) || c().var_has_negative_upper_bound(j))) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
// here we use the fact xy = 0 -> x = 0 or y = 0
|
||||
void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const factorization& f) {
|
||||
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
|
||||
SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
|
||||
add_empty_lemma();
|
||||
int sign = c().get_derived_sign(rm, f);
|
||||
if (sign == 0) {
|
||||
if (is_separated_from_zero(f)) {
|
||||
c().mk_ineq(var(rm), llc::NE);
|
||||
for (auto j : f) {
|
||||
c().mk_ineq(var(j), llc::EQ);
|
||||
|
|
@ -496,7 +507,6 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
|
|||
c().explain_separation_from_zero(var(j));
|
||||
}
|
||||
}
|
||||
explain(rm);
|
||||
explain(f);
|
||||
TRACE("nla_solver", c().print_lemma(tout););
|
||||
}
|
||||
|
|
@ -692,7 +702,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const f
|
|||
// use the fact
|
||||
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
|
||||
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& rm, const factorization& f) {
|
||||
rational sign = rm.rsign();
|
||||
rational sign = sign_to_rat(rm.rsign());
|
||||
TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
|
||||
lpvar not_one = -1;
|
||||
for (auto j : f){
|
||||
|
|
|
|||
|
|
@ -103,5 +103,6 @@ struct basics: common {
|
|||
// none of the factors is zero and the product is not zero
|
||||
// -> |fc[factor_index]| <= |rm|
|
||||
void generate_pl(const monomial& rm, const factorization& fc, int factor_index);
|
||||
bool is_separated_from_zero(const factorization&) const;
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,15 +40,14 @@ template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
|
|||
template lpvar common::var<factor>(factor const& t) const;
|
||||
template lpvar common::var<monomial>(monomial const& t) const;
|
||||
void common::add_empty_lemma() { c().add_empty_lemma(); }
|
||||
template <typename T> rational common::canonize_sign(const T& t) const {
|
||||
template <typename T> bool common::canonize_sign(const T& t) const {
|
||||
return c().canonize_sign(t);
|
||||
}
|
||||
|
||||
template rational common::canonize_sign<monomial>(const monomial& t) const;
|
||||
template rational common::canonize_sign<factor>(const factor& t) const;
|
||||
rational common::canonize_sign(lpvar j) const {
|
||||
return c().canonize_sign_of_var(j);
|
||||
}
|
||||
template bool common::canonize_sign<monomial>(const monomial&) const;
|
||||
template bool common::canonize_sign<factor>(const factor&) const;
|
||||
template bool common::canonize_sign<lpvar>(const lpvar&) const;
|
||||
|
||||
void common::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs){
|
||||
c().mk_ineq(t, cmp, rs);
|
||||
}
|
||||
|
|
@ -68,6 +67,10 @@ void common::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc
|
|||
c().mk_ineq(a, j, b, k, cmp);
|
||||
}
|
||||
|
||||
void common::mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp) {
|
||||
c().mk_ineq(sign_to_rat(a), j, sign_to_rat(b), k, cmp);
|
||||
}
|
||||
|
||||
void common::mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) {
|
||||
c().mk_ineq(a, j, k, cmp, rs);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -57,8 +57,7 @@ struct common {
|
|||
template <typename T> void explain(const T&);
|
||||
void explain(lpvar);
|
||||
void add_empty_lemma();
|
||||
template <typename T> rational canonize_sign(const T&) const;
|
||||
rational canonize_sign(lpvar) const;
|
||||
template <typename T> bool canonize_sign(const T&) const;
|
||||
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs);
|
||||
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs);
|
||||
|
||||
|
|
@ -67,6 +66,7 @@ struct common {
|
|||
void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp);
|
||||
|
||||
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp);
|
||||
void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp);
|
||||
|
||||
void mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs);
|
||||
|
||||
|
|
|
|||
|
|
@ -92,23 +92,23 @@ svector<lpvar> core::sorted_rvars(const factor& f) const {
|
|||
|
||||
// the value of the factor is equal to the value of the variable multiplied
|
||||
// by the canonize_sign
|
||||
rational core::canonize_sign(const factor& f) const {
|
||||
return f.rat_sign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign());
|
||||
bool core::canonize_sign(const factor& f) const {
|
||||
return f.sign() ^ (f.is_var()? canonize_sign(f.var()) : m_emons[f.var()].rsign());
|
||||
}
|
||||
|
||||
rational core::canonize_sign_of_var(lpvar j) const {
|
||||
return m_evars.find(j).rsign();
|
||||
bool core::canonize_sign(lpvar j) const {
|
||||
return m_evars.find(j).sign();
|
||||
}
|
||||
|
||||
bool core::canonize_sign_is_correct(const monomial& m) const {
|
||||
rational r(1);
|
||||
bool r = false;
|
||||
for (lpvar j : m.vars()) {
|
||||
r *= canonize_sign_of_var(j);
|
||||
r ^= canonize_sign(j);
|
||||
}
|
||||
return r == m.rsign();
|
||||
}
|
||||
|
||||
rational core::canonize_sign(const monomial& m) const {
|
||||
bool core::canonize_sign(const monomial& m) const {
|
||||
SASSERT(canonize_sign_is_correct(m));
|
||||
return m.rsign();
|
||||
}
|
||||
|
|
@ -811,18 +811,6 @@ void core::explain_separation_from_zero(lpvar j) {
|
|||
explain_existing_upper_bound(j);
|
||||
}
|
||||
|
||||
int core::get_derived_sign(const monomial& rm, const factorization& f) const {
|
||||
rational sign = rm.rsign(); // this is the flip sign of the variable var(rm)
|
||||
SASSERT(!sign.is_zero());
|
||||
for (const factor& fc: f) {
|
||||
lpvar j = var(fc);
|
||||
if (!(var_has_positive_lower_bound(j) || var_has_negative_upper_bound(j))) {
|
||||
return 0;
|
||||
}
|
||||
sign *= m_evars.find(j).rsign();
|
||||
}
|
||||
return nla::rat_sign(sign);
|
||||
}
|
||||
void core::trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const {
|
||||
out << "rooted vars: ";
|
||||
print_product(rm.rvars(), out);
|
||||
|
|
@ -1390,11 +1378,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
|
|||
// divides bc by c, so bc = b*c
|
||||
bool core::divide(const monomial& bc, const factor& c, factor & b) const {
|
||||
svector<lpvar> c_rvars = sorted_rvars(c);
|
||||
TRACE("nla_solver",
|
||||
tout << "c_rvars = ";
|
||||
print_product(c_rvars, tout);
|
||||
tout << "\nbc_rvars = ";
|
||||
print_product(bc.rvars(), tout););
|
||||
TRACE("nla_solver_div", tout << "c_rvars = "; print_product(c_rvars, tout); tout << "\nbc_rvars = "; print_product(bc.rvars(), tout););
|
||||
if (!lp::is_proper_factor(c_rvars, bc.rvars()))
|
||||
return false;
|
||||
|
||||
|
|
@ -1412,12 +1396,10 @@ bool core::divide(const monomial& bc, const factor& c, factor & b) const {
|
|||
b = factor(sv->var(), factor_type::MON);
|
||||
}
|
||||
SASSERT(!b.sign());
|
||||
// we should have bc.vars()*canonize_sign(bc) = bc.rvar() = b.rvars()*c.rvars() =
|
||||
// = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
|
||||
// so bc.vars()*canonize_sign(bc) = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
|
||||
// but canonize_sign(b) now is canonize_sign_of_var(b.m_var) or canonize_sign(m_monomials[b.m_var])
|
||||
// so we are adjusting it
|
||||
b.sign() = (canonize_sign(b) * canonize_sign(c) * canonize_sign(bc) == rational(1))? false: true;
|
||||
// We have bc = canonize_sign(bc)*bc.rvars() = canonize_sign(b)*b.rvars()*canonize_sign(c)*c.rvars().
|
||||
// Dividing by bc.rvars() we get canonize_sign(bc) = canonize_sign(b)*canonize_sign(c)
|
||||
// Currently, canonize_sign(b) is 1, we might need to adjust it
|
||||
b.sign() = canonize_sign(b) ^ canonize_sign(c) ^ canonize_sign(bc);
|
||||
TRACE("nla_solver", tout << "success div:"; print_factor(b, tout););
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1438,8 +1420,8 @@ void core::negate_factor_equality(const factor& c,
|
|||
}
|
||||
|
||||
void core::negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
|
||||
rational a_fs = canonize_sign(a);
|
||||
rational b_fs = canonize_sign(b);
|
||||
rational a_fs = sign_to_rat(canonize_sign(a));
|
||||
rational b_fs = sign_to_rat(canonize_sign(b));
|
||||
llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
|
||||
mk_ineq(a_fs*a_sign, var(a), - b_fs*b_sign, var(b), cmp);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -116,13 +116,13 @@ public:
|
|||
void add_empty_lemma();
|
||||
// the value of the factor is equal to the value of the variable multiplied
|
||||
// by the canonize_sign
|
||||
rational canonize_sign(const factor& f) const;
|
||||
bool canonize_sign(const factor& f) const;
|
||||
|
||||
rational canonize_sign_of_var(lpvar j) const;
|
||||
bool canonize_sign(lpvar j) const;
|
||||
|
||||
// the value of the rooted monomias is equal to the value of the m.var() variable multiplied
|
||||
// by the canonize_sign
|
||||
rational canonize_sign(const monomial& m) const;
|
||||
bool canonize_sign(const monomial& m) const;
|
||||
|
||||
|
||||
void deregister_monomial_from_monomialomials (const monomial & m, unsigned i);
|
||||
|
|
@ -186,6 +186,8 @@ public:
|
|||
|
||||
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs);
|
||||
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs);
|
||||
void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp, const rational& rs);
|
||||
void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp);
|
||||
void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs);
|
||||
void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp);
|
||||
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp);
|
||||
|
|
@ -240,20 +242,13 @@ public:
|
|||
|
||||
const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
|
||||
|
||||
|
||||
int get_derived_sign(const monomial& rm, const factorization& f) const;
|
||||
|
||||
|
||||
bool var_has_positive_lower_bound(lpvar j) const;
|
||||
|
||||
bool var_has_negative_upper_bound(lpvar j) const;
|
||||
|
||||
bool var_is_separated_from_zero(lpvar j) const;
|
||||
|
||||
|
||||
bool vars_are_equiv(lpvar a, lpvar b) const;
|
||||
|
||||
|
||||
bool vars_are_equiv(lpvar a, lpvar b) const;
|
||||
void explain_equiv_vars(lpvar a, lpvar b);
|
||||
void explain(const factorization& f, lp::explanation& exp);
|
||||
bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const;
|
||||
|
|
@ -353,6 +348,7 @@ struct pp_rmon {
|
|||
pp_rmon(core const& c, monomial const& m): c(c), m(m) {}
|
||||
pp_rmon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
|
||||
};
|
||||
inline rational sign_to_rat(bool s) { return rational(s? -1 : 1); }
|
||||
inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); }
|
||||
inline std::ostream& operator<<(std::ostream& out, pp_rmon const& p) { return p.c.print_monomial_with_vars(p.m, out); }
|
||||
|
||||
|
|
|
|||
|
|
@ -209,12 +209,14 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
|
|||
order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[!k], ac_f[k], rm_bd, b);
|
||||
}
|
||||
|
||||
// TBD: document what lemma is created here.
|
||||
|
||||
// Here ab is a binary factorization of m.
|
||||
// We try to find a monomial n = cd, such that |b| = |d|
|
||||
// and get a lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation
|
||||
void order::order_lemma_on_factorization(const monomial& m, const factorization& ab) {
|
||||
rational sign = m.rsign();
|
||||
bool sign = m.rsign();
|
||||
for (factor f: ab)
|
||||
sign *= _().canonize_sign(f);
|
||||
sign ^= _().canonize_sign(f);
|
||||
const rational fv = val(ab[0]) * val(ab[1]);
|
||||
const rational mv = sign * val(m);
|
||||
TRACE("nla_solver",
|
||||
|
|
@ -225,7 +227,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
|
|||
bool gt = mv > fv;
|
||||
TRACE("nla_solver", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
|
||||
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
|
||||
order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
|
||||
order_lemma_on_ab(m, sign_to_rat(sign), var(ab[k]), var(ab[j]), gt);
|
||||
explain(ab); explain(m);
|
||||
TRACE("nla_solver", _().print_lemma(tout););
|
||||
order_lemma_on_ac_explore(m, ab, j == 1);
|
||||
|
|
@ -265,7 +267,7 @@ void order::generate_ol(const monomial& ac,
|
|||
add_empty_lemma();
|
||||
rational rc_sign = rational(c_sign);
|
||||
mk_ineq(rc_sign * canonize_sign(c), var(c), llc::LE);
|
||||
mk_ineq(canonize_sign(ac), var(ac), -canonize_sign(bc), var(bc), ab_cmp);
|
||||
mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
|
||||
mk_ineq(canonize_sign(a)*rc_sign, var(a), - canonize_sign(b)*rc_sign, var(b), negate(ab_cmp));
|
||||
explain(ac);
|
||||
explain(a);
|
||||
|
|
|
|||
Loading…
Reference in a new issue