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

renam vvr to val

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-24 09:53:14 -07:00
parent 11e3e1b463
commit 02379417a6
11 changed files with 155 additions and 236 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,7 +28,7 @@ basics::basics(core * c) : common(c) {}
// 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();
if (vvr(m) == vvr(n) * sign)
if (val(m) == val(n) * sign)
return false;
TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
generate_sign_lemma(m, n, sign);
@ -36,8 +36,8 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
}
void basics::generate_zero_lemmas(const monomial& m) {
SASSERT(!vvr(m).is_zero() && c().product_value(m.vars()).is_zero());
int sign = nla::rat_sign(vvr(m));
SASSERT(!val(m).is_zero() && c().product_value(m.vars()).is_zero());
int sign = nla::rat_sign(val(m));
unsigned_vector fixed_zeros;
lpvar zero_j = find_best_zero(m, fixed_zeros);
SASSERT(is_set(zero_j));
@ -77,7 +77,7 @@ bool basics::try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
}
void basics::get_non_strict_sign(lpvar j, int& sign) const {
const rational v = vvr(j);
const rational v = val(j);
if (v.is_zero()) {
try_get_non_strict_sign_from_bounds(j, sign);
} else {
@ -105,7 +105,7 @@ bool basics::basic_sign_lemma_model_based() {
unsigned sz = c().m_to_refine.size();
for (unsigned i = sz; i-- > 0; ) {
monomial const& m = c().m_emons[c().m_to_refine[(start + i) % sz]];
int mon_sign = nla::rat_sign(vvr(m));
int mon_sign = nla::rat_sign(val(m));
int product_sign = c().rat_sign(m);
if (mon_sign != product_sign) {
basic_sign_lemma_model_based_one_mon(m, product_sign);
@ -162,12 +162,12 @@ void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rat
explain(n);
TRACE("nla_solver", c().print_lemma(tout););
}
// try to find a variable j such that vvr(j) = 0
// try to find a variable j such that val(j) = 0
// and the bounds on j contain 0 as an inner point
lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
lpvar zero_j = -1;
for (unsigned j : m.vars()){
if (vvr(j).is_zero()){
if (val(j).is_zero()){
if (c().var_is_fixed_to_zero(j))
fixed_zeros.push_back(j);
@ -204,10 +204,10 @@ void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
}
void basics::negate_strict_sign(lpvar j) {
TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";);
if (!vvr(j).is_zero()) {
int sign = nla::rat_sign(vvr(j));
if (!val(j).is_zero()) {
int sign = nla::rat_sign(val(j));
c().mk_ineq(j, (sign == 1? llc::LE : llc::GE));
} else { // vvr(j).is_zero()
} else { // val(j).is_zero()
if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0)) {
c().explain_existing_lower_bound(j);
c().mk_ineq(j, llc::GT);
@ -322,7 +322,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
lpvar mon_var = c().m_emons[rm.var()].var();
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto mv = vvr(mon_var);
const auto mv = val(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
@ -332,7 +332,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
lpvar jl = -1;
for (auto fc : f ) {
lpvar j = var(fc);
if (abs(vvr(j)) == abs_mv && c().vars_are_equiv(j, mon_var) &&
if (abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) &&
(mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) {
jl = j;
break;
@ -346,7 +346,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomi
if (var(j) == jl) {
continue;
}
if (abs(vvr(j)) != rational(1)) {
if (abs(val(j)) != rational(1)) {
not_one_j = var(j);
break;
}
@ -382,14 +382,14 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monomial& rm, const facto
// x != 0 or y = 0 => |xy| >= |y|
void basics::proportion_lemma_model_based(const monomial& rm, const factorization& factorization) {
rational rmv = abs(vvr(rm));
rational rmv = abs(val(rm));
if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization));
return;
}
int factor_index = 0;
for (factor f : factorization) {
if (abs(vvr(f)) > rmv) {
if (abs(val(f)) > rmv) {
generate_pl(rm, factorization, factor_index);
return;
}
@ -399,14 +399,14 @@ void basics::proportion_lemma_model_based(const monomial& rm, const factorizatio
// x != 0 or y = 0 => |xy| >= |y|
bool basics::proportion_lemma_derived(const monomial& rm, const factorization& factorization) {
return false;
rational rmv = abs(vvr(rm));
rational rmv = abs(val(rm));
if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization));
return false;
}
int factor_index = 0;
for (factor f : factorization) {
if (abs(vvr(f)) > rmv) {
if (abs(val(f)) > rmv) {
generate_pl(rm, factorization, factor_index);
return true;
}
@ -418,7 +418,7 @@ bool basics::proportion_lemma_derived(const monomial& rm, const factorization& f
void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
add_empty_lemma();
unsigned mon_var = m.var();
rational mv = vvr(mon_var);
rational mv = val(mon_var);
rational sm = rational(nla::rat_sign(mv));
c().mk_ineq(sm, mon_var, llc::LT);
for (unsigned fi = 0; fi < m.size(); fi ++) {
@ -426,7 +426,7 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
if (fi != factor_index) {
c().mk_ineq(j, llc::EQ);
} else {
rational jv = vvr(j);
rational jv = val(j);
rational sj = rational(nla::rat_sign(jv));
SASSERT(sm*mv < sj*jv);
c().mk_ineq(sj, j, llc::LT);
@ -449,7 +449,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
}
add_empty_lemma();
int fi = 0;
rational rmv = vvr(rm);
rational rmv = val(rm);
rational sm = rational(nla::rat_sign(rmv));
unsigned mon_var = var(rm);
c().mk_ineq(sm, mon_var, llc::LT);
@ -458,7 +458,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
c().mk_ineq(var(f), llc::EQ);
} else {
lpvar j = var(f);
rational jv = vvr(j);
rational jv = val(j);
rational sj = rational(nla::rat_sign(jv));
SASSERT(sm*rmv < sj*jv);
c().mk_ineq(sj, j, llc::LT);
@ -474,7 +474,7 @@ void basics::generate_pl(const monomial& rm, const factorization& fc, int factor
// 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(vvr(rm).is_zero()&& ! c().rm_check(rm));
SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
add_empty_lemma();
int sign = c().get_derived_sign(rm, f);
if (sign == 0) {
@ -495,7 +495,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
if (vvr(rm).is_zero()) {
if (val(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty())
continue;
@ -519,14 +519,14 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
TRACE("nla_solver_bl", c().print_monomial(m, tout););
lpvar mon_var = m.var();
const auto mv = vvr(mon_var);
const auto mv = val(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
return false;
}
lpvar jl = -1;
for (auto j : m.vars() ) {
if (abs(vvr(j)) == abs_mv) {
if (abs(val(j)) == abs_mv) {
jl = j;
break;
}
@ -538,7 +538,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
if (j == jl) {
continue;
}
if (abs(vvr(j)) != rational(1)) {
if (abs(val(j)) != rational(1)) {
not_one_j = j;
break;
}
@ -553,7 +553,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
c().mk_ineq(mon_var, llc::EQ);
// negate abs(jl) == abs()
if (vvr(jl) == - vvr(mon_var))
if (val(jl) == - val(mon_var))
c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());
else // jl == mon_var
c().mk_ineq(jl, -rational(1), mon_var, llc::NE);
@ -573,7 +573,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
rational sign(1);
TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
for (auto j : m.vars()){
auto v = vvr(j);
auto v = val(j);
if (v == rational(1)) {
continue;
}
@ -590,7 +590,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
}
if (not_one + 1) { // we found the only not_one
if (vvr(m) == vvr(not_one) * sign) {
if (val(m) == val(not_one) * sign) {
TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
return false;
}
@ -599,7 +599,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
add_empty_lemma();
for (auto j : m.vars()){
if (not_one == j) continue;
c().mk_ineq(j, llc::NE, vvr(j));
c().mk_ineq(j, llc::NE, val(j));
}
if (not_one == static_cast<lpvar>(-1)) {
@ -619,7 +619,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
lpvar mon_var = c().m_emons[rm.var()].var();
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto mv = vvr(mon_var);
const auto mv = val(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
@ -627,7 +627,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
}
lpvar jl = -1;
for (auto j : f ) {
if (abs(vvr(j)) == abs_mv) {
if (abs(val(j)) == abs_mv) {
jl = var(j);
break;
}
@ -639,7 +639,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
if (var(j) == jl) {
continue;
}
if (abs(vvr(j)) != rational(1)) {
if (abs(val(j)) != rational(1)) {
not_one_j = var(j);
break;
}
@ -654,7 +654,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const mo
c().mk_ineq(mon_var, llc::EQ);
// negate abs(jl) == abs()
if (vvr(jl) == - vvr(mon_var))
if (val(jl) == - val(mon_var))
c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma());
else // jl == mon_var
c().mk_ineq(jl, -rational(1), mon_var, llc::NE);
@ -689,7 +689,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
lpvar not_one = -1;
for (auto j : f){
TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
auto v = vvr(j);
auto v = val(j);
if (v == rational(1)) {
continue;
}
@ -710,13 +710,13 @@ 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 (vvr(rm) == vvr(not_one) * sign) {
if (val(rm) == val(not_one) * sign) {
TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
return false;
}
} else {
// we have +-ones only in the factorization
if (vvr(rm) == sign) {
if (val(rm) == sign) {
return false;
}
}
@ -728,7 +728,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()? vvr(j) : c().canonize_sign(j) * vvr(j));
c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : c().canonize_sign(j) * val(j));
}
if (not_one == static_cast<lpvar>(-1)) {
@ -750,7 +750,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
TRACE("nla_solver_bl", c().print_factorization(f, tout););
int zero_j = -1;
for (auto j : f) {
if (vvr(j).is_zero()) {
if (val(j).is_zero()) {
zero_j = var(j);
break;
}

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

@ -32,10 +32,10 @@ template void common::explain<factorization>(const factorization& t);
void common::explain(lpvar j) { c().explain(j, c().current_expl()); }
template <typename T> rational common::vvr(T const& t) const { return c().vvr(t); }
template rational common::vvr<monomial>(monomial const& t) const;
template rational common::vvr<factor>(factor const& t) const;
rational common::vvr(lpvar t) const { return c().vvr(t); }
template <typename T> rational common::val(T const& t) const { return c().val(t); }
template rational common::val<monomial>(monomial const& t) const;
template rational common::val<factor>(factor const& t) const;
rational common::val(lpvar t) const { return c().val(t); }
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;

4
src/util/lp/nla_common.h
View file

@ -49,8 +49,8 @@ struct common {
core& _() { return *m_core; }
const core& _() const { return *m_core; }
template <typename T> rational vvr(T const& t) const;
rational vvr(lpvar) const;
template <typename T> rational val(T const& t) const;
rational val(lpvar) const;
template <typename T> lpvar var(T const& t) const;
bool done() const;
template <typename T> void explain(const T&);

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

@ -48,7 +48,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
rational core::value(const lp::lar_term& r) const {
rational ret(0);
for (const auto & t : r.coeffs()) {
ret += t.second * vvr(t.first);
ret += t.second * val(t.first);
}
return ret;
}
@ -151,7 +151,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
bool first = true;
for (lpvar v : m) {
if (!first) out << "*"; else first = false;
out << "(" << m_lar_solver.get_variable_name(v) << "=" << vvr(v) << ")";
out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
}
return out;
}
@ -180,7 +180,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
}
std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const {
out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << vvr(m.var()) << " = ";
out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
print_product(m.vars(), out) << ")\n";
return out;
}
@ -497,7 +497,7 @@ const lp::explanation& core::current_expl() const { return current_lemma().expl(
int core::vars_sign(const svector<lpvar>& v) {
int sign = 1;
for (lpvar j : v) {
sign *= nla::rat_sign(vvr(j));
sign *= nla::rat_sign(val(j));
if (sign == 0)
return 0;
}
@ -562,7 +562,7 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
int core::rat_sign(const monomial& m) const {
int sign = 1;
for (lpvar j : m.vars()) {
auto v = vvr(j);
auto v = val(j);
if (v.is_neg()) {
sign = - sign;
continue;
@ -577,8 +577,8 @@ int core::rat_sign(const monomial& m) const {
}
// Returns true if the monomial sign is incorrect
bool core:: sign_contradiction(const monomial& m) const {
return nla::rat_sign(vvr(m)) != rat_sign(m);
bool core::sign_contradiction(const monomial& m) const {
return nla::rat_sign(val(m)) != rat_sign(m);
}
/*
@ -718,7 +718,7 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
std::ostream & core::print_var(lpvar j, std::ostream & out) const {
if (m_emons.is_monomial_var(j)) {
print_monomial(m_emons[j], out);
out << " = " << vvr(j);;
out << " = " << val(j);;
}
m_lar_solver.print_column_info(j, out) <<";";
@ -791,8 +791,8 @@ void core::explain_existing_upper_bound(lpvar j) {
}
void core::explain_separation_from_zero(lpvar j) {
SASSERT(!vvr(j).is_zero());
if (vvr(j).is_pos())
SASSERT(!val(j).is_zero());
if (val(j).is_pos())
explain_existing_lower_bound(j);
else
explain_existing_upper_bound(j);
@ -816,7 +816,7 @@ void core::trace_print_monomial_and_factorization(const monomial& rm, const fact
out << "\n";
out << "mon: " << pp_mon(*this, rm.var()) << "\n";
out << "value: " << vvr(rm) << "\n";
out << "value: " << val(rm) << "\n";
print_factorization(f, out << "fact: ") << "\n";
}
@ -906,93 +906,14 @@ bool core:: basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const roo
}
}
if (not_one_j == static_cast<lpvar>(-1)) {
return false;
}
add_empty_lemma();
// mon_var = 0
mk_ineq(mon_var, llc::EQ);
// negate abs(jl) == abs()
if (vvr(jl) == - vvr(mon_var))
mk_ineq(jl, mon_var, llc::NE, current_lemma());
else // jl == mon_var
mk_ineq(jl, -rational(1), mon_var, llc::NE);
// not_one_j = 1
mk_ineq(not_one_j, llc::EQ, rational(1));
// not_one_j = -1
mk_ineq(not_one_j, llc::EQ, -rational(1));
explain(rm, current_expl());
explain(f, current_expl());
TRACE("nla_solver", print_lemma(tout); );
return true;
}
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool core:: basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m) {
TRACE("nla_solver_bl", print_monomial(m, tout););
lpvar mon_var = m.var();
const auto & mv = vvr(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
return false;
}
lpvar jl = -1;
for (auto j : m ) {
if (abs(vvr(j)) == abs_mv) {
jl = j;
break;
}
}
if (jl == static_cast<lpvar>(-1))
return false;
lpvar not_one_j = -1;
for (auto j : m ) {
if (j == jl) {
continue;
}
if (abs(vvr(j)) != rational(1)) {
not_one_j = j;
break;
}
}
if (not_one_j == static_cast<lpvar>(-1)) {
return false;
}
add_empty_lemma();
// mon_var = 0
mk_ineq(mon_var, llc::EQ);
// negate abs(jl) == abs()
if (vvr(jl) == - vvr(mon_var))
mk_ineq(jl, mon_var, llc::NE, current_lemma());
else // jl == mon_var
mk_ineq(jl, -rational(1), mon_var, llc::NE);
// not_one_j = 1
mk_ineq(not_one_j, llc::EQ, rational(1));
// not_one_j = -1
mk_ineq(not_one_j, llc::EQ, -rational(1));
TRACE("nla_solver", print_lemma(tout); );
return true;
}
bool core:: vars_are_equiv(lpvar a, lpvar b) const {
SASSERT(abs(vvr(a)) == abs(vvr(b)));
bool core::vars_are_equiv(lpvar a, lpvar b) const {
SASSERT(abs(val(a)) == abs(val(b)));
return m_evars.vars_are_equiv(a, b);
}
void core::explain_equiv_vars(lpvar a, lpvar b) {
SASSERT(abs(vvr(a)) == abs(vvr(b)));
SASSERT(abs(val(a)) == abs(val(b)));
if (m_evars.vars_are_equiv(a, b)) {
explain(a, current_expl());
explain(b, current_expl());
@ -1245,7 +1166,7 @@ void core::explain(const factorization& f, lp::explanation& exp) {
bool core:: has_zero_factor(const factorization& factorization) const {
for (factor f : factorization) {
if (vvr(f).is_zero())
if (val(f).is_zero())
return true;
}
return false;
@ -1255,7 +1176,7 @@ bool core:: has_zero_factor(const factorization& factorization) const {
template <typename T>
bool core:: mon_has_zero(const T& product) const {
for (lpvar j: product) {
if (vvr(j).is_zero())
if (val(j).is_zero())
return true;
}
return false;
@ -1292,7 +1213,7 @@ void core::collect_equivs_of_fixed_vars() {
for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
if (!var_is_fixed(j))
continue;
rational v = abs(vvr(j));
rational v = abs(val(j));
auto it = abs_map.find(v);
if (it == abs_map.end()) {
abs_map[v] = svector<lpvar>();
@ -1309,10 +1230,10 @@ void core::collect_equivs_of_fixed_vars() {
for (unsigned k = 1; k < v.size(); k++) {
auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]);
auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]);
if (vvr(head) == vvr(v[k])) {
if (val(head) == val(v[k])) {
m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3}));
} else {
SASSERT(vvr(head) == -vvr(v[k]));
SASSERT(val(head) == -val(v[k]));
m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3}));
}
}
@ -1396,7 +1317,7 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
if (m.size() == 2) return;
monomial_coeff mc = canonize_monomial(m);
for(unsigned i = 0; i < mc.vars().size(); i++){
if (abs(vvr(mc.vars()[i])) == rational(1)) {
if (abs(val(mc.vars()[i])) == rational(1)) {
auto vv = mc.vars();
vv.erase(vv.begin()+i);
monomial const* sv = m_emons.find_canonical(vv);
@ -1488,7 +1409,7 @@ void core::negate_factor_equality(const factor& c,
return;
lpvar i = var(c);
lpvar j = var(d);
auto iv = vvr(i), jv = vvr(j);
auto iv = val(i), jv = val(j);
SASSERT(abs(iv) == abs(jv));
if (iv == jv) {
mk_ineq(i, -rational(1), j, llc::NE);
@ -1500,7 +1421,7 @@ 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);
llc cmp = a_sign*vvr(a) < b_sign*vvr(b)? llc::GE : llc::LE;
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);
}
@ -1543,7 +1464,7 @@ void core::maybe_add_a_factor(lpvar i,
std::unordered_set<lpvar>& found_vars,
std::unordered_set<unsigned>& found_rm,
vector<factor> & r) const {
SASSERT(abs(vvr(i)) == abs(vvr(c)));
SASSERT(abs(val(i)) == abs(val(c)));
if (!m_emons.is_monomial_var(i)) {
i = m_evars.find(i).var();
if (try_insert(i, found_vars)) {
@ -1583,30 +1504,30 @@ bool core::rm_check(const monomial& rm) const {
/**
\brief Add |v| ~ |bound|
where ~ is <, <=, >, >=,
and bound = vvr(v)
and bound = val(v)
|v| > |bound|
<=>
(v < 0 or v > |bound|) & (v > 0 or -v > |bound|)
=> Let s be the sign of vvr(v)
=> Let s be the sign of val(v)
(s*v < 0 or s*v > |bound|)
|v| < |bound|
<=>
v < |bound| & -v < |bound|
=> Let s be the sign of vvr(v)
=> Let s be the sign of val(v)
s*v < |bound|
*/
void core::add_abs_bound(lpvar v, llc cmp) {
add_abs_bound(v, cmp, vvr(v));
add_abs_bound(v, cmp, val(v));
}
void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
SASSERT(!vvr(v).is_zero());
SASSERT(!val(v).is_zero());
lp::lar_term t; // t = abs(v)
t.add_coeff_var(rrat_sign(vvr(v)), v);
t.add_coeff_var(rrat_sign(val(v)), v);
switch (cmp) {
case llc::GT:
@ -1626,9 +1547,9 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
// NB - move this comment to monotonicity or appropriate.
/** \brief enforce the inequality |m| <= product |m[i]| .
by enforcing lemma:
/\_i |m[i]| <= |vvr(m[i])| => |m| <= |product_i vvr(m[i])|
/\_i |m[i]| <= |val(m[i])| => |m| <= |product_i val(m[i])|
<=>
\/_i |m[i]| > |vvr(m[i])} or |m| <= |product_i vvr(m[i])|
\/_i |m[i]| > |val(m[i])} or |m| <= |product_i val(m[i])|
*/
@ -1637,7 +1558,7 @@ bool core::find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf) {
if (factorization.size() == 2) {
auto a = factorization[0];
auto b = factorization[1];
if (vvr(rm) != vvr(a) * vvr(b)) {
if (val(rm) != val(a) * val(b)) {
bf = bfc(a, b);
return true;
}
@ -1668,7 +1589,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
TRACE("nla_solver", tout << "found bf";
tout << ":rm:" << rm << "\n";
tout << "bf:"; print_bfc(bf, tout);
tout << ", product = " << vvr(rm) << ", but should be =" << vvr(bf.m_x)*vvr(bf.m_y);
tout << ", product = " << val(rm) << ", but should be =" << val(bf.m_x)*val(bf.m_y);
tout << ", j == "; print_var(j, tout) << "\n";);
return true;
}
@ -1679,10 +1600,10 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
SASSERT(sign == nla::rat_sign(product_value(m.vars())));
for (lpvar j : m.vars()) {
if (vvr(j).is_pos()) {
if (val(j).is_pos()) {
mk_ineq(j, llc::LE);
} else {
SASSERT(vvr(j).is_neg());
SASSERT(val(j).is_neg());
mk_ineq(j, llc::GE);
}
}
@ -1805,8 +1726,8 @@ void core::generate_tang_plane(const rational & a, const rational& b, const fact
}
void core::negate_relation(unsigned j, const rational& a) {
SASSERT(vvr(j) != a);
if (vvr(j) < a) {
SASSERT(val(j) != a);
if (val(j) < a) {
mk_ineq(j, llc::GE, a);
}
else {

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

@ -96,17 +96,15 @@ public:
bool ineq_holds(const ineq& n) const;
bool lemma_holds(const lemma& l) const;
rational vvr(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
rational vvr(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
rational val(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
lpvar var(monomial const& sv) const { return sv.var(); }
rational vvr_rooted(const monomial& m) const { return m.rsign()*vvr(m.var()); }
rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
rational vvr(const factor& f) const { return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
rational val(const factor& f) const { return f.is_var()? val(f.var()) : val(m_emons[f.var()]); }
lpvar var(const factor& f) const { return f.var(); }
@ -227,7 +225,7 @@ public:
bool zero_is_an_inner_point_of_bounds(lpvar j) const;
int rat_sign(const monomial& m) const;
inline int rat_sign(lpvar j) const { return nla::rat_sign(vvr(j)); }
inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); }
bool sign_contradiction(const monomial& m) const;

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

@ -36,9 +36,9 @@ void monotone::monotonicity_lemma() {
void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
rational av = vvr(a);
rational av = val(a);
rational as = rational(nla::rat_sign(av));
rational bv = vvr(b);
rational bv = val(b);
rational bs = rational(nla::rat_sign(bv));
TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
SASSERT(as*av <= bs*bv);
@ -56,9 +56,9 @@ void monotone::assert_abs_val_a_le_abs_var_b(
bool strict) {
lpvar aj = var(a);
lpvar bj = var(b);
rational av = vvr(aj);
rational av = val(aj);
rational as = rational(nla::rat_sign(av));
rational bv = vvr(bj);
rational bv = val(bj);
rational bs = rational(nla::rat_sign(bv));
// TRACE("nla_solver", tout << "rmv = " << rmv << ", jv = " << jv << "\n";);
mk_ineq(as, aj, llc::LT); // |aj| < 0
@ -67,9 +67,9 @@ void monotone::assert_abs_val_a_le_abs_var_b(
}
void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
rational av = vvr(a);
rational av = val(a);
rational as = rational(nla::rat_sign(av));
rational bv = vvr(b);
rational bv = val(b);
rational bs = rational(nla::rat_sign(bv));
TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
SASSERT(as*av < bs*bv);
@ -83,7 +83,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
if (c().mon_has_zero(m.vars()))
return;
const rational prod_val = abs(c().product_value(m.vars()));
const rational m_val = abs(vvr(m));
const rational m_val = abs(val(m));
if (m_val < prod_val)
monotonicity_lemma_lt(m, prod_val);
else if (m_val > prod_val)
@ -102,9 +102,9 @@ void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val
/** \brief enforce the inequality |m| >= product |m[i]| .
/\_i |m[i]| >= |vvr(m[i])| => |m| >= |product_i vvr(m[i])|
/\_i |m[i]| >= |val(m[i])| => |m| >= |product_i val(m[i])|
<=>
\/_i |m[i]| < |vvr(m[i])} or |m| >= |product_i vvr(m[i])|
\/_i |m[i]| < |val(m[i])} or |m| >= |product_i val(m[i])|
*/
void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
add_empty_lemma();

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

@ -63,8 +63,8 @@ void order::order_lemma_on_rmonomial(const monomial& m) {
void order::order_lemma_on_binomial(const monomial& ac) {
TRACE("nla_solver", tout << pp_mon(c(), ac););
SASSERT(!check_monomial(ac) && ac.size() == 2);
const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]);
const rational acv = vvr(ac);
const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]);
const rational acv = val(ac);
bool gt = acv > mult_val;
bool k = false;
do {
@ -75,13 +75,13 @@ void order::order_lemma_on_binomial(const monomial& ac) {
}
void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
SASSERT(gt == (vvr(m) > vvr(m.vars()[0]) * vvr(m.vars()[1])));
SASSERT(gt == (val(m) > val(m.vars()[0]) * val(m.vars()[1])));
order_lemma_on_binomial_sign(m, m.vars()[k], m.vars()[!k], gt ? 1: -1);
}
/**
\brief
sign = the sign of vvr(xy) - vvr(x) * vvr(y) != 0
sign = the sign of val(xy) - val(x) * val(y) != 0
y <= 0 or x < a or xy >= ay
y <= 0 or x > a or xy <= ay
y >= 0 or x < a or xy <= ay
@ -90,11 +90,11 @@ void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
*/
void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(vvr(y));
int sy = rat_sign(val(y));
add_empty_lemma();
mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy
mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , vvr(x));
mk_ineq(xy.var(), - vvr(x), y, sign == 1 ? llc::LE : llc::GE);
mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x));
mk_ineq(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE);
TRACE("nla_solver", print_lemma(tout););
}
// m's size is 2 and m = m[k]a[!k] if k is false and m = m[!k]a[k] if k is true
@ -127,12 +127,12 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const mono
lpvar a = ac.vars()[p];
lpvar c = ac.vars()[k];
SASSERT(_().m_evars.find(c).var() == d);
rational acv = vvr(ac);
rational av = vvr(a);
rational c_sign = rrat_sign(vvr(c));
rational d_sign = rrat_sign(vvr(d));
rational bdv = vvr(bd);
rational bv = vvr(b);
rational acv = val(ac);
rational av = val(a);
rational c_sign = rrat_sign(val(c));
rational d_sign = rrat_sign(val(d));
rational bdv = val(bd);
rational bv = val(b);
auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
// suppose ac >= bd, then ac/|c| >= bd/|d|.
@ -193,11 +193,11 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
rational sign = m.rsign();
for (factor f: ab)
sign *= _().canonize_sign(f);
const rational fv = vvr(ab[0]) * vvr(ab[1]);
const rational mv = sign * vvr(m);
const rational fv = val(ab[0]) * val(ab[1]);
const rational mv = sign * val(m);
TRACE("nla_solver",
tout << "ab.size()=" << ab.size() << "\n";
tout << "we should have sign*vvr(m):" << mv << "=(" << sign << ")*(" << vvr(m) <<") to be equal to " << " vvr(ab[0])*vvr(ab[1]):" << fv << "\n";);
tout << "we should have sign*val(m):" << mv << "=(" << sign << ")*(" << val(m) <<") to be equal to " << " val(ab[0])*val(ab[1]):" << fv << "\n";);
if (mv == fv)
return;
bool gt = mv > fv;
@ -256,7 +256,7 @@ void order::generate_ol(const monomial& ac,
void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b) {
rational b_fs = canonize_sign(b);
llc cmp = a_sign*vvr(a) < b_sign*vvr(b)? llc::GE : llc::LE;
llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
mk_ineq(a_sign, a, - b_fs*b_sign, var(b), cmp);
}
@ -266,13 +266,13 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
const factor& c,
const monomial& bc,
const factor& b) {
auto cv = vvr(c);
auto cv = val(c);
int c_sign = nla::rat_sign(cv);
SASSERT(c_sign != 0);
auto av_c_s = vvr(a)*rational(c_sign);
auto bv_c_s = vvr(b)*rational(c_sign);
auto acv = vvr(ac);
auto bcv = vvr(bc);
auto av_c_s = val(a)*rational(c_sign);
auto bv_c_s = val(b)*rational(c_sign);
auto acv = val(ac);
auto bcv = val(bc);
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
// Suppose ac >= bc, then ac/|c| >= bc/|c|.
// Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s
@ -291,51 +291,51 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0
*/
void order::order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * vvr(m) > vvr(a) * vvr(b));
SASSERT(sign * val(m) > val(a) * val(b));
add_empty_lemma();
if (vvr(a).is_pos()) {
if (val(a).is_pos()) {
TRACE("nla_solver", tout << "a is pos\n";);
//negate a > 0
mk_ineq(a, llc::LE);
// negate b <= vvr(b)
mk_ineq(b, llc::GT, vvr(b));
// ab <= vvr(b)a
mk_ineq(sign, m.var(), -vvr(b), a, llc::LE);
// negate b <= val(b)
mk_ineq(b, llc::GT, val(b));
// ab <= val(b)a
mk_ineq(sign, m.var(), -val(b), a, llc::LE);
} else {
TRACE("nla_solver", tout << "a is neg\n";);
SASSERT(vvr(a).is_neg());
SASSERT(val(a).is_neg());
//negate a < 0
mk_ineq(a, llc::GE);
// negate b >= vvr(b)
mk_ineq(b, llc::LT, vvr(b));
// ab <= vvr(b)a
mk_ineq(sign, m.var(), -vvr(b), a, llc::LE);
// negate b >= val(b)
mk_ineq(b, llc::LT, val(b));
// ab <= val(b)a
mk_ineq(sign, m.var(), -val(b), a, llc::LE);
}
}
// we need to deduce ab >= vvr(b)*a
// we need to deduce ab >= val(b)*a
/**
\brief Add lemma:
a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0
a < 0 & b <= value(b) => sign*ab >= value(b)*a if value(a) < 0
*/
void order::order_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar a, lpvar b) {
SASSERT(sign * vvr(m) < vvr(a) * vvr(b));
SASSERT(sign * val(m) < val(a) * val(b));
add_empty_lemma();
if (vvr(a).is_pos()) {
if (val(a).is_pos()) {
//negate a > 0
mk_ineq(a, llc::LE);
// negate b >= vvr(b)
mk_ineq(b, llc::LT, vvr(b));
// ab <= vvr(b)a
mk_ineq(sign, m.var(), -vvr(b), a, llc::GE);
// negate b >= val(b)
mk_ineq(b, llc::LT, val(b));
// ab <= val(b)a
mk_ineq(sign, m.var(), -val(b), a, llc::GE);
} else {
SASSERT(vvr(a).is_neg());
SASSERT(val(a).is_neg());
//negate a < 0
mk_ineq(a, llc::GE);
// negate b <= vvr(b)
mk_ineq(b, llc::GT, vvr(b));
// ab >= vvr(b)a
mk_ineq(sign, m.var(), -vvr(b), a, llc::GE);
// negate b <= val(b)
mk_ineq(b, llc::GT, val(b));
// ab >= val(b)a
mk_ineq(sign, m.var(), -val(b), a, llc::GE);
}
}

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

@ -55,7 +55,7 @@ private:
a < 0 & b >= value(b) => sign*ab <= value(b)*a if value(a) < 0
*/
void order_lemma_on_ab_gt(const monomial& m, const rational& sign, lpvar a, lpvar b);
// we need to deduce ab >= vvr(b)*a
// we need to deduce ab >= val(b)*a
/**
\brief Add lemma:
a > 0 & b >= value(b) => sign*ab >= value(b)*a if value(a) > 0

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

@ -21,7 +21,7 @@
#include "util/lp/nla_core.h"
namespace nla {
template <typename T> rational tangents::vvr(T const& t) const { return m_core->vvr(t); }
template <typename T> rational tangents::val(T const& t) const { return m_core->val(t); }
tangents::tangents(core * c) : common(c) {}
@ -36,7 +36,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
c().add_empty_lemma();
const rational v = c().product_value(m.vars());
const rational mv = vvr(m);
const rational mv = val(m);
SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(nla::rat_sign(mv));
@ -47,7 +47,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
bool gt = abs(mv) > abs(v);
if (gt) {
for (lpvar j : m.vars()) {
const rational jv = vvr(j);
const rational jv = val(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT);
c().mk_ineq(js, j, llc::GT, jv);
@ -55,7 +55,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
c().mk_ineq(sign, m.var(), llc::LE, std::max(v, rational(-1)));
} else {
for (lpvar j : m.vars()) {
const rational jv = vvr(j);
const rational jv = val(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
}
@ -95,11 +95,11 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
c().negate_relation(jy, b);
bool sbelow = j_sign.is_pos()? below: !below;
#if Z3DEBUG
int mult_sign = nla::rat_sign(a - vvr(jx))*nla::rat_sign(b - vvr(jy));
int mult_sign = nla::rat_sign(a - val(jx))*nla::rat_sign(b - val(jy));
SASSERT((mult_sign == 1) == sbelow);
// If "mult_sign is 1" then (a - x)(b-y) > 0 and ab - bx - ay + xy > 0
// or -ab + bx + ay < xy or -ay - bx + xy > -ab
// j_sign*vvr(j) stands for xy. So, finally we have -ay - bx + j_sign*j > - ab
// j_sign*val(j) stands for xy. So, finally we have -ay - bx + j_sign*j > - ab
#endif
lp::lar_term t;
@ -110,12 +110,12 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
}
void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* rm){
point a, b;
point xy (vvr(bf.m_x), vvr(bf.m_y));
point xy (val(bf.m_x), val(bf.m_y));
rational correct_mult_val = xy.x * xy.y;
rational val = vvr(j) * sign;
bool below = val < correct_mult_val;
rational v = val(j) * sign;
bool below = v < correct_mult_val;
TRACE("nla_solver", tout << "rm = " << rm << ", below = " << below << std::endl; );
get_tang_points(a, b, below, val, xy);
get_tang_points(a, b, below, v, xy);
TRACE("nla_solver", tout << "sign = " << sign << ", tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;);
unsigned lemmas_size_was = c().m_lemma_vec->size();
generate_two_tang_lines(bf, xy, sign, j);

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

@ -80,7 +80,7 @@ private:
const rational & correct_val,
const rational & val,
bool below) const;
template <typename T> rational vvr(T const& t) const;
template <typename T> rational val(T const& t) const;
template <typename T> lpvar var(T const& t) const { return t.var(); }
}; // end of tangents
}

4
src/util/lp/vars_equivalence.h
View file

@ -64,11 +64,11 @@ struct vars_equivalence {
// If m_tree[v] == -1 then the variable is a root.
// if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
vector<equiv> m_equivs; // all equivalences extracted from constraints
std::function<rational(lpvar)> m_vvr;
std::function<rational(lpvar)> m_val;
// constructor
vars_equivalence(std::function<rational(lpvar)> vvr) : m_vvr(vvr) {}
vars_equivalence(std::function<rational(lpvar)> val) : m_val(val) {}
void clear() {
m_equivs.clear();