mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

debug emons

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-19 15:51:08 -07:00
parent ef6fd1cf8e
commit 1ab3957eea
19 changed files with 203 additions and 196 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/util/lp/emonomials.cpp
View file

@ -132,7 +132,8 @@ namespace nla {
return m_use_lists[v].m_head;
}
signed_vars const* emonomials::find_canonical(svector<lpvar> const& vars) const {
smon const* emonomials::find_canonical(svector<lpvar> const& vars) const {
SASSERT(m_ve.is_root(vars));
// find a unique key for dummy monomial
lpvar v = m_var2index.size();
for (unsigned i = 0; i < m_var2index.size(); ++i) {
@ -143,10 +144,10 @@ namespace nla {
}
unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr()));
m_canonized.push_back(signed_vars_ts(v, idx));
m_canonized.push_back(smon_ts(v, idx));
m_var2index.setx(v, idx, UINT_MAX);
do_canonize(m_monomials[idx]);
signed_vars const* result = nullptr;
smon const* result = nullptr;
lpvar w;
if (m_cg_table.find(v, w)) {
SASSERT(w != v);
@ -179,7 +180,7 @@ namespace nla {
}
void emonomials::remove_cg(unsigned idx, monomial const& m) {
signed_vars_ts& sv = m_canonized[idx];
smon_ts& sv = m_canonized[idx];
unsigned next = sv.m_next;
unsigned prev = sv.m_prev;
@ -203,7 +204,7 @@ namespace nla {
/**
\brief insert canonized monomials using v into a congruence table.
Prior to insertion, the monomials are canonized according to the current
variable equivalences. The canonized monomials (signed_vars) are considered
variable equivalences. The canonized monomials (smon) are considered
in the same equivalence class if they have the same set of representative
variables. Their signs may differ.
*/
@ -258,13 +259,13 @@ namespace nla {
\brief insert a new monomial.
Assume that the variables are canonical, that is, not equal in current
context so another variable. The monomial is inserted into a congruence
context to another variable. The monomial is inserted into a congruence
class of equal up-to var_eqs monomials.
*/
void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, sz, vs));
m_canonized.push_back(signed_vars_ts(v, idx));
m_canonized.push_back(smon_ts(v, idx));
lpvar last_var = UINT_MAX;
for (unsigned i = 0; i < sz; ++i) {
lpvar w = vs[i];
@ -282,7 +283,7 @@ namespace nla {
void emonomials::do_canonize(monomial const& mon) const {
unsigned index = m_var2index[mon.var()];
signed_vars& svs = m_canonized[index];
smon& svs = m_canonized[index];
svs.reset();
for (lpvar v : mon) {
svs.push_var(m_ve.find(v));
@ -292,8 +293,8 @@ namespace nla {
bool emonomials::canonize_divides(monomial const& m1, monomial const& m2) const {
if (m1.size() > m2.size()) return false;
signed_vars const& s1 = canonize(m1);
signed_vars const& s2 = canonize(m2);
smon const& s1 = canonize(m1);
smon const& s2 = canonize(m2);
unsigned sz1 = s1.size(), sz2 = s2.size();
unsigned i = 0, j = 0;
while (true) {

30
src/util/lp/emonomials.h
View file

@ -31,12 +31,12 @@ namespace nla {
\brief class used to summarize the coefficients to a monomial after
canonization with respect to current equalities.
*/
class signed_vars {
class smon {
lpvar m_var; // variable representing original monomial
svector<lpvar> m_vars;
bool m_sign;
public:
signed_vars(lpvar v) : m_var(v), m_sign(false) {}
smon(lpvar v) : m_var(v), m_sign(false) {}
lpvar var() const { return m_var; }
svector<lpvar> const& vars() const { return m_vars; }
svector<lp::var_index>::const_iterator begin() const { return vars().begin(); }
@ -58,7 +58,7 @@ namespace nla {
}
};
inline std::ostream& operator<<(std::ostream& out, signed_vars const& m) { return m.display(out); }
inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); }
class emonomials : public var_eqs_merge_handler {
@ -86,9 +86,9 @@ namespace nla {
/**
\brief private fields used by emonomials for maintaining state of canonized monomials.
*/
class signed_vars_ts : public signed_vars {
class smon_ts : public smon {
public:
signed_vars_ts(lpvar v, unsigned idx): signed_vars(v), m_next(idx), m_prev(idx), m_visited(0) {}
smon_ts(lpvar v, unsigned idx): smon(v), m_next(idx), m_prev(idx), m_visited(0) {}
unsigned m_next; // next congruent node.
unsigned m_prev; // previous congruent node
mutable unsigned m_visited;
@ -120,7 +120,7 @@ namespace nla {
unsigned_vector m_lim; // backtracking point
mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator
region m_region; // region for allocating linked lists
mutable vector<signed_vars_ts> m_canonized; // canonized versions of signed variables
mutable vector<smon_ts> m_canonized; // canonized versions of signed variables
mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur.
hash_canonical m_cg_hash;
eq_canonical m_cg_eq;
@ -189,14 +189,14 @@ namespace nla {
/**
\brief retrieve canonized monomial corresponding to variable v from definition v := vs
*/
signed_vars const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
smon const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
class canonical {
emonomials& m;
public:
canonical(emonomials& m): m(m) {}
signed_vars const& operator[](lpvar v) const { return m.var2canonical(v); }
signed_vars const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
smon const& operator[](lpvar v) const { return m.var2canonical(v); }
smon const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
};
canonical canonical;
@ -205,13 +205,13 @@ namespace nla {
\brief obtain a canonized signed monomial
corresponding to current equivalence class.
*/
signed_vars const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
smon const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
/**
\brief obtain the representative canonized monomial up to sign.
*/
//signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
signed_vars const& rep(signed_vars const& sv) const {
//smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
smon const& rep(smon const& sv) const {
unsigned j = -1;
m_cg_table.find(sv.var(), j);
return m_canonized[m_var2index[j]];
@ -220,7 +220,7 @@ namespace nla {
/**
\brief the original sign is defined as a sign of the equivalence class representative.
*/
rational orig_sign(signed_vars const& sv) const { return rep(sv).rsign(); }
rational orig_sign(smon const& sv) const { return rep(sv).rsign(); }
/**
\brief determine if m1 divides m2 over the canonization obtained from merged variables.
@ -301,7 +301,7 @@ namespace nla {
factors_of get_factors_of(monomial const& m) const { inc_visited(); return factors_of(*this, m); }
factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); }
signed_vars const* find_canonical(svector<lpvar> const& vars) const;
smon const* find_canonical(svector<lpvar> const& vars) const;
/**
\brief iterator over sign equivalent monomials.
@ -350,7 +350,7 @@ namespace nla {
sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) { return sign_equiv_monomials(*this, m); }
sign_equiv_monomials enum_sign_equiv_monomials(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
sign_equiv_monomials enum_sign_equiv_monomials(signed_vars const& sv) { return enum_sign_equiv_monomials(sv.var()); }
sign_equiv_monomials enum_sign_equiv_monomials(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); }
/**
\brief display state of emonomials

2
src/util/lp/factorization_factory_imp.cpp
View file

@ -21,7 +21,7 @@
#include "util/lp/nla_core.h"
namespace nla {
factorization_factory_imp::factorization_factory_imp(const signed_vars& rm, const core& s) :
factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) :
factorization_factory(rm.vars(), &s.m_emons[rm.var()]),
m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }

6
src/util/lp/factorization_factory_imp.h
View file

@ -21,14 +21,14 @@
#include "util/lp/factorization.h"
namespace nla {
class core;
class signed_vars;
class smon;
struct factorization_factory_imp: factorization_factory {
const core& m_core;
const monomial & m_mon;
const signed_vars& m_rm;
const smon& m_rm;
factorization_factory_imp(const signed_vars& rm, const core& s);
factorization_factory_imp(const smon& rm, const core& s);
bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
};

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

@ -246,6 +246,7 @@ public:
void clear();
lar_solver();
void set_track_pivoted_rows(bool v);
bool get_track_pivoted_rows() const;

63
src/util/lp/monomial.h
View file

@ -1,7 +1,7 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Nikolaj Bjorner
Lev Nachmanson
Lev Nachmanson
*/
#pragma once
@ -10,33 +10,33 @@
#include "util/lp/lar_solver.h"
namespace nla {
/*
* represents definition m_v = v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn]
*/
class monomial {
// fields
lp::var_index m_v;
svector<lp::var_index> m_vs;
public:
// constructors
monomial(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) {
std::sort(m_vs.begin(), m_vs.end());
}
monomial(lp::var_index v, const svector<lp::var_index> &vs):
m_v(v), m_vs(vs) {
std::sort(m_vs.begin(), m_vs.end());
}
monomial() {}
/*
* represents definition m_v = v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn]
*/
class monomial {
// fields
lp::var_index m_v;
svector<lp::var_index> m_vs;
public:
// constructors
monomial(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) {
std::sort(m_vs.begin(), m_vs.end());
}
monomial(lp::var_index v, const svector<lp::var_index> &vs):
m_v(v), m_vs(vs) {
std::sort(m_vs.begin(), m_vs.end());
}
monomial() {}
unsigned var() const { return m_v; }
unsigned size() const { return m_vs.size(); }
unsigned operator[](unsigned idx) const { return m_vs[idx]; }
svector<lp::var_index>::const_iterator begin() const { return m_vs.begin(); }
svector<lp::var_index>::const_iterator end() const { return m_vs.end(); }
const svector<lp::var_index>& vars() const { return m_vs; }
bool empty() const { return m_vs.empty(); }
unsigned var() const { return m_v; }
unsigned size() const { return m_vs.size(); }
unsigned operator[](unsigned idx) const { return m_vs[idx]; }
svector<lp::var_index>::const_iterator begin() const { return m_vs.begin(); }
svector<lp::var_index>::const_iterator end() const { return m_vs.end(); }
const svector<lp::var_index>& vars() const { return m_vs; }
bool empty() const { return m_vs.empty(); }
std::ostream& display(std::ostream& out) const {
out << "v" << var() << " := ";
@ -48,16 +48,17 @@ namespace nla {
};
inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
SASSERT(false);
return m.display(out);
}
typedef std::unordered_map<lp::var_index, rational> variable_map_type;
bool check_assignment(monomial const& m, variable_map_type & vars);
bool check_assignment(monomial const& m, variable_map_type & vars);
bool check_assignments(const vector<monomial> & monomimials,
const lp::lar_solver& s,
variable_map_type & vars);
bool check_assignments(const vector<monomial> & monomimials,
const lp::lar_solver& s,
variable_map_type & vars);

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

@ -122,11 +122,11 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
}
const monomial& m_v = c().m_emons[v];
signed_vars const& sv_v = c().m_emons.canonical[v];
TRACE("nla_solver_details", tout << "mon = " << m_v;);
smon const& sv_v = c().m_emons.canonical[v];
TRACE("nla_solver_details", tout << "mon = " << pp_mon(c(), m_v););
for (auto const& m_w : c().m_emons.enum_sign_equiv_monomials(v)) {
signed_vars const& sv_w = c().m_emons.canonical[m_w];
smon const& sv_w = c().m_emons.canonical[m_w];
if (m_v.var() != m_w.var() && basic_sign_lemma_on_two_monomials(m_v, m_w, sv_v.rsign() * sv_w.rsign()) && done())
return true;
}
@ -222,7 +222,7 @@ void basics::negate_strict_sign(lpvar j) {
// here we use the fact
// xy = 0 -> x = 0 or y = 0
bool basics::basic_lemma_for_mon_zero(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_zero(const smon& rm, const factorization& f) {
NOT_IMPLEMENTED_YET();
return true;
#if 0
@ -251,7 +251,7 @@ bool basics::basic_lemma(bool derived) {
unsigned sz = rm_ref.size();
for (unsigned j = 0; j < sz; ++j) {
lpvar v = rm_ref[(j + start) % rm_ref.size()];
const signed_vars& r = c().m_emons.canonical[v];
const smon& r = c().m_emons.canonical[v];
SASSERT (!c().check_monomial(c().m_emons[v]));
basic_lemma_for_mon(r, derived);
}
@ -261,13 +261,13 @@ bool basics::basic_lemma(bool derived) {
// Use basic multiplication properties to create a lemma
// for the given monomial.
// "derived" means derived from constraints - the alternative is model based
void basics::basic_lemma_for_mon(const signed_vars& rm, bool derived) {
void basics::basic_lemma_for_mon(const smon& rm, bool derived) {
if (derived)
basic_lemma_for_mon_derived(rm);
else
basic_lemma_for_mon_model_based(rm);
}
bool basics::basic_lemma_for_mon_derived(const signed_vars& rm) {
bool basics::basic_lemma_for_mon_derived(const smon& rm) {
if (c().var_is_fixed_to_zero(var(rm))) {
for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty())
@ -293,7 +293,7 @@ bool basics::basic_lemma_for_mon_derived(const signed_vars& rm) {
return false;
}
// x = 0 or y = 0 -> xy = 0
bool basics::basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_non_zero_derived(const smon& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
if (! c().var_is_separated_from_zero(var(rm)))
return false;
@ -317,7 +317,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const f
}
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
lpvar mon_var = c().m_emons[rm.var()].var();
@ -377,7 +377,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed
}
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const smon& rm, const factorization& f) {
return false;
rational sign = c().m_emons.orig_sign(rm);
lpvar not_one = -1;
@ -424,7 +424,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const
return true;
}
bool basics::basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const factorization& factorization) {
bool basics::basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization) {
return
basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization) ||
basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(rm, factorization);
@ -432,7 +432,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const fa
}
// x != 0 or y = 0 => |xy| >= |y|
void basics::proportion_lemma_model_based(const signed_vars& rm, const factorization& factorization) {
void basics::proportion_lemma_model_based(const smon& rm, const factorization& factorization) {
rational rmv = abs(vvr(rm));
if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization));
@ -448,7 +448,7 @@ void basics::proportion_lemma_model_based(const signed_vars& rm, const factoriza
}
}
// x != 0 or y = 0 => |xy| >= |y|
bool basics::proportion_lemma_derived(const signed_vars& rm, const factorization& factorization) {
bool basics::proportion_lemma_derived(const smon& rm, const factorization& factorization) {
return false;
rational rmv = abs(vvr(rm));
if (rmv.is_zero()) {
@ -489,7 +489,7 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
// none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm|
void basics::generate_pl(const signed_vars& rm, const factorization& fc, int factor_index) {
void basics::generate_pl(const smon& rm, const factorization& fc, int factor_index) {
TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
tout << rm;
tout << "fc = "; c().print_factorization(fc, tout);
@ -523,7 +523,7 @@ void basics::generate_pl(const signed_vars& rm, const factorization& fc, int fac
TRACE("nla_solver", c().print_lemma(tout); );
}
// here we use the fact xy = 0 -> x = 0 or y = 0
void basics::basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const factorization& f) {
void basics::basic_lemma_for_mon_zero_model_based(const smon& 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));
add_empty_lemma();
@ -544,7 +544,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const f
TRACE("nla_solver", c().print_lemma(tout););
}
void basics::basic_lemma_for_mon_model_based(const signed_vars& rm) {
void basics::basic_lemma_for_mon_model_based(const smon& rm) {
TRACE("nla_solver_bl", tout << "rm = " << rm;);
if (vvr(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) {
@ -664,7 +664,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const smon& rm, const factorization& f) {
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
lpvar mon_var = c().m_emons[rm.var()].var();
@ -722,7 +722,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const si
return true;
}
void basics::basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f) {
void basics::basic_lemma_for_mon_neutral_model_based(const smon& rm, const factorization& f) {
if (f.is_mon()) {
basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(*f.mon());
basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(*f.mon());
@ -734,7 +734,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, cons
}
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const signed_vars& rm, const factorization& f) {
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const smon& rm, const factorization& f) {
rational sign = c().m_emons.orig_sign(rm);
TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
lpvar not_one = -1;
@ -815,7 +815,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
}
// x = 0 or y = 0 -> xy = 0
void basics::basic_lemma_for_mon_non_zero_model_based(const signed_vars& rm, const factorization& f) {
void basics::basic_lemma_for_mon_non_zero_model_based(const smon& rm, const factorization& f) {
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
if (f.is_mon())
basic_lemma_for_mon_non_zero_model_based_mf(f);

34
src/util/lp/nla_basics_lemmas.h
View file

@ -40,47 +40,47 @@ struct basics: common {
-ab = a(-b)
*/
bool basic_sign_lemma(bool derived);
bool basic_lemma_for_mon_zero(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_zero(const smon& rm, const factorization& f);
void basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const factorization& f);
void basic_lemma_for_mon_zero_model_based(const smon& rm, const factorization& f);
void basic_lemma_for_mon_non_zero_model_based(const signed_vars& rm, const factorization& f);
void basic_lemma_for_mon_non_zero_model_based(const smon& rm, const factorization& f);
// x = 0 or y = 0 -> xy = 0
void basic_lemma_for_mon_non_zero_model_based_rm(const signed_vars& rm, const factorization& f);
void basic_lemma_for_mon_non_zero_model_based_rm(const smon& rm, const factorization& f);
void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f);
// x = 0 or y = 0 -> xy = 0
bool basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_non_zero_derived(const smon& rm, const factorization& f);
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const smon& rm, const factorization& f);
// use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m);
bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon& rm, const factorization& f);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const smon& rm, const factorization& f);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m);
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const signed_vars& rm, const factorization& f);
void basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f);
bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const smon& rm, const factorization& f);
void basic_lemma_for_mon_neutral_model_based(const smon& rm, const factorization& f);
bool basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const factorization& factorization);
bool basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization);
void basic_lemma_for_mon_model_based(const signed_vars& rm);
void basic_lemma_for_mon_model_based(const smon& rm);
bool basic_lemma_for_mon_derived(const signed_vars& rm);
bool basic_lemma_for_mon_derived(const smon& rm);
// Use basic multiplication properties to create a lemma
// for the given monomial.
// "derived" means derived from constraints - the alternative is model based
void basic_lemma_for_mon(const signed_vars& rm, bool derived);
void basic_lemma_for_mon(const smon& rm, bool derived);
// use basic multiplication properties to create a lemma
bool basic_lemma(bool derived);
void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign);
@ -94,14 +94,14 @@ struct basics: common {
void add_fixed_zero_lemma(const monomial& m, lpvar j);
void negate_strict_sign(lpvar j);
// x != 0 or y = 0 => |xy| >= |y|
void proportion_lemma_model_based(const signed_vars& rm, const factorization& factorization);
void proportion_lemma_model_based(const smon& rm, const factorization& factorization);
// x != 0 or y = 0 => |xy| >= |y|
bool proportion_lemma_derived(const signed_vars& rm, const factorization& factorization);
bool proportion_lemma_derived(const smon& rm, const factorization& factorization);
// if there are no zero factors then |m| >= |m[factor_index]|
void generate_pl_on_mon(const monomial& m, unsigned factor_index);
// none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm|
void generate_pl(const signed_vars& rm, const factorization& fc, int factor_index);
void generate_pl(const smon& rm, const factorization& fc, int factor_index);
};
}

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

@ -28,24 +28,25 @@ template <typename T> void common::explain(const T& t) {
}
template void common::explain<monomial>(const monomial& t);
template void common::explain<factor>(const factor& t);
template void common::explain<signed_vars>(const signed_vars& t);
template void common::explain<smon>(const smon& t);
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<signed_vars>(signed_vars const& t) const;
template rational common::vvr<smon>(smon 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> lpvar common::var(T const& t) const { return c().var(t); }
template lpvar common::var<factor>(factor const& t) const;
template lpvar common::var<signed_vars>(signed_vars const& t) const;
template lpvar common::var<smon>(smon const& t) const;
void common::add_empty_lemma() { c().add_empty_lemma(); }
template <typename T> rational common::canonize_sign(const T& t) const {
return c().canonize_sign(t);
}
template rational common::canonize_sign<signed_vars>(const signed_vars& t) const;
template rational common::canonize_sign<smon>(const smon& 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);
@ -99,17 +100,17 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
template
std::ostream& common::print_product<monomial>(const monomial & m, std::ostream& out) const;
template std::ostream& common::print_product<signed_vars>(const signed_vars & m, std::ostream& out) const;
template std::ostream& common::print_product<smon>(const smon & m, std::ostream& out) const;
std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
return c().print_monomial(m, out);
}
//std::ostream& common::print_rooted_monomial(const signed_vars& rm, std::ostream& out) const {
//std::ostream& common::print_rooted_monomial(const smon& rm, std::ostream& out) const {
// return c().print_rooted_monomial(rm, out);
//}
//std::ostream& common::print_rooted_monomial_with_vars(const signed_vars& rm, std::ostream& out) const {
//std::ostream& common::print_rooted_monomial_with_vars(const smon& rm, std::ostream& out) const {
// return c().print_rooted_monomial_with_vars(rm, out);
//}
std::ostream& common::print_factor(const factor & f, std::ostream& out) const {

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

@ -84,8 +84,8 @@ struct common {
std::ostream& print_var(lpvar, std::ostream& out) const;
std::ostream& print_monomial(const monomial & m, std::ostream& out) const;
std::ostream& print_rooted_monomial(const signed_vars &, std::ostream& out) const;
std::ostream& print_rooted_monomial_with_vars(const signed_vars&, std::ostream& out) const;
std::ostream& print_rooted_monomial(const smon &, std::ostream& out) const;
std::ostream& print_rooted_monomial_with_vars(const smon&, std::ostream& out) const;
bool check_monomial(const monomial&) const;
unsigned random();
};

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

@ -97,13 +97,10 @@ rational core::canonize_sign_of_var(lpvar j) const {
return m_evars.find(j).rsign();
}
rational core::canonize_sign(const signed_vars& m) const {
NOT_IMPLEMENTED_YET();
return rational::one();
rational core::canonize_sign(const smon& m) const {
return m.rsign();
}
// returns the monomial index
void core::add(lpvar v, unsigned sz, lpvar const* vs) {
m_emons.add(v, sz, vs);
}
@ -139,7 +136,7 @@ void core::explain(const monomial& m, lp::explanation& exp) const {
explain(j, exp);
}
void core::explain(const signed_vars& rm, lp::explanation& exp) const {
void core::explain(const smon& rm, lp::explanation& exp) const {
explain(m_emons[rm.var()], exp);
}
@ -165,7 +162,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
return out;
}
template std::ostream& core::print_product<monomial>(const monomial & m, std::ostream& out) const;
template std::ostream& core::print_product<signed_vars>(const signed_vars & m, std::ostream& out) const;
template std::ostream& core::print_product<smon>(const smon & m, std::ostream& out) const;
std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
if (f.is_var()) {
@ -781,12 +778,12 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o
bool core:: find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
SASSERT(vars_are_roots(vars));
signed_vars const* sv = m_emons.find_canonical(vars);
smon const* sv = m_emons.find_canonical(vars);
return sv && (i = sv->var(), true);
}
const monomial* core::find_monomial_of_vars(const svector<lpvar>& vars) const {
signed_vars const* sv = m_emons.find_canonical(vars);
smon const* sv = m_emons.find_canonical(vars);
return sv ? &m_emons[sv->var()] : nullptr;
}
@ -809,7 +806,7 @@ void core::explain_separation_from_zero(lpvar j) {
explain_existing_upper_bound(j);
}
int core::get_derived_sign(const signed_vars& rm, const factorization& f) const {
int core::get_derived_sign(const smon& 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) {
@ -821,7 +818,7 @@ int core::get_derived_sign(const signed_vars& rm, const factorization& f) const
}
return nla::rat_sign(sign);
}
void core::trace_print_monomial_and_factorization(const signed_vars& rm, const factorization& f, std::ostream& out) const {
void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const {
out << "rooted vars: ";
print_product(rm.vars(), out);
out << "\n";
@ -1410,7 +1407,7 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
if (abs(vvr(mc.vars()[i])) == rational(1)) {
auto vv = mc.vars();
vv.erase(vv.begin()+i);
signed_vars const* sv = m_emons.find_canonical(vv);
smon const* sv = m_emons.find_canonical(vv);
if (!sv) {
out << "nf length" << vv.size() << "\n"; ;
}
@ -1439,7 +1436,7 @@ void core::init_to_refine() {
TRACE("nla_solver",
tout << m_to_refine.size() << " mons to refine:\n";
for (lpvar v : m_to_refine) tout << m_emons[v] << "\n";);
for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << "\n";);
}
std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
@ -1465,7 +1462,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
return vars;
}
bool core::divide(const signed_vars& bc, const factor& c, factor & b) const {
bool core::divide(const smon& bc, const factor& c, factor & b) const {
svector<lpvar> c_vars = sorted_vars(c);
TRACE("nla_solver_div",
tout << "c_vars = ";
@ -1482,7 +1479,7 @@ bool core::divide(const signed_vars& bc, const factor& c, factor & b) const {
b = factor(b_vars[0], factor_type::VAR);
return true;
}
signed_vars const* sv = m_emons.find_canonical(b_vars);
smon const* sv = m_emons.find_canonical(b_vars);
if (!sv) {
TRACE("nla_solver_div", tout << "not in rooted";);
return false;
@ -1532,10 +1529,10 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
}
void core::trace_print_ol(const signed_vars& ac,
void core::trace_print_ol(const smon& ac,
const factor& a,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b,
std::ostream& out) {
out << "ac = " << ac << "\n";
@ -1584,7 +1581,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
bool core::rm_check(const signed_vars& rm) const {
bool core::rm_check(const smon& rm) const {
return check_monomial(m_emons[rm.var()]);
}
@ -1642,7 +1639,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
*/
bool core::find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf) {
bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) {
for (auto factorization : factorization_factory_imp(rm, *this)) {
if (factorization.size() == 2) {
auto a = factorization[0];
@ -1656,7 +1653,7 @@ bool core::find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf) {
return false;
}
bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found){
bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found){
rm_found = nullptr;
for (unsigned i: m_to_refine) {
const auto& rm = m_emons.canonical[i];
@ -1975,7 +1972,6 @@ lbool core::test_check(
return check(l);
}
template rational core::product_value<monomial>(const monomial & m) const;
} // end of nla

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

@ -102,9 +102,9 @@ public:
lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
lpvar var(signed_vars const& sv) const { return sv.var(); }
lpvar var(smon const& sv) const { return sv.var(); }
rational vvr(const signed_vars& rm) const { return vvr(m_emons[rm.var()]); } // NB: removed multiplication with sign.
rational vvr(const smon& rm) const { return rm.rsign()*vvr(m_emons[rm.var()]); }
rational vvr(const factor& f) const { return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
@ -112,7 +112,7 @@ public:
svector<lpvar> sorted_vars(const factor& f) const;
bool done() const;
void add_empty_lemma();
// the value of the factor is equal to the value of the variable multiplied
// by the canonize_sign
@ -120,12 +120,12 @@ public:
rational canonize_sign_of_var(lpvar j) const;
// the value of the rooted monomias is equal to the value of the variable multiplied
// 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 signed_vars& m) const;
rational canonize_sign(const smon& m) const;
void deregister_monomial_from_signed_varsomials (const monomial & m, unsigned i);
void deregister_monomial_from_smonomials (const monomial & m, unsigned i);
void deregister_monomial_from_tables(const monomial & m, unsigned i);
@ -142,7 +142,7 @@ public:
bool check_monomial(const monomial& m) const;
void explain(const monomial& m, lp::explanation& exp) const;
void explain(const signed_vars& rm, lp::explanation& exp) const;
void explain(const smon& rm, lp::explanation& exp) const;
void explain(const factor& f, lp::explanation& exp) const;
void explain(lpvar j, lp::explanation& exp) const;
void explain_existing_lower_bound(lpvar j);
@ -169,7 +169,7 @@ public:
std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
template <typename T>
void trace_print_rms(const T& p, std::ostream& out);
void trace_print_monomial_and_factorization(const signed_vars& rm, const factorization& f, std::ostream& out) const;
void trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const;
void print_monomial_stats(const monomial& m, std::ostream& out);
void print_stats(std::ostream& out);
std::ostream& print_lemma(std::ostream& out) const;
@ -177,10 +177,10 @@ public:
void print_specific_lemma(const lemma& l, std::ostream& out) const;
void trace_print_ol(const signed_vars& ac,
void trace_print_ol(const smon& ac,
const factor& a,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b,
std::ostream& out);
@ -243,7 +243,7 @@ public:
const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
int get_derived_sign(const signed_vars& rm, const factorization& f) const;
int get_derived_sign(const smon& rm, const factorization& f) const;
bool var_has_positive_lower_bound(lpvar j) const;
@ -312,7 +312,7 @@ public:
void init_to_refine();
bool divide(const signed_vars& bc, const factor& c, factor & b) const;
bool divide(const smon& bc, const factor& c, factor & b) const;
void negate_factor_equality(const factor& c, const factor& d);
@ -320,15 +320,15 @@ public:
std::unordered_set<lpvar> collect_vars(const lemma& l) const;
bool rm_check(const signed_vars&) const;
bool rm_check(const smon&) const;
std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
void add_abs_bound(lpvar v, llc cmp);
void add_abs_bound(lpvar v, llc cmp, rational const& bound);
bool find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf);
bool find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf);
bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found);
bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found);
void generate_simple_sign_lemma(const rational& sign, const monomial& m);
void negate_relation(unsigned j, const rational& a);

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

@ -33,13 +33,13 @@ void monotone::print_monotone_array(const vector<std::pair<std::vector<rational>
}
out << "}";
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm) {
const rational v = abs(vvr(rm));
const auto& key = lex_sorted[i].first;
TRACE("nla_solver", tout << "rm = " << rm << "i = " << i << std::endl;);
for (unsigned k = i + 1; k < lex_sorted.size(); k++) {
const auto& p = lex_sorted[k];
const signed_vars& rmk = c().m_emons.canonical[p.second];
const smon& rmk = c().m_emons.canonical[p.second];
const rational vk = abs(vvr(rmk));
TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
tout << "vk = " << vk << std::endl;);
@ -61,14 +61,14 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<
return false;
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm) {
const rational v = abs(vvr(rm));
const auto& key = lex_sorted[i].first;
TRACE("nla_solver", tout << "rm = " << rm << "i = " << i << std::endl;);
for (unsigned k = i; k-- > 0;) {
const auto& p = lex_sorted[k];
const signed_vars& rmk = c().m_emons.canonical[p.second];
const smon& rmk = c().m_emons.canonical[p.second];
const rational vk = abs(vvr(rmk));
TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
tout << "vk = " << vk << std::endl;);
@ -92,14 +92,14 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<
return false;
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm) {
return monotonicity_lemma_on_lex_sorted_rm_upper(lex_sorted, i, rm)
|| monotonicity_lemma_on_lex_sorted_rm_lower(lex_sorted, i, rm);
}
bool monotone::monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted) {
for (unsigned i = 0; i < lex_sorted.size(); i++) {
unsigned rmi = lex_sorted[i].second;
const signed_vars& rm = c().m_emons.canonical[rmi];
const smon& rm = c().m_emons.canonical[rmi];
TRACE("nla_solver", tout << rm << "\n, rm_check = " << c().rm_check(rm); tout << std::endl;);
if ((!c().rm_check(rm)) && monotonicity_lemma_on_lex_sorted_rm(lex_sorted, i, rm))
return true;
@ -107,7 +107,7 @@ bool monotone::monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vect
return false;
}
vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const signed_vars& a) const {
vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const smon& a) const {
vector<std::pair<rational, lpvar>> r;
for (lpvar j : a.vars()) {
r.push_back(std::make_pair(abs(vvr(j)), j));
@ -137,8 +137,8 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
}
// strict version
void monotone::generate_monl_strict(const signed_vars& a,
const signed_vars& b,
void monotone::generate_monl_strict(const smon& a,
const smon& b,
unsigned strict) {
add_empty_lemma();
auto akey = get_sorted_key_with_vars(a);
@ -159,8 +159,8 @@ void monotone::generate_monl_strict(const signed_vars& a,
}
void monotone::assert_abs_val_a_le_abs_var_b(
const signed_vars& a,
const signed_vars& b,
const smon& a,
const smon& b,
bool strict) {
lpvar aj = var(a);
lpvar bj = var(b);
@ -188,8 +188,8 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
// not a strict version
void monotone::generate_monl(const signed_vars& a,
const signed_vars& b) {
void monotone::generate_monl(const smon& a,
const smon& b) {
TRACE("nla_solver",
tout << "a = " << a << "\n:";
tout << "b = " << b << "\n:";);
@ -206,7 +206,7 @@ void monotone::generate_monl(const signed_vars& a,
TRACE("nla_solver", print_lemma(tout););
}
std::vector<rational> monotone::get_sorted_key(const signed_vars& rm) const {
std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
std::vector<rational> r;
for (unsigned j : rm.vars()) {
r.push_back(abs(vvr(j)));

16
src/util/lp/nla_monotone_lemmas.h
View file

@ -24,21 +24,21 @@ struct monotone: common {
monotone(core *core);
void print_monotone_array(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted,
std::ostream& out) const;
bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted);
bool monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms);
void monotonicity_lemma();
void monotonicity_lemma(monomial const& m);
void monotonicity_lemma_gt(const monomial& m, const rational& prod_val);
void monotonicity_lemma_lt(const monomial& m, const rational& prod_val);
void generate_monl_strict(const signed_vars& a, const signed_vars& b, unsigned strict);
void generate_monl(const signed_vars& a, const signed_vars& b);
std::vector<rational> get_sorted_key(const signed_vars& rm) const;
vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const signed_vars& a) const;
void generate_monl_strict(const smon& a, const smon& b, unsigned strict);
void generate_monl(const smon& a, const smon& b);
std::vector<rational> get_sorted_key(const smon& rm) const;
vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const smon& a) const;
void negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict);
void negate_abs_a_lt_abs_b(lpvar a, lpvar b);
void assert_abs_val_a_le_abs_var_b(const signed_vars& a, const signed_vars& b, bool strict);
void assert_abs_val_a_le_abs_var_b(const smon& a, const smon& b, bool strict);
};
}

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

@ -29,10 +29,10 @@ namespace nla {
// a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c
bool order::order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
const factorization& ac_f,
unsigned k,
const signed_vars& rm_bd) {
const smon& rm_bd) {
TRACE("nla_solver",
tout << "rm_ac = " << rm_ac << "\n";
tout << "rm_bd = " << rm_bd << "\n";
@ -44,7 +44,7 @@ bool order::order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[(k + 1) % 2], ac_f[k], rm_bd, b);
}
bool order::order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k) {
bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, unsigned k) {
const factor c = ac[k];
TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
if (c.is_var()) {
@ -65,7 +65,7 @@ bool order::order_lemma_on_ac_explore(const signed_vars& rm, const factorization
return false;
}
void order::order_lemma_on_factorization(const signed_vars& rm, const factorization& ab) {
void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) {
const monomial& m = _().m_emons[rm.var()];
TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
rational sign = _().m_emons.orig_sign(rm);
@ -90,11 +90,11 @@ void order::order_lemma_on_factorization(const signed_vars& rm, const factorizat
}
// |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
void order::generate_ol(const signed_vars& ac,
void order::generate_ol(const smon& ac,
const factor& a,
int c_sign,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b,
llc ab_cmp) {
add_empty_lemma();
@ -114,7 +114,7 @@ void order::generate_mon_ol(const monomial& ac,
lpvar a,
const rational& c_sign,
lpvar c,
const signed_vars& bd,
const smon& bd,
const factor& b,
const rational& d_sign,
lpvar d,
@ -142,15 +142,15 @@ void order::order_lemma() {
unsigned start = random();
unsigned sz = rm_ref.size();
for (unsigned i = sz; i-- > 0 && !done(); ) {
const signed_vars& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
order_lemma_on_rmonomial(rm);
}
}
bool order::order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
bool order::order_lemma_on_ac_and_bc_and_factors(const smon& ac,
const factor& a,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b) {
auto cv = vvr(c);
int c_sign = nla::rat_sign(cv);
@ -232,10 +232,10 @@ void order::order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a,
order_lemma_on_ab_lt(m, sign, a, b);
}
// a > b && c > 0 => ac > bc
void order::order_lemma_on_rmonomial(const signed_vars& rm) {
void order::order_lemma_on_rmonomial(const smon& rm) {
TRACE("nla_solver_details",
tout << "rm = "; print_product(rm, tout);
tout << ", orig = " << c().m_emons[rm.var()] << "\n";
tout << ", orig = " << pp_mon(c(), c().m_emons[rm.var()]);
);
for (auto ac : factorization_factory_imp(rm, c())) {
if (ac.size() != 2)
@ -267,7 +267,7 @@ void order::order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, i
TRACE("nla_solver", print_lemma(tout););
}
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd) {
signed_vars const& rm_bd = _().m_emons.canonical[bd];
smon const& rm_bd = _().m_emons.canonical[bd];
factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
factor b;
if (_().divide(rm_bd, d, b)) {
@ -275,7 +275,7 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, co
}
}
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d) {
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const smon& bd, const factor& b, lpvar d) {
TRACE("nla_solver", tout << "ac=" << pp_mon(c(), ac);
tout << "\nrm=" << bd;
print_factor(b, tout << ", b="); print_var(d, tout << ", d=") << "\n";);

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

@ -29,23 +29,23 @@ struct order: common {
const core& _() const { return *m_core; }
//constructor
order(core *c) : common(c) {}
bool order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
bool order_lemma_on_ac_and_bc_and_factors(const smon& ac,
const factor& a,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b);
// a >< b && c > 0 => ac >< bc
// a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c
bool order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
bool order_lemma_on_ac_and_bc(const smon& rm_ac,
const factorization& ac_f,
unsigned k,
const signed_vars& rm_bd);
const smon& rm_bd);
bool order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k);
bool order_lemma_on_ac_explore(const smon& rm, const factorization& ac, unsigned k);
void order_lemma_on_factorization(const signed_vars& rm, const factorization& ab);
void order_lemma_on_factorization(const smon& rm, const factorization& ab);
/**
\brief Add lemma:
@ -63,19 +63,19 @@ struct order: common {
void order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt);
void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k);
void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd);
void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d);
void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const smon& bd, const factor& b, lpvar d);
void order_lemma_on_binomial_k(const monomial& m, lpvar k, bool gt);
void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
void order_lemma_on_binomial(const monomial& ac);
void order_lemma_on_rmonomial(const signed_vars& rm);
void order_lemma_on_rmonomial(const smon& rm);
void order_lemma();
// |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
void generate_ol(const signed_vars& ac,
void generate_ol(const smon& ac,
const factor& a,
int c_sign,
const factor& c,
const signed_vars& bc,
const smon& bc,
const factor& b,
llc ab_cmp);
@ -83,7 +83,7 @@ struct order: common {
lpvar a,
const rational& c_sign,
lpvar c,
const signed_vars& bd,
const smon& bd,
const factor& b,
const rational& d_sign,
lpvar d,

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

@ -33,7 +33,7 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
out << "("; print_point(a, out); out << ", "; print_point(b, out); out << ")";
return out;
}
void tangents::generate_simple_tangent_lemma(const signed_vars* rm) {
void tangents::generate_simple_tangent_lemma(const smon* rm) {
if (rm->size() != 2)
return;
TRACE("nla_solver", tout << "rm:" << *rm << std::endl;);
@ -73,7 +73,7 @@ void tangents::tangent_lemma() {
bfc bf;
lpvar j;
rational sign;
const signed_vars* rm = nullptr;
const smon* rm = nullptr;
if (c().find_bfc_to_refine(bf, j, sign, rm)) {
tangent_lemma_bf(bf, j, sign, rm);
@ -84,7 +84,7 @@ void tangents::tangent_lemma() {
}
}
void tangents::generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp) {
void tangents::generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp) {
// here we repeat the same explanation for each lemma
c().explain(rm, exp);
c().explain(bf.m_x, exp);
@ -112,7 +112,7 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
t.add_coeff_var( j_sign, j);
c().mk_ineq(t, sbelow? llc::GT : llc::LT, - a*b);
}
void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm){
void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm){
point a, b;
point xy (vvr(bf.m_x), vvr(bf.m_y));
rational correct_mult_val = xy.x * xy.y;

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

@ -47,13 +47,13 @@ struct tangents: common {
tangents(core *core);
void generate_simple_tangent_lemma(const signed_vars* rm);
void generate_simple_tangent_lemma(const smon* rm);
void tangent_lemma();
void generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp);
void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp);
void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm);
void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm);
void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j, const rational& j_sign);
void generate_two_tang_lines(const bfc & bf, const point& xy, const rational& sign, lpvar j);

7
src/util/lp/var_eqs.h
View file

@ -123,6 +123,13 @@ public:
signed_var sv = find(signed_var(j, false));
return sv.var() == j;
}
inline bool is_root(svector<lpvar> v) const {
for (lpvar j : v)
if (! is_root(j))
return false;
return true;
}
bool vars_are_equiv(lpvar j, lpvar k) const {
signed_var sj = find(signed_var(j, false));
signed_var sk = find(signed_var(k, false));