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

fix bool sign usage

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-07 11:49:51 -07:00
parent c35b561496
commit eb657a322a
4 changed files with 35 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/lp/nla_basics_lemmas.cpp
View file

@ -703,7 +703,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const f
// 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 = sign_to_rat(rm.rsign());
TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
TRACE("nla_solver_bl", tout << pp_rmon(_(), rm) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; );
lpvar not_one = -1;
for (auto j : f){
TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
@ -729,7 +729,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
if (not_one + 1) {
// we found the only not_one
if (val(rm) == val(not_one) * sign) {
TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;);
return false;
}
} else {
@ -746,7 +746,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
for (auto j : f){
lpvar var_j = var(j);
if (not_one == var_j) continue;
c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : c().canonize_sign(j) * val(j));
c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : sign_to_rat(c().canonize_sign(j)) * val(j));
}
if (not_one == static_cast<lpvar>(-1)) {

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

@ -228,8 +228,12 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const
std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
out << "["; print_var(m.var(), out) << "]\n";
out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
out << "rsign:" << m.rsign() << "\n";
if (m.vars() == m.rvars())
out << "same rvars, and m.rsign = " << m.rsign() << " of course\n";
else {
out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
out << "rsign:" << m.rsign() << "\n";
}
return out;
}
@ -1586,7 +1590,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
rm_found = &rm;
if (find_bfc_to_refine_on_rmonomial(rm, bf)) {
j = rm.var();
sign = rm.rsign();
sign = sign_to_rat(rm.rsign());
TRACE("nla_solver", tout << "found bf";
tout << ":rm:" << pp_rmon(*this, rm) << "\n";
tout << "bf:"; print_bfc(bf, tout);

4
src/util/lp/nla_order_lemmas.cpp
View file

@ -218,7 +218,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
for (factor f: ab)
sign ^= _().canonize_sign(f);
const rational fv = val(ab[0]) * val(ab[1]);
const rational mv = sign * val(m);
const rational mv = sign_to_rat(sign) * val(m);
TRACE("nla_solver",
tout << "ab.size()=" << ab.size() << "\n";
tout << "we should have sign*val(m):" << mv << "=(" << sign << ")*(" << val(m) <<") to be equal to " << " val(ab[0])*val(ab[1]):" << fv << "\n";);
@ -266,7 +266,7 @@ void order::generate_ol(const monomial& ac,
llc ab_cmp) {
add_empty_lemma();
rational rc_sign = rational(c_sign);
mk_ineq(rc_sign * canonize_sign(c), var(c), llc::LE);
mk_ineq(rc_sign * sign_to_rat(canonize_sign(c)), var(c), llc::LE);
mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
mk_ineq(sign_to_rat(canonize_sign(a))*rc_sign, var(a), - sign_to_rat(canonize_sign(b))*rc_sign, var(b), negate(ab_cmp));
explain(ac);

23
src/util/rational.h
View file

@ -137,7 +137,16 @@ public:
m().set(m_val, r.m_val);
return *this;
}
private:
rational & operator=(bool) {
UNREACHABLE(); return *this;
}
inline rational operator*(bool r1) const {
UNREACHABLE();
return *this;
}
public:
rational & operator=(int v) {
*this = rational(v);
return *this;
@ -506,9 +515,18 @@ inline rational operator*(rational const & r1, rational const & r2) {
return rational(r1) *= r2;
}
inline rational operator*(rational const & r1, bool r2) {
UNREACHABLE();
return r1 * rational(r2);
}
inline rational operator*(rational const & r1, int r2) {
return r1 * rational(r2);
}
inline rational operator*(bool r1, rational const & r2) {
UNREACHABLE();
return rational(r1) * r2;
}
inline rational operator*(int r1, rational const & r2) {
return rational(r1) * r2;
}
@ -521,6 +539,11 @@ inline rational operator/(rational const & r1, int r2) {
return r1 / rational(r2);
}
inline rational operator/(rational const & r1, bool r2) {
UNREACHABLE();
return r1 / rational(r2);
}
inline rational operator/(int r1, rational const & r2) {
return rational(r1) / r2;
}