mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

merge smon with monomial

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-22 16:33:58 -07:00
parent e73296fbe5
commit 53cc8048f7
20 changed files with 312 additions and 633 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -28,7 +28,7 @@ namespace nla {
void emonomials::inc_visited() const { void emonomials::inc_visited() const {
++m_visited; ++m_visited;
if (m_visited == 0) { if (m_visited == 0) {
for (auto& svt : m_canonized) { for (auto& svt : m_monomials) {
svt.visited() = 0; svt.visited() = 0;
} }
++m_visited; ++m_visited;
@ -45,7 +45,7 @@ namespace nla {
m_ve.pop(n); m_ve.pop(n);
unsigned old_sz = m_lim[m_lim.size() - n]; unsigned old_sz = m_lim[m_lim.size() - n];
for (unsigned i = m_monomials.size(); i-- > old_sz; ) { for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
monomial const& m = m_monomials[i]; monomial & m = m_monomials[i];
remove_cg(i, m); remove_cg(i, m);
m_var2index[m.var()] = UINT_MAX; m_var2index[m.var()] = UINT_MAX;
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
@ -57,7 +57,7 @@ namespace nla {
} }
} }
m_monomials.shrink(old_sz); m_monomials.shrink(old_sz);
m_canonized.shrink(old_sz); m_monomials.shrink(old_sz);
m_region.pop_scope(n); m_region.pop_scope(n);
m_lim.shrink(m_lim.size() - n); m_lim.shrink(m_lim.size() - n);
} }
@ -132,7 +132,7 @@ namespace nla {
return m_use_lists[v].m_head; return m_use_lists[v].m_head;
} }
smon const* emonomials::find_canonical(svector<lpvar> const& vars) const { monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
SASSERT(m_ve.is_root(vars)); SASSERT(m_ve.is_root(vars));
// find a unique key for dummy monomial // find a unique key for dummy monomial
lpvar v = m_var2index.size(); lpvar v = m_var2index.size();
@ -143,19 +143,17 @@ namespace nla {
} }
} }
unsigned idx = m_monomials.size(); unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr())); m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr(), idx));
m_canonized.push_back(smon(v, idx));
m_var2index.setx(v, idx, UINT_MAX); m_var2index.setx(v, idx, UINT_MAX);
do_canonize(m_monomials[idx]); do_canonize(m_monomials[idx]);
smon const* result = nullptr; monomial const* result = nullptr;
lpvar w; lpvar w;
if (m_cg_table.find(v, w)) { if (m_cg_table.find(v, w)) {
SASSERT(w != v); SASSERT(w != v);
result = &m_canonized[m_var2index[w]]; result = &m_monomials[m_var2index[w]];
} }
m_var2index[v] = UINT_MAX; m_var2index[v] = UINT_MAX;
m_monomials.pop_back(); m_monomials.pop_back();
m_canonized.pop_back(); // NB. relies on the pointer m_canonized not to change.
return result; return result;
} }
@ -170,7 +168,7 @@ namespace nla {
do { do {
unsigned idx = c->m_index; unsigned idx = c->m_index;
c = c->m_next; c = c->m_next;
monomial const& m = m_monomials[idx]; monomial & m = m_monomials[idx];
if (!is_visited(m)) { if (!is_visited(m)) {
set_visited(m); set_visited(m);
remove_cg(idx, m); remove_cg(idx, m);
@ -179,8 +177,8 @@ namespace nla {
while (c != first); while (c != first);
} }
void emonomials::remove_cg(unsigned idx, monomial const& m) { void emonomials::remove_cg(unsigned idx, monomial& m) {
smon& sv = m_canonized[idx]; monomial& sv = m_monomials[idx];
unsigned next = sv.next(); unsigned next = sv.next();
unsigned prev = sv.prev(); unsigned prev = sv.prev();
@ -194,8 +192,8 @@ namespace nla {
} }
} }
if (prev != idx) { if (prev != idx) {
m_canonized[next].prev() = prev; m_monomials[next].prev() = prev;
m_canonized[prev].next() = next; m_monomials[prev].next() = next;
sv.next() = idx; sv.next() = idx;
sv.prev() = idx; sv.prev() = idx;
} }
@ -204,7 +202,7 @@ namespace nla {
/** /**
\brief insert canonized monomials using v into a congruence table. \brief insert canonized monomials using v into a congruence table.
Prior to insertion, the monomials are canonized according to the current Prior to insertion, the monomials are canonized according to the current
variable equivalences. The canonized monomials (smon) are considered variable equivalences. The canonized monomials (monomial) are considered
in the same equivalence class if they have the same set of representative in the same equivalence class if they have the same set of representative
variables. Their signs may differ. variables. Their signs may differ.
*/ */
@ -219,7 +217,7 @@ namespace nla {
do { do {
unsigned idx = c->m_index; unsigned idx = c->m_index;
c = c->m_next; c = c->m_next;
monomial const& m = m_monomials[idx]; monomial & m = m_monomials[idx];
if (!is_visited(m)) { if (!is_visited(m)) {
set_visited(m); set_visited(m);
insert_cg(idx, m); insert_cg(idx, m);
@ -228,31 +226,31 @@ namespace nla {
while (c != first); while (c != first);
} }
void emonomials::insert_cg(unsigned idx, monomial const& m) { void emonomials::insert_cg(unsigned idx, monomial & m) {
do_canonize(m); do_canonize(m);
lpvar v = m.var(), w; lpvar v = m.var(), w;
if (m_cg_table.find(v, w)) { if (m_cg_table.find(v, w)) {
SASSERT(w != v); SASSERT(w != v);
unsigned idxr = m_var2index[w]; unsigned idxr = m_var2index[w];
unsigned idxl = m_canonized[idxr].prev(); unsigned idxl = m_monomials[idxr].prev();
m_canonized[idx].next() = idxr; m_monomials[idx].next() = idxr;
m_canonized[idx].prev() = idxl; m_monomials[idx].prev() = idxl;
m_canonized[idxr].prev() = idx; m_monomials[idxr].prev() = idx;
m_canonized[idxl].next() = idx; m_monomials[idxl].next() = idx;
} }
else { else {
m_cg_table.insert(v); m_cg_table.insert(v);
SASSERT(m_canonized[idx].next() == idx); SASSERT(m_monomials[idx].next() == idx);
SASSERT(m_canonized[idx].prev() == idx); SASSERT(m_monomials[idx].prev() == idx);
} }
} }
void emonomials::set_visited(monomial const& m) const { void emonomials::set_visited(monomial& m) const {
m_canonized[m_var2index[m.var()]].visited() = m_visited; m_monomials[m_var2index[m.var()]].visited() = m_visited;
} }
bool emonomials::is_visited(monomial const& m) const { bool emonomials::is_visited(monomial const& m) const {
return m_visited == m_canonized[m_var2index[m.var()]].visited(); return m_visited == m_monomials[m_var2index[m.var()]].visited();
} }
/** /**
@ -264,8 +262,7 @@ namespace nla {
*/ */
void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
unsigned idx = m_monomials.size(); unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, sz, vs)); m_monomials.push_back(monomial(v, sz, vs, idx));
m_canonized.push_back(smon(v, idx));
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
lpvar w = vs[i]; lpvar w = vs[i];
@ -281,33 +278,29 @@ namespace nla {
insert_cg(idx, m_monomials[idx]); insert_cg(idx, m_monomials[idx]);
} }
void emonomials::do_canonize(monomial const& mon) const { void emonomials::do_canonize(monomial & m) const {
unsigned index = m_var2index[mon.var()]; m.reset_rfields();
smon& svs = m_canonized[index]; for (lpvar v : m.vars()) {
svs.reset(); m.push_rvar(m_ve.find(v));
for (lpvar v : mon) {
svs.push_var(m_ve.find(v));
} }
svs.done_push(); m.sort_rvars();
} }
bool emonomials::canonize_divides(monomial const& m1, monomial const& m2) const { bool emonomials::canonize_divides(monomial& m, monomial & n) const {
if (m1.size() > m2.size()) return false; if (m.size() > n.size()) return false;
smon const& s1 = canonize(m1); unsigned ms = m.size(), ns = n.size();
smon const& s2 = canonize(m2);
unsigned sz1 = s1.size(), sz2 = s2.size();
unsigned i = 0, j = 0; unsigned i = 0, j = 0;
while (true) { while (true) {
if (i == sz1) { if (i == ms) {
return true; return true;
} }
else if (j == sz2) { else if (j == ns) {
return false; return false;
} }
else if (s1[i] == s2[j]) { else if (m.rvars()[i] == n.rvars()[j]) {
++i; ++j; ++i; ++j;
} }
else if (s1[i] < s2[j]) { else if (m.rvars()[i] < n.rvars()[j]) {
return false; return false;
} }
else { else {
@ -316,16 +309,9 @@ namespace nla {
} }
} }
void emonomials::explain_canonized(monomial const& m, lp::explanation& exp) {
for (lpvar v : m) {
signed_var w = m_ve.find(v);
m_ve.explain(signed_var(v, false), w, exp);
}
}
// yes, assume that monomials are non-empty. // yes, assume that monomials are non-empty.
emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial const& mon, bool at_end): emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end):
m(m), m_mon(&mon), m_it(iterator(m, m.head(mon[0]), at_end)), m_end(iterator(m, m.head(mon[0]), true)) { m(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) {
fast_forward(); fast_forward();
} }

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

@ -27,51 +27,6 @@
namespace nla { namespace nla {
/**
\brief class used to summarize the coefficients to a monomial after
canonization with respect to current equalities.
*/
class smon {
lpvar m_var; // variable representing original monomial
svector<lpvar> m_rvars;
bool m_rsign;
unsigned m_next; // next congruent node.
unsigned m_prev; // previous congruent node
mutable unsigned m_visited;
public:
smon(lpvar v, unsigned idx): m_var(v), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) {}
lpvar var() const { return m_var; }
unsigned next() const { return m_next; }
unsigned& next() { return m_next; }
unsigned prev() const { return m_prev; }
unsigned& prev() { return m_prev; }
unsigned visited() const { return m_visited; }
unsigned& visited() { return m_visited; }
svector<lpvar> const& rvars() const { return m_rvars; }
svector<lp::var_index>::const_iterator begin() const { return rvars().begin(); }
svector<lp::var_index>::const_iterator end() const { return rvars().end(); }
unsigned size() const { return m_rvars.size(); }
lpvar operator[](unsigned i) const { return m_rvars[i]; }
bool sign() const { return m_rsign; }
rational rsign() const { return rational(m_rsign ? -1 : 1); }
void reset() { m_rsign = false; m_rvars.reset(); }
void push_var(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
void done_push() {
std::sort(m_rvars.begin(), m_rvars.end());
}
std::ostream& display(std::ostream& out) const {
// out << "v" << var() << " := ";
// if (sign()) out << "- ";
// for (lpvar v : vars()) out << "v" << v << " ";
SASSERT(false);
return out;
}
};
inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); }
class emonomials : public var_eqs_merge_handler { class emonomials : public var_eqs_merge_handler {
/** /**
@ -97,7 +52,7 @@ class emonomials : public var_eqs_merge_handler {
hash_canonical(emonomials& em): em(em) {} hash_canonical(emonomials& em): em(em) {}
unsigned operator()(lpvar v) const { unsigned operator()(lpvar v) const {
auto const& vec = em.m_canonized[em.m_var2index[v]].rvars(); auto const& vec = em.m_monomials[em.m_var2index[v]].rvars();
return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10); return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
} }
}; };
@ -112,8 +67,8 @@ class emonomials : public var_eqs_merge_handler {
emonomials& em; emonomials& em;
eq_canonical(emonomials& em): em(em) {} eq_canonical(emonomials& em): em(em) {}
bool operator()(lpvar u, lpvar v) const { bool operator()(lpvar u, lpvar v) const {
auto const& uvec = em.m_canonized[em.m_var2index[u]].rvars(); auto const& uvec = em.m_monomials[em.m_var2index[u]].rvars();
auto const& vvec = em.m_canonized[em.m_var2index[v]].rvars(); auto const& vvec = em.m_monomials[em.m_var2index[v]].rvars();
return uvec == vvec; return uvec == vvec;
} }
}; };
@ -124,7 +79,6 @@ class emonomials : public var_eqs_merge_handler {
unsigned_vector m_lim; // backtracking point unsigned_vector m_lim; // backtracking point
mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator
region m_region; // region for allocating linked lists region m_region; // region for allocating linked lists
mutable vector<smon> m_canonized; // canonized versions of signed variables
mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur. mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur.
hash_canonical m_cg_hash; hash_canonical m_cg_hash;
eq_canonical m_cg_eq; eq_canonical m_cg_eq;
@ -139,14 +93,14 @@ class emonomials : public var_eqs_merge_handler {
void remove_cg(lpvar v); void remove_cg(lpvar v);
void insert_cg(lpvar v); void insert_cg(lpvar v);
void insert_cg(unsigned idx, monomial const& m); void insert_cg(unsigned idx, monomial & m);
void remove_cg(unsigned idx, monomial const& m); void remove_cg(unsigned idx, monomial & m);
void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
void do_canonize(monomial const& m) const; void do_canonize(monomial& m) const;
cell* head(lpvar v) const; cell* head(lpvar v) const;
void set_visited(monomial const& m) const; void set_visited(monomial& m) const;
bool is_visited(monomial const& m) const; bool is_visited(monomial const& m) const;
public: public:
@ -160,8 +114,7 @@ public:
m_visited(0), m_visited(0),
m_cg_hash(*this), m_cg_hash(*this),
m_cg_eq(*this), m_cg_eq(*this),
m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq), m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq) {
canonical(*this) {
m_ve.set_merge_handler(this); m_ve.set_merge_handler(this);
} }
@ -184,59 +137,23 @@ public:
/** /**
\brief retrieve monomial corresponding to variable v from definition v := vs \brief retrieve monomial corresponding to variable v from definition v := vs
*/ */
monomial const& var2monomial(lpvar v) const { SASSERT(is_monomial_var(v)); return m_monomials[m_var2index[v]]; } monomial const& operator[](lpvar v) const { return m_monomials[m_var2index[v]]; }
monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; }
monomial const& operator[](lpvar v) const { return var2monomial(v); }
monomial const& operator[](smon const& m) const { return var2monomial(m.var()); }
bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
/**
\brief retrieve canonized monomial corresponding to variable v from definition v := vs
*/
smon const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
class canonical {
emonomials& m;
public:
canonical(emonomials& m): m(m) {}
smon const& operator[](lpvar v) const { return m.var2canonical(v); }
smon const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
};
canonical canonical;
/**
\brief obtain a canonized signed monomial
corresponding to current equivalence class.
*/
smon const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
/** /**
\brief obtain the representative canonized monomial up to sign. \brief obtain the representative canonized monomial up to sign.
*/ */
//smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
smon const& rep(smon const& sv) const { monomial const& rep(monomial const& sv) const {
unsigned j = -1; unsigned j = -1;
m_cg_table.find(sv.var(), j); m_cg_table.find(sv.var(), j);
return m_canonized[m_var2index[j]]; return m_monomials[m_var2index[j]];
} }
/**
\brief the original sign is defined as a sign of the equivalence class representative.
*/
rational orig_sign(smon const& sv) const { return rep(sv).rsign(); }
/** /**
\brief determine if m1 divides m2 over the canonization obtained from merged variables. \brief determine if m1 divides m2 over the canonization obtained from merged variables.
*/ */
bool canonize_divides(monomial const& m1, monomial const& m2) const; bool canonize_divides(monomial & m1, monomial& m2) const;
/**
\brief produce explanation for monomial canonization.
*/
void explain_canonized(monomial const& m, lp::explanation& exp);
/** /**
\brief iterator over monomials that are declared. \brief iterator over monomials that are declared.
@ -253,7 +170,7 @@ public:
bool m_touched; bool m_touched;
public: public:
iterator(emonomials const& m, cell* c, bool at_end): m(m), m_cell(c), m_touched(at_end || c == nullptr) {} iterator(emonomials const& m, cell* c, bool at_end): m(m), m_cell(c), m_touched(at_end || c == nullptr) {}
monomial const& operator*() { return m.m_monomials[m_cell->m_index]; } monomial & operator*() { return m.m_monomials[m_cell->m_index]; }
iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; } iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_cell == other.m_cell && m_touched == other.m_touched; } bool operator==(iterator const& other) const { return m_cell == other.m_cell && m_touched == other.m_touched; }
@ -277,15 +194,15 @@ public:
*/ */
class pf_iterator { class pf_iterator {
emonomials const& m; emonomials const& m;
monomial const* m_mon; // monomial monomial * m_mon; // monomial
iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors. iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors.
iterator m_end; iterator m_end;
void fast_forward(); void fast_forward();
public: public:
pf_iterator(emonomials const& m, monomial const& mon, bool at_end); pf_iterator(emonomials const& m, monomial& mon, bool at_end);
pf_iterator(emonomials const& m, lpvar v, bool at_end); pf_iterator(emonomials const& m, lpvar v, bool at_end);
monomial const& operator*() { return *m_it; } monomial & operator*() { return *m_it; }
pf_iterator& operator++() { ++m_it; fast_forward(); return *this; } pf_iterator& operator++() { ++m_it; fast_forward(); return *this; }
pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; } pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; }
bool operator==(pf_iterator const& other) const { return m_it == other.m_it; } bool operator==(pf_iterator const& other) const { return m_it == other.m_it; }
@ -294,19 +211,19 @@ public:
class factors_of { class factors_of {
emonomials const& m; emonomials const& m;
monomial const* mon; monomial * mon;
lpvar m_var; lpvar m_var;
public: public:
factors_of(emonomials const& m, monomial const& mon): m(m), mon(&mon), m_var(UINT_MAX) {} factors_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {}
factors_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {} factors_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {}
pf_iterator begin() { if (mon) return pf_iterator(m, *mon, false); return pf_iterator(m, m_var, false); } pf_iterator begin() { if (mon) return pf_iterator(m, *mon, false); return pf_iterator(m, m_var, false); }
pf_iterator end() { if (mon) return pf_iterator(m, *mon, true); return pf_iterator(m, m_var, true); } pf_iterator end() { if (mon) return pf_iterator(m, *mon, true); return pf_iterator(m, m_var, true); }
}; };
factors_of get_factors_of(monomial const& m) const { inc_visited(); return factors_of(*this, m); } factors_of get_factors_of(monomial& m) const { inc_visited(); return factors_of(*this, m); }
factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); } factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); }
smon const* find_canonical(svector<lpvar> const& vars) const; monomial const* find_canonical(svector<lpvar> const& vars) const;
/** /**
\brief iterator over sign equivalent monomials. \brief iterator over sign equivalent monomials.
@ -324,7 +241,7 @@ public:
sign_equiv_monomials_it& operator++() { sign_equiv_monomials_it& operator++() {
m_touched = true; m_touched = true;
m_index = m.m_canonized[m_index].next(); m_index = m.m_monomials[m_index].next();
return *this; return *this;
} }
@ -355,8 +272,6 @@ public:
sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) { return sign_equiv_monomials(*this, m); } 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(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
sign_equiv_monomials enum_sign_equiv_monomials(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); }
/** /**
\brief display state of emonomials \brief display state of emonomials
*/ */
@ -373,6 +288,7 @@ public:
void unmerge_eh(signed_var r2, signed_var r1) override; void unmerge_eh(signed_var r2, signed_var r1) override;
bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
}; };
inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); } inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); }

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

@ -54,7 +54,7 @@ class factorization {
public: public:
factorization(const monomial* m): m_mon(m) { factorization(const monomial* m): m_mon(m) {
if (m != nullptr) { if (m != nullptr) {
for (lpvar j : *m) for (lpvar j : m->vars())
m_vars.push_back(factor(j, factor_type::VAR)); m_vars.push_back(factor(j, factor_type::VAR));
} }
} }

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

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

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

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

17
src/util/lp/mon_eq.cpp
View file

@ -5,24 +5,25 @@
#include "util/lp/lar_solver.h" #include "util/lp/lar_solver.h"
#include "util/lp/monomial.h" #include "util/lp/monomial.h"
namespace nla { namespace nla {
typedef monomial mon_eq;
bool check_assignment(mon_eq const& m, variable_map_type & vars) { template <typename T>
bool check_assignment(T const& m, variable_map_type & vars) {
rational r1 = vars[m.var()]; rational r1 = vars[m.var()];
if (r1.is_zero()) { if (r1.is_zero()) {
for (auto w : m) { for (auto w : m.vars()) {
if (vars[w].is_zero()) if (vars[w].is_zero())
return true; return true;
} }
return false; return false;
} }
rational r2(1); rational r2(1);
for (auto w : m) { for (auto w : m.vars()) {
r2 *= vars[w]; r2 *= vars[w];
} }
return r1 == r2; return r1 == r2;
} }
template <typename K>
bool check_assignments(const vector<mon_eq> & monomials, bool check_assignments(const K & monomials,
const lp::lar_solver& s, const lp::lar_solver& s,
variable_map_type & vars) { variable_map_type & vars) {
s.get_model(vars); s.get_model(vars);
@ -32,4 +33,8 @@ bool check_assignments(const vector<mon_eq> & monomials,
return true; return true;
} }
template bool check_assignments<vector<mon_eq>>(const vector<mon_eq>&,
const lp::lar_solver& s,
variable_map_type & vars);
} }

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

@ -8,41 +8,71 @@
#include "util/lp/lp_settings.h" #include "util/lp/lp_settings.h"
#include "util/vector.h" #include "util/vector.h"
#include "util/lp/lar_solver.h" #include "util/lp/lar_solver.h"
#include "util/lp/nla_defs.h"
namespace nla { namespace nla {
/* /*
* represents definition m_v = v1*v2*...*vn, * represents definition m_v = v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn] * where m_vs = [v1, v2, .., vn]
*/ */
class monomial {
class mon_eq {
// fields // fields
lp::var_index m_v; lp::var_index m_v;
svector<lp::var_index> m_vs; svector<lp::var_index> m_vs;
public: public:
// constructors // constructors
monomial(lp::var_index v, unsigned sz, lp::var_index const* vs): mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) { m_v(v), m_vs(sz, vs) {
std::sort(m_vs.begin(), m_vs.end()); std::sort(m_vs.begin(), m_vs.end());
} }
monomial(lp::var_index v, const svector<lp::var_index> &vs): mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
m_v(v), m_vs(vs) { m_v(v), m_vs(vs) {
std::sort(m_vs.begin(), m_vs.end()); std::sort(m_vs.begin(), m_vs.end());
} }
monomial() {} mon_eq() {}
unsigned var() const { return m_v; } unsigned var() const { return m_v; }
unsigned size() const { return m_vs.size(); } 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; } const svector<lp::var_index>& vars() const { return m_vs; }
svector<lp::var_index>& vars() { return m_vs; }
bool empty() const { return m_vs.empty(); } bool empty() const { return m_vs.empty(); }
};
std::ostream& display(std::ostream& out) const { // support the congruence
out << "v" << var() << " := "; class monomial: public mon_eq {
for (auto v : *this) { // fields
out << "v" << v << " "; svector<lpvar> m_rvars;
bool m_rsign;
unsigned m_next; // next congruent node.
unsigned m_prev; // previous congruent node
mutable unsigned m_visited;
public:
// constructors
monomial(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monomial(v, svector<lpvar>(sz, vs), idx) {
} }
monomial(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) {
std::sort(vars().begin(), vars().end());
}
unsigned next() const { return m_next; }
unsigned& next() { return m_next; }
unsigned prev() const { return m_prev; }
unsigned& prev() { return m_prev; }
unsigned visited() const { return m_visited; }
unsigned& visited() { return m_visited; }
svector<lpvar> const& rvars() const { return m_rvars; }
bool sign() const { return m_rsign; }
rational rsign() const { return rational(m_rsign ? -1 : 1); }
void reset_rfields() { m_rsign = false; m_rvars.reset(); }
void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
void sort_rvars() {
std::sort(m_rvars.begin(), m_rvars.end());
}
std::ostream& display(std::ostream& out) const {
// out << "v" << var() << " := ";
// if (sign()) out << "- ";
// for (lpvar v : vars()) out << "v" << v << " ";
SASSERT(false);
return out; return out;
} }
}; };
@ -52,28 +82,12 @@ public:
return m.display(out); return m.display(out);
} }
typedef std::unordered_map<lp::var_index, rational> variable_map_type; typedef std::unordered_map<lpvar, rational> variable_map_type;
template <typename T>
bool check_assignment(monomial const& m, variable_map_type & vars); bool check_assignment(T const& m, variable_map_type & vars);
template <typename K>
bool check_assignments(const vector<monomial> & monomimials, bool check_assignments(const K & monomimials,
const lp::lar_solver& s, const lp::lar_solver& s,
variable_map_type & vars); variable_map_type & vars);
} // end of namespace nla
/*
* represents definition m_v = coeff* v1*v2*...*vn,
* where m_vs = [v1, v2, .., vn]
*/
class monomial_coeff {
svector<lp::var_index> m_vs;
rational m_coeff;
public:
monomial_coeff(const svector<lp::var_index>& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {}
rational const& coeff() const { return m_coeff; }
const svector<lp::var_index> & vars() const { return m_vs; }
};
}

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

@ -26,7 +26,8 @@ basics::basics(core * c) : common(c) {}
// Monomials m and n vars have the same values, up to "sign" // Monomials m and n vars have the same values, up to "sign"
// Generate a lemma if values of m.var() and n.var() are not the same up to sign // 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) { 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 (vvr(m) == vvr(n) * sign)
return false; return false;
TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";); TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
@ -35,13 +36,13 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
} }
void basics::generate_zero_lemmas(const monomial& m) { void basics::generate_zero_lemmas(const monomial& m) {
SASSERT(!vvr(m).is_zero() && c().product_value(m).is_zero()); SASSERT(!vvr(m).is_zero() && c().product_value(m.vars()).is_zero());
int sign = nla::rat_sign(vvr(m)); int sign = nla::rat_sign(vvr(m));
unsigned_vector fixed_zeros; unsigned_vector fixed_zeros;
lpvar zero_j = find_best_zero(m, fixed_zeros); lpvar zero_j = find_best_zero(m, fixed_zeros);
SASSERT(is_set(zero_j)); SASSERT(is_set(zero_j));
unsigned zero_power = 0; unsigned zero_power = 0;
for (lpvar j : m){ for (lpvar j : m.vars()){
if (j == zero_j) { if (j == zero_j) {
zero_power++; zero_power++;
continue; continue;
@ -91,7 +92,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product
generate_zero_lemmas(m); generate_zero_lemmas(m);
} else { } else {
add_empty_lemma(); add_empty_lemma();
for(lpvar j: m) { for(lpvar j: m.vars()) {
negate_strict_sign(j); negate_strict_sign(j);
} }
c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT); c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT);
@ -122,12 +123,10 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
} }
const monomial& m_v = c().m_emons[v]; const monomial& m_v = c().m_emons[v];
smon const& sv_v = c().m_emons.canonical[v];
TRACE("nla_solver_details", tout << "mon = " << pp_mon(c(), m_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)) { for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) {
smon const& sv_w = c().m_emons.canonical[m_w]; if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done())
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; return true;
} }
@ -167,7 +166,7 @@ void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rat
// and the bounds on j contain 0 as an inner point // 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 basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
lpvar zero_j = -1; lpvar zero_j = -1;
for (unsigned j : m){ for (unsigned j : m.vars()){
if (vvr(j).is_zero()){ if (vvr(j).is_zero()){
if (c().var_is_fixed_to_zero(j)) if (c().var_is_fixed_to_zero(j))
fixed_zeros.push_back(j); fixed_zeros.push_back(j);
@ -189,7 +188,7 @@ void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j,
// we know all the signs // we know all the signs
add_empty_lemma(); add_empty_lemma();
c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
for (unsigned j : m){ for (unsigned j : m.rvars()){
if (j != zero_j) { if (j != zero_j) {
negate_strict_sign(j); negate_strict_sign(j);
} }
@ -222,7 +221,7 @@ void basics::negate_strict_sign(lpvar j) {
// here we use the fact // here we use the fact
// xy = 0 -> x = 0 or y = 0 // xy = 0 -> x = 0 or y = 0
bool basics::basic_lemma_for_mon_zero(const smon& rm, const factorization& f) { bool basics::basic_lemma_for_mon_zero(const monomial& rm, const factorization& f) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return true; return true;
#if 0 #if 0
@ -251,7 +250,7 @@ bool basics::basic_lemma(bool derived) {
unsigned sz = rm_ref.size(); unsigned sz = rm_ref.size();
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
lpvar v = rm_ref[(j + start) % rm_ref.size()]; lpvar v = rm_ref[(j + start) % rm_ref.size()];
const smon& r = c().m_emons.canonical[v]; const monomial& r = c().m_emons[v];
SASSERT (!c().check_monomial(c().m_emons[v])); SASSERT (!c().check_monomial(c().m_emons[v]));
basic_lemma_for_mon(r, derived); basic_lemma_for_mon(r, derived);
} }
@ -261,13 +260,13 @@ bool basics::basic_lemma(bool derived) {
// Use basic multiplication properties to create a lemma // Use basic multiplication properties to create a lemma
// for the given monomial. // for the given monomial.
// "derived" means derived from constraints - the alternative is model based // "derived" means derived from constraints - the alternative is model based
void basics::basic_lemma_for_mon(const smon& rm, bool derived) { void basics::basic_lemma_for_mon(const monomial& rm, bool derived) {
if (derived) if (derived)
basic_lemma_for_mon_derived(rm); basic_lemma_for_mon_derived(rm);
else else
basic_lemma_for_mon_model_based(rm); basic_lemma_for_mon_model_based(rm);
} }
bool basics::basic_lemma_for_mon_derived(const smon& rm) { bool basics::basic_lemma_for_mon_derived(const monomial& rm) {
if (c().var_is_fixed_to_zero(var(rm))) { if (c().var_is_fixed_to_zero(var(rm))) {
for (auto factorization : factorization_factory_imp(rm, c())) { for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty()) if (factorization.is_empty())
@ -293,7 +292,7 @@ bool basics::basic_lemma_for_mon_derived(const smon& rm) {
return false; return false;
} }
// x = 0 or y = 0 -> xy = 0 // x = 0 or y = 0 -> xy = 0
bool basics::basic_lemma_for_mon_non_zero_derived(const smon& rm, const factorization& f) { bool basics::basic_lemma_for_mon_non_zero_derived(const monomial& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
if (! c().var_is_separated_from_zero(var(rm))) if (! c().var_is_separated_from_zero(var(rm)))
return false; return false;
@ -317,7 +316,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const smon& rm, const factoriz
} }
// use the fact that // use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon& rm, const factorization& f) { bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& rm, const factorization& f) {
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
lpvar mon_var = c().m_emons[rm.var()].var(); lpvar mon_var = c().m_emons[rm.var()].var();
@ -375,64 +374,14 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon&
TRACE("nla_solver", c().print_lemma(tout); ); TRACE("nla_solver", c().print_lemma(tout); );
return true; return true;
} }
// use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x
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;
TRACE("nla_solver", tout << "f = "; c().print_factorization(f, tout);); bool basics::basic_lemma_for_mon_neutral_derived(const monomial& rm, const factorization& factorization) {
for (auto j : f){
TRACE("nla_solver", tout << "j = "; c().print_factor_with_vars(j, tout););
auto v = vvr(j);
if (v == rational(1)) {
continue;
}
if (v == -rational(1)) {
sign = - sign;
continue;
}
if (not_one == static_cast<lpvar>(-1)) {
not_one = var(j);
continue;
}
// if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma
return false;
}
add_empty_lemma();
explain(rm);
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));
}
if (not_one == static_cast<lpvar>(-1)) {
c().mk_ineq( c().m_emons[rm.var()].var(), llc::EQ, sign);
} else {
c().mk_ineq( c().m_emons[rm.var()].var(), -sign, not_one, llc::EQ);
}
TRACE("nla_solver",
tout << "rm = " << rm;
c().print_lemma(tout););
return true;
}
bool basics::basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization) {
return return
basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization) || basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization);
basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(rm, factorization);
return false;
} }
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
void basics::proportion_lemma_model_based(const smon& rm, const factorization& factorization) { void basics::proportion_lemma_model_based(const monomial& rm, const factorization& factorization) {
rational rmv = abs(vvr(rm)); rational rmv = abs(vvr(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization)); SASSERT(c().has_zero_factor(factorization));
@ -448,7 +397,7 @@ void basics::proportion_lemma_model_based(const smon& rm, const factorization& f
} }
} }
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
bool basics::proportion_lemma_derived(const smon& rm, const factorization& factorization) { bool basics::proportion_lemma_derived(const monomial& rm, const factorization& factorization) {
return false; return false;
rational rmv = abs(vvr(rm)); rational rmv = abs(vvr(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
@ -473,7 +422,7 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
rational sm = rational(nla::rat_sign(mv)); rational sm = rational(nla::rat_sign(mv));
c().mk_ineq(sm, mon_var, llc::LT); c().mk_ineq(sm, mon_var, llc::LT);
for (unsigned fi = 0; fi < m.size(); fi ++) { for (unsigned fi = 0; fi < m.size(); fi ++) {
lpvar j = m[fi]; lpvar j = m.vars()[fi];
if (fi != factor_index) { if (fi != factor_index) {
c().mk_ineq(j, llc::EQ); c().mk_ineq(j, llc::EQ);
} else { } else {
@ -489,10 +438,10 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
// none of the factors is zero and the product is not zero // none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm| // -> |fc[factor_index]| <= |rm|
void basics::generate_pl(const smon& rm, const factorization& fc, int factor_index) { void basics::generate_pl(const monomial& rm, const factorization& fc, int factor_index) {
TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = "; TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = "
tout << rm; << pp_mon(c(), rm);
tout << "fc = "; c().print_factorization(fc, tout); tout << ", fc = "; c().print_factorization(fc, tout);
tout << "orig mon = "; c().print_monomial(c().m_emons[rm.var()], tout);); tout << "orig mon = "; c().print_monomial(c().m_emons[rm.var()], tout););
if (fc.is_mon()) { if (fc.is_mon()) {
generate_pl_on_mon(*fc.mon(), factor_index); generate_pl_on_mon(*fc.mon(), factor_index);
@ -523,7 +472,7 @@ void basics::generate_pl(const smon& rm, const factorization& fc, int factor_ind
TRACE("nla_solver", c().print_lemma(tout); ); TRACE("nla_solver", c().print_lemma(tout); );
} }
// here we use the fact xy = 0 -> x = 0 or y = 0 // here we use the fact xy = 0 -> x = 0 or y = 0
void basics::basic_lemma_for_mon_zero_model_based(const smon& rm, const factorization& f) { 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);); TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
SASSERT(vvr(rm).is_zero()&& ! c().rm_check(rm)); SASSERT(vvr(rm).is_zero()&& ! c().rm_check(rm));
add_empty_lemma(); add_empty_lemma();
@ -544,7 +493,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const smon& rm, const factoriz
TRACE("nla_solver", c().print_lemma(tout);); TRACE("nla_solver", c().print_lemma(tout););
} }
void basics::basic_lemma_for_mon_model_based(const smon& rm) { void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
TRACE("nla_solver_bl", tout << "rm = " << rm;); TRACE("nla_solver_bl", tout << "rm = " << rm;);
if (vvr(rm).is_zero()) { if (vvr(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) { for (auto factorization : factorization_factory_imp(rm, c())) {
@ -576,7 +525,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
return false; return false;
} }
lpvar jl = -1; lpvar jl = -1;
for (auto j : m ) { for (auto j : m.vars() ) {
if (abs(vvr(j)) == abs_mv) { if (abs(vvr(j)) == abs_mv) {
jl = j; jl = j;
break; break;
@ -585,7 +534,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
if (jl == static_cast<lpvar>(-1)) if (jl == static_cast<lpvar>(-1))
return false; return false;
lpvar not_one_j = -1; lpvar not_one_j = -1;
for (auto j : m ) { for (auto j : m.vars() ) {
if (j == jl) { if (j == jl) {
continue; continue;
} }
@ -623,7 +572,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
lpvar not_one = -1; lpvar not_one = -1;
rational sign(1); rational sign(1);
TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout);); TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
for (auto j : m){ for (auto j : m.vars()){
auto v = vvr(j); auto v = vvr(j);
if (v == rational(1)) { if (v == rational(1)) {
continue; continue;
@ -648,7 +597,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
} }
add_empty_lemma(); add_empty_lemma();
for (auto j : m){ for (auto j : m.vars()){
if (not_one == j) continue; if (not_one == j) continue;
c().mk_ineq(j, llc::NE, vvr(j)); c().mk_ineq(j, llc::NE, vvr(j));
} }
@ -664,7 +613,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
// use the fact that // use the fact that
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const smon& rm, const factorization& f) { bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& rm, const factorization& f) {
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
lpvar mon_var = c().m_emons[rm.var()].var(); lpvar mon_var = c().m_emons[rm.var()].var();
@ -722,7 +671,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const sm
return true; return true;
} }
void basics::basic_lemma_for_mon_neutral_model_based(const smon& rm, const factorization& f) { void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const factorization& f) {
if (f.is_mon()) { if (f.is_mon()) {
basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(*f.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()); basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(*f.mon());
@ -734,8 +683,8 @@ void basics::basic_lemma_for_mon_neutral_model_based(const smon& rm, const facto
} }
// use the fact // use the fact
// 1 * 1 ... * 1 * x * 1 ... * 1 = x // 1 * 1 ... * 1 * x * 1 ... * 1 = x
bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const smon& rm, const factorization& f) { bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& rm, const factorization& f) {
rational sign = c().m_emons.orig_sign(rm); rational sign = rm.rsign();
TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; ); TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
lpvar not_one = -1; lpvar not_one = -1;
for (auto j : f){ for (auto j : f){
@ -815,7 +764,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
} }
// x = 0 or y = 0 -> xy = 0 // x = 0 or y = 0 -> xy = 0
void basics::basic_lemma_for_mon_non_zero_model_based(const smon& rm, const factorization& f) { void basics::basic_lemma_for_mon_non_zero_model_based(const monomial& rm, const factorization& f) {
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
if (f.is_mon()) if (f.is_mon())
basic_lemma_for_mon_non_zero_model_based_mf(f); basic_lemma_for_mon_non_zero_model_based_mf(f);

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

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

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

@ -28,25 +28,23 @@ template <typename T> void common::explain(const T& t) {
} }
template void common::explain<monomial>(const monomial& t); template void common::explain<monomial>(const monomial& t);
template void common::explain<factor>(const factor& t); template void common::explain<factor>(const factor& t);
template void common::explain<smon>(const smon& t);
template void common::explain<factorization>(const factorization& t); template void common::explain<factorization>(const factorization& t);
void common::explain(lpvar j) { c().explain(j, c().current_expl()); } 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 <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<monomial>(monomial const& t) const;
template rational common::vvr<smon>(smon const& t) const;
template rational common::vvr<factor>(factor const& t) const; template rational common::vvr<factor>(factor const& t) const;
rational common::vvr(lpvar t) const { return c().vvr(t); } 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 <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<factor>(factor const& t) const;
template lpvar common::var<smon>(smon const& t) const; template lpvar common::var<monomial>(monomial const& t) const;
void common::add_empty_lemma() { c().add_empty_lemma(); } void common::add_empty_lemma() { c().add_empty_lemma(); }
template <typename T> rational common::canonize_sign(const T& t) const { template <typename T> rational common::canonize_sign(const T& t) const {
return c().canonize_sign(t); return c().canonize_sign(t);
} }
template rational common::canonize_sign<smon>(const smon& t) const; template rational common::canonize_sign<monomial>(const monomial& t) const;
template rational common::canonize_sign<factor>(const factor& t) const; template rational common::canonize_sign<factor>(const factor& t) const;
rational common::canonize_sign(lpvar j) const { rational common::canonize_sign(lpvar j) const {
return c().canonize_sign_of_var(j); return c().canonize_sign_of_var(j);
@ -98,10 +96,7 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
return c().print_product(m, out); return c().print_product(m, out);
} }
template template
std::ostream& common::print_product<monomial>(const monomial & m, std::ostream& out) const; std::ostream& common::print_product<unsigned_vector>(const unsigned_vector & 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 { std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
return c().print_monomial(m, out); return c().print_monomial(m, out);

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

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

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

@ -83,21 +83,20 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
return r; return r;
} }
TRACE("nla_solver", tout << "nv";); TRACE("nla_solver", tout << "nv";);
return m_emons.canonical[f.var()].rvars(); return m_emons[f.var()].rvars();
} }
// the value of the factor is equal to the value of the variable multiplied // the value of the factor is equal to the value of the variable multiplied
// by the canonize_sign // by the canonize_sign
rational core::canonize_sign(const factor& f) const { rational core::canonize_sign(const factor& f) const {
return f.is_var()? return f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign();
canonize_sign_of_var(f.var()) : m_emons.canonical[f.var()].rsign();
} }
rational core::canonize_sign_of_var(lpvar j) const { rational core::canonize_sign_of_var(lpvar j) const {
return m_evars.find(j).rsign(); return m_evars.find(j).rsign();
} }
rational core::canonize_sign(const smon& m) const { rational core::canonize_sign(const monomial& m) const {
return m.rsign(); return m.rsign();
} }
@ -116,8 +115,7 @@ void core::pop(unsigned n) {
m_emons.pop(n); m_emons.pop(n);
} }
template <typename T> rational core::product_value(const unsigned_vector & m) const {
rational core::product_value(const T & m) const {
rational r(1); rational r(1);
for (auto j : m) { for (auto j : m) {
r *= m_lar_solver.get_column_value_rational(j); r *= m_lar_solver.get_column_value_rational(j);
@ -128,18 +126,14 @@ rational core::product_value(const T & m) const {
// return true iff the monomial value is equal to the product of the values of the factors // return true iff the monomial value is equal to the product of the values of the factors
bool core::check_monomial(const monomial& m) const { bool core::check_monomial(const monomial& m) const {
SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
return product_value(m) == m_lar_solver.get_column_value_rational(m.var()); return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
} }
void core::explain(const monomial& m, lp::explanation& exp) const { void core::explain(const monomial& m, lp::explanation& exp) const {
for (lpvar j : m) for (lpvar j : m.vars())
explain(j, exp); explain(j, exp);
} }
void core::explain(const smon& rm, lp::explanation& exp) const {
explain(m_emons[rm.var()], exp);
}
void core::explain(const factor& f, lp::explanation& exp) const { void core::explain(const factor& f, lp::explanation& exp) const {
if (f.type() == factor_type::VAR) { if (f.type() == factor_type::VAR) {
explain(f.var(), exp); explain(f.var(), exp);
@ -161,8 +155,6 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
} }
return out; return out;
} }
template std::ostream& core::print_product<monomial>(const monomial & 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 { std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
if (f.is_var()) { if (f.is_var()) {
@ -170,7 +162,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
print_var(f.var(), out); print_var(f.var(), out);
} else { } else {
out << "PROD, "; out << "PROD, ";
print_product(m_emons.canonical[f.var()].rvars(), out); print_product(m_emons[f.var()].rvars(), out);
} }
out << "\n"; out << "\n";
return out; return out;
@ -181,7 +173,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
print_var(f.var(), out); print_var(f.var(), out);
} }
else { else {
out << " RM = " << m_emons.canonical[f.var()]; out << " RM = " << m_emons[f.var()];
out << "\n orig mon = " << m_emons[f.var()]; out << "\n orig mon = " << m_emons[f.var()];
} }
return out; return out;
@ -214,7 +206,7 @@ std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
template <typename T> template <typename T>
std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const { std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
print_product(m, out) << "\n"; print_product(m.vars(), out) << "\n";
for (unsigned k = 0; k < m.size(); k++) { for (unsigned k = 0; k < m.size(); k++) {
print_var(m[k], out); print_var(m[k], out);
} }
@ -223,7 +215,7 @@ 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 { std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
out << "["; print_var(m.var(), out) << "]\n"; out << "["; print_var(m.var(), out) << "]\n";
for (lpvar j: m) for (lpvar j: m.vars())
print_var(j, out); print_var(j, out);
out << ")\n"; out << ")\n";
return out; return out;
@ -569,7 +561,7 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
int core::rat_sign(const monomial& m) const { int core::rat_sign(const monomial& m) const {
int sign = 1; int sign = 1;
for (lpvar j : m) { for (lpvar j : m.vars()) {
auto v = vvr(j); auto v = vvr(j);
if (v.is_neg()) { if (v.is_neg()) {
sign = - sign; sign = - sign;
@ -778,12 +770,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 { bool core:: find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
SASSERT(vars_are_roots(vars)); SASSERT(vars_are_roots(vars));
smon const* sv = m_emons.find_canonical(vars); monomial const* sv = m_emons.find_canonical(vars);
return sv && (i = sv->var(), true); return sv && (i = sv->var(), true);
} }
const monomial* core::find_monomial_of_vars(const svector<lpvar>& vars) const { const monomial* core::find_monomial_of_vars(const svector<lpvar>& vars) const {
smon const* sv = m_emons.find_canonical(vars); monomial const* sv = m_emons.find_canonical(vars);
return sv ? &m_emons[sv->var()] : nullptr; return sv ? &m_emons[sv->var()] : nullptr;
} }
@ -806,7 +798,7 @@ void core::explain_separation_from_zero(lpvar j) {
explain_existing_upper_bound(j); explain_existing_upper_bound(j);
} }
int core::get_derived_sign(const smon& rm, const factorization& f) const { int core::get_derived_sign(const monomial& rm, const factorization& f) const {
rational sign = rm.rsign(); // this is the flip sign of the variable var(rm) rational sign = rm.rsign(); // this is the flip sign of the variable var(rm)
SASSERT(!sign.is_zero()); SASSERT(!sign.is_zero());
for (const factor& fc: f) { for (const factor& fc: f) {
@ -818,7 +810,7 @@ int core::get_derived_sign(const smon& rm, const factorization& f) const {
} }
return nla::rat_sign(sign); return nla::rat_sign(sign);
} }
void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const { void core::trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const {
out << "rooted vars: "; out << "rooted vars: ";
print_product(rm.rvars(), out); print_product(rm.rvars(), out);
out << "\n"; out << "\n";
@ -1269,7 +1261,7 @@ bool core:: mon_has_zero(const T& product) const {
return false; return false;
} }
template bool core::mon_has_zero<monomial>(const monomial& product) const; template bool core::mon_has_zero<unsigned_vector>(const unsigned_vector& product) const;
lp::lp_settings& core::settings() { lp::lp_settings& core::settings() {
@ -1395,7 +1387,7 @@ template <typename T>
void core::trace_print_rms(const T& p, std::ostream& out) { void core::trace_print_rms(const T& p, std::ostream& out) {
out << "p = {\n"; out << "p = {\n";
for (auto j : p) { for (auto j : p) {
out << "j = " << j << ", rm = " << m_emons.canonical[j] << "\n"; out << "j = " << j << ", rm = " << m_emons[j] << "\n";
} }
out << "}"; out << "}";
} }
@ -1407,7 +1399,7 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
if (abs(vvr(mc.vars()[i])) == rational(1)) { if (abs(vvr(mc.vars()[i])) == rational(1)) {
auto vv = mc.vars(); auto vv = mc.vars();
vv.erase(vv.begin()+i); vv.erase(vv.begin()+i);
smon const* sv = m_emons.find_canonical(vv); monomial const* sv = m_emons.find_canonical(vv);
if (!sv) { if (!sv) {
out << "nf length" << vv.size() << "\n"; ; out << "nf length" << vv.size() << "\n"; ;
} }
@ -1444,7 +1436,8 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
auto insert_j = [&](lpvar j) { auto insert_j = [&](lpvar j) {
vars.insert(j); vars.insert(j);
if (m_emons.is_monomial_var(j)) { if (m_emons.is_monomial_var(j)) {
for (lpvar k : m_emons[j]) vars.insert(k); for (lpvar k : m_emons[j].vars())
vars.insert(k);
} }
}; };
@ -1462,7 +1455,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
return vars; return vars;
} }
bool core::divide(const smon& bc, const factor& c, factor & b) const { bool core::divide(const monomial& bc, const factor& c, factor & b) const {
svector<lpvar> c_vars = sorted_vars(c); svector<lpvar> c_vars = sorted_vars(c);
TRACE("nla_solver_div", TRACE("nla_solver_div",
tout << "c_vars = "; tout << "c_vars = ";
@ -1479,7 +1472,7 @@ bool core::divide(const smon& bc, const factor& c, factor & b) const {
b = factor(b_vars[0], factor_type::VAR); b = factor(b_vars[0], factor_type::VAR);
return true; return true;
} }
smon const* sv = m_emons.find_canonical(b_vars); monomial const* sv = m_emons.find_canonical(b_vars);
if (!sv) { if (!sv) {
TRACE("nla_solver_div", tout << "not in rooted";); TRACE("nla_solver_div", tout << "not in rooted";);
return false; return false;
@ -1529,10 +1522,10 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
} }
void core::trace_print_ol(const smon& ac, void core::trace_print_ol(const monomial& ac,
const factor& a, const factor& a,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b, const factor& b,
std::ostream& out) { std::ostream& out) {
out << "ac = " << ac << "\n"; out << "ac = " << ac << "\n";
@ -1581,7 +1574,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
bool core::rm_check(const smon& rm) const { bool core::rm_check(const monomial& rm) const {
return check_monomial(m_emons[rm.var()]); return check_monomial(m_emons[rm.var()]);
} }
@ -1639,7 +1632,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
*/ */
bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) { bool core::find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf) {
for (auto factorization : factorization_factory_imp(rm, *this)) { for (auto factorization : factorization_factory_imp(rm, *this)) {
if (factorization.size() == 2) { if (factorization.size() == 2) {
auto a = factorization[0]; auto a = factorization[0];
@ -1653,18 +1646,18 @@ bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) {
return false; return false;
} }
bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found){ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*& rm_found){
rm_found = nullptr; rm_found = nullptr;
for (unsigned i: m_to_refine) { for (unsigned i: m_to_refine) {
const auto& rm = m_emons.canonical[i]; const auto& rm = m_emons[i];
SASSERT (!check_monomial(m_emons[rm.var()])); SASSERT (!check_monomial(m_emons[rm.var()]));
if (rm.size() == 2) { if (rm.size() == 2) {
sign = rational(1); sign = rational(1);
const monomial & m = m_emons[rm.var()]; const monomial & m = m_emons[rm.var()];
j = m.var(); j = m.var();
rm_found = nullptr; rm_found = nullptr;
bf.m_x = factor(m[0], factor_type::VAR); bf.m_x = factor(m.vars()[0], factor_type::VAR);
bf.m_y = factor(m[1], factor_type::VAR); bf.m_y = factor(m.vars()[1], factor_type::VAR);
return true; return true;
} }
@ -1684,8 +1677,8 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm
} }
void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) { void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
SASSERT(sign == nla::rat_sign(product_value(m))); SASSERT(sign == nla::rat_sign(product_value(m.vars())));
for (lpvar j : m) { for (lpvar j : m.vars()) {
if (vvr(j).is_pos()) { if (vvr(j).is_pos()) {
mk_ineq(j, llc::LE); mk_ineq(j, llc::LE);
} else { } else {
@ -1971,7 +1964,7 @@ lbool core::test_check(
m_lar_solver.set_status(lp::lp_status::OPTIMAL); m_lar_solver.set_status(lp::lp_status::OPTIMAL);
return check(l); return check(l);
} }
template rational core::product_value<monomial>(const monomial & m) const;
} // end of nla } // end of nla

28
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); } lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
lpvar var(smon const& sv) const { return sv.var(); } lpvar var(monomial const& sv) const { return sv.var(); }
rational vvr(const smon& rm) const { return rm.rsign()*vvr(m_emons[rm.var()]); } rational vvr_rooted(const monomial& m) const { return m.rsign()*vvr(m.var()); }
rational vvr(const factor& f) const { return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); } rational vvr(const factor& f) const { return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
@ -122,10 +122,10 @@ public:
// the value of the rooted monomias is equal to the value of the m.var() variable multiplied // the value of the rooted monomias is equal to the value of the m.var() variable multiplied
// by the canonize_sign // by the canonize_sign
rational canonize_sign(const smon& m) const; rational canonize_sign(const monomial& m) const;
void deregister_monomial_from_smonomials (const monomial & m, unsigned i); void deregister_monomial_from_monomialomials (const monomial & m, unsigned i);
void deregister_monomial_from_tables(const monomial & m, unsigned i); void deregister_monomial_from_tables(const monomial & m, unsigned i);
@ -135,14 +135,12 @@ public:
void pop(unsigned n); void pop(unsigned n);
rational mon_value_by_vars(unsigned i) const; rational mon_value_by_vars(unsigned i) const;
template <typename T> rational product_value(const unsigned_vector & m) const;
rational product_value(const T & m) const;
// return true iff the monomial value is equal to the product of the values of the factors // return true iff the monomial value is equal to the product of the values of the factors
bool check_monomial(const monomial& m) const; bool check_monomial(const monomial& m) const;
void explain(const monomial& m, lp::explanation& exp) const; void explain(const monomial& m, lp::explanation& exp) const;
void explain(const smon& rm, lp::explanation& exp) const;
void explain(const factor& f, lp::explanation& exp) const; void explain(const factor& f, lp::explanation& exp) const;
void explain(lpvar j, lp::explanation& exp) const; void explain(lpvar j, lp::explanation& exp) const;
void explain_existing_lower_bound(lpvar j); void explain_existing_lower_bound(lpvar j);
@ -169,7 +167,7 @@ public:
std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const; std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
template <typename T> template <typename T>
void trace_print_rms(const T& p, std::ostream& out); void trace_print_rms(const T& p, std::ostream& out);
void trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const; void trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const;
void print_monomial_stats(const monomial& m, std::ostream& out); void print_monomial_stats(const monomial& m, std::ostream& out);
void print_stats(std::ostream& out); void print_stats(std::ostream& out);
std::ostream& print_lemma(std::ostream& out) const; std::ostream& print_lemma(std::ostream& out) const;
@ -177,10 +175,10 @@ public:
void print_specific_lemma(const lemma& l, std::ostream& out) const; void print_specific_lemma(const lemma& l, std::ostream& out) const;
void trace_print_ol(const smon& ac, void trace_print_ol(const monomial& ac,
const factor& a, const factor& a,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b, const factor& b,
std::ostream& out); std::ostream& out);
@ -243,7 +241,7 @@ public:
const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const; const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
int get_derived_sign(const smon& rm, const factorization& f) const; int get_derived_sign(const monomial& rm, const factorization& f) const;
bool var_has_positive_lower_bound(lpvar j) const; bool var_has_positive_lower_bound(lpvar j) const;
@ -312,7 +310,7 @@ public:
void init_to_refine(); void init_to_refine();
bool divide(const smon& bc, const factor& c, factor & b) const; bool divide(const monomial& bc, const factor& c, factor & b) const;
void negate_factor_equality(const factor& c, const factor& d); void negate_factor_equality(const factor& c, const factor& d);
@ -320,15 +318,15 @@ public:
std::unordered_set<lpvar> collect_vars(const lemma& l) const; std::unordered_set<lpvar> collect_vars(const lemma& l) const;
bool rm_check(const smon&) const; bool rm_check(const monomial&) const;
std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity(); 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);
void add_abs_bound(lpvar v, llc cmp, rational const& bound); void add_abs_bound(lpvar v, llc cmp, rational const& bound);
bool find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf); bool find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf);
bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found); bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*& rm_found );
void generate_simple_sign_lemma(const rational& sign, const monomial& m); void generate_simple_sign_lemma(const rational& sign, const monomial& m);
void negate_relation(unsigned j, const rational& a); void negate_relation(unsigned j, const rational& a);

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

@ -34,104 +34,6 @@ void monotone::monotonicity_lemma() {
} }
} }
void monotone::print_monotone_array(const monotone_array_t& lex_sorted,
std::ostream& out) const {
out << "Monotone array :\n";
for (const auto & t : lex_sorted ){
out << "(";
print_vector(t.first, out);
out << "), rm[" << t.second << "]" << std::endl;
}
out << "}";
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const monotone_array_t& 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 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;);
if (vk > v) continue;
unsigned strict;
if (uniform_le(key, p.first, strict)) {
if (static_cast<int>(strict) != -1 && !has_zero(key)) {
generate_monl_strict(rm, rmk, strict);
return true;
}
else if (vk < v) {
generate_monl(rm, rmk);
return true;
}
}
}
return false;
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const monotone_array_t& 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 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;);
if (vk < v) continue;
unsigned strict;
if (uniform_le(p.first, key, strict)) {
TRACE("nla_solver", tout << "strict = " << strict << std::endl;);
if (static_cast<int>(strict) != -1) {
generate_monl_strict(rmk, rm, strict);
return true;
} else {
SASSERT(key == p.first);
if (vk < v) {
generate_monl(rmk, rm);
return true;
}
}
}
}
return false;
}
bool monotone::monotonicity_lemma_on_lex_sorted_rm(const monotone_array_t& 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 monotone_array_t& lex_sorted) {
for (unsigned i = 0; i < lex_sorted.size(); i++) {
unsigned rmi = lex_sorted[i].second;
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;
}
return false;
}
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.rvars()) {
r.push_back(std::make_pair(abs(vvr(j)), j));
}
std::sort(r.begin(), r.end(), [](const std::pair<rational, lpvar>& a,
const std::pair<rational, lpvar>& b) {
return
a.first < b.first ||
(a.first == b.first &&
a.second < b.second);
});
return r;
}
void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) { void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
rational av = vvr(a); rational av = vvr(a);
@ -148,31 +50,9 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
} }
} }
// strict version
void monotone::generate_monl_strict(const smon& a,
const smon& b,
unsigned strict) {
add_empty_lemma();
auto akey = get_sorted_key_with_vars(a);
auto bkey = get_sorted_key_with_vars(b);
SASSERT(akey.size() == bkey.size());
for (unsigned i = 0; i < akey.size(); i++) {
if (i != strict) {
negate_abs_a_le_abs_b(akey[i].second, bkey[i].second, true);
} else {
mk_ineq(b[i], llc::EQ);
negate_abs_a_lt_abs_b(akey[i].second, bkey[i].second);
}
}
assert_abs_val_a_le_abs_var_b(a, b, true);
explain(a);
explain(b);
TRACE("nla_solver", print_lemma(tout););
}
void monotone::assert_abs_val_a_le_abs_var_b( void monotone::assert_abs_val_a_le_abs_var_b(
const smon& a, const monomial& a,
const smon& b, const monomial& b,
bool strict) { bool strict) {
lpvar aj = var(a); lpvar aj = var(a);
lpvar bj = var(b); lpvar bj = var(b);
@ -198,54 +78,11 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj| mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj|
} }
// not a strict version
void monotone::generate_monl(const smon& a,
const smon& b) {
TRACE("nla_solver",
tout << "a = " << a << "\n:";
tout << "b = " << b << "\n:";);
add_empty_lemma();
auto akey = get_sorted_key_with_vars(a);
auto bkey = get_sorted_key_with_vars(b);
SASSERT(akey.size() == bkey.size());
for (unsigned i = 0; i < akey.size(); i++) {
negate_abs_a_le_abs_b(akey[i].second, bkey[i].second, false);
}
assert_abs_val_a_le_abs_var_b(a, b, false);
explain(a);
explain(b);
TRACE("nla_solver", print_lemma(tout););
}
std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
std::vector<rational> r;
for (unsigned j : rm.rvars()) {
r.push_back(abs(vvr(j)));
}
std::sort(r.begin(), r.end());
return r;
}
bool monotone::monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms) {
monotone_array_t lex_sorted;
for (unsigned i : rms) {
lex_sorted.push_back(std::make_pair(get_sorted_key(c().m_emons.canonical[i]), i));
}
std::sort(lex_sorted.begin(), lex_sorted.end(),
[](const std::pair<std::vector<rational>, unsigned> &a,
const std::pair<std::vector<rational>, unsigned> &b) {
return a.first < b.first;
});
TRACE("nla_solver", print_monotone_array(lex_sorted, tout););
return monotonicity_lemma_on_lex_sorted(lex_sorted);
}
void monotone::monotonicity_lemma(monomial const& m) { void monotone::monotonicity_lemma(monomial const& m) {
SASSERT(!check_monomial(m)); SASSERT(!check_monomial(m));
if (c().mon_has_zero(m)) if (c().mon_has_zero(m.vars()))
return; return;
const rational prod_val = abs(c().product_value(m)); const rational prod_val = abs(c().product_value(m.vars()));
const rational m_val = abs(vvr(m)); const rational m_val = abs(vvr(m));
if (m_val < prod_val) if (m_val < prod_val)
monotonicity_lemma_lt(m, prod_val); monotonicity_lemma_lt(m, prod_val);
@ -255,7 +92,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val) { void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val) {
add_empty_lemma(); add_empty_lemma();
for (lpvar j : m) { for (lpvar j : m.vars()) {
c().add_abs_bound(j, llc::GT); c().add_abs_bound(j, llc::GT);
} }
lpvar m_j = m.var(); lpvar m_j = m.var();
@ -271,7 +108,7 @@ void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val
*/ */
void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) { void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
add_empty_lemma(); add_empty_lemma();
for (lpvar j : m) { for (lpvar j : m.vars()) {
c().add_abs_bound(j, llc::LT); c().add_abs_bound(j, llc::LT);
} }
lpvar m_j = m.var(); lpvar m_j = m.var();

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

@ -25,22 +25,13 @@ public:
monotone(core *core); monotone(core *core);
void monotonicity_lemma(); void monotonicity_lemma();
private: private:
typedef vector<std::pair<std::vector<rational>, unsigned>> monotone_array_t;
void print_monotone_array(const monotone_array_t& lex_sorted, std::ostream& out) const;
bool monotonicity_lemma_on_lex_sorted_rm_upper(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted_rm_lower(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted_rm(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
bool monotonicity_lemma_on_lex_sorted(const monotone_array_t& lex_sorted);
bool monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms);
void monotonicity_lemma(monomial const& m); void monotonicity_lemma(monomial const& m);
void monotonicity_lemma_gt(const monomial& m, const rational& prod_val); void monotonicity_lemma_gt(const monomial& m, const rational& prod_val);
void monotonicity_lemma_lt(const monomial& m, const rational& prod_val); void monotonicity_lemma_lt(const monomial& m, const rational& prod_val);
void generate_monl_strict(const smon& a, const smon& b, unsigned strict); std::vector<rational> get_sorted_key(const monomial& rm) const;
void generate_monl(const smon& a, const smon& b); vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monomial& a) const;
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_le_abs_b(lpvar a, lpvar b, bool strict);
void negate_abs_a_lt_abs_b(lpvar a, lpvar b); void negate_abs_a_lt_abs_b(lpvar a, lpvar b);
void assert_abs_val_a_le_abs_var_b(const smon& a, const smon& b, bool strict); void assert_abs_val_a_le_abs_var_b(const monomial& a, const monomial& b, bool strict);
}; };
} }

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

@ -30,22 +30,22 @@ void order::order_lemma() {
unsigned start = random(); unsigned start = random();
unsigned sz = rm_ref.size(); unsigned sz = rm_ref.size();
for (unsigned i = 0; i < sz && !done(); ++i) { for (unsigned i = 0; i < sz && !done(); ++i) {
const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]]; const monomial& rm = c().m_emons[rm_ref[(i + start) % sz]];
order_lemma_on_rmonomial(rm); order_lemma_on_rmonomial(rm);
} }
} }
void order::order_lemma_on_rmonomial(const smon& rm) { void order::order_lemma_on_rmonomial(const monomial& m) {
TRACE("nla_solver_details", TRACE("nla_solver_details",
tout << "rm = " << rm << ", orig = " << pp_mon(c(), c().m_emons[rm]);); tout << "m = " << pp_mon(c(), m););
for (auto ac : factorization_factory_imp(rm, c())) { for (auto ac : factorization_factory_imp(m, c())) {
if (ac.size() != 2) if (ac.size() != 2)
continue; continue;
if (ac.is_mon()) if (ac.is_mon())
order_lemma_on_binomial(*ac.mon()); order_lemma_on_binomial(*ac.mon());
else else
order_lemma_on_factorization(rm, ac); order_lemma_on_factorization(m, ac);
if (done()) if (done())
break; break;
} }
@ -54,7 +54,7 @@ void order::order_lemma_on_rmonomial(const smon& rm) {
void order::order_lemma_on_binomial(const monomial& ac) { void order::order_lemma_on_binomial(const monomial& ac) {
TRACE("nla_solver", tout << pp_mon(c(), ac);); TRACE("nla_solver", tout << pp_mon(c(), ac););
SASSERT(!check_monomial(ac) && ac.size() == 2); SASSERT(!check_monomial(ac) && ac.size() == 2);
const rational mult_val = vvr(ac[0]) * vvr(ac[1]); const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]);
const rational acv = vvr(ac); const rational acv = vvr(ac);
bool gt = acv > mult_val; bool gt = acv > mult_val;
for (unsigned k = 0; k < 2; k++) { for (unsigned k = 0; k < 2; k++) {
@ -64,8 +64,8 @@ void order::order_lemma_on_binomial(const monomial& ac) {
} }
void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) { void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
SASSERT(gt == (vvr(m) > vvr(m[0]) * vvr(m[1]))); SASSERT(gt == (vvr(m) > vvr(m.vars()[0]) * vvr(m.vars()[1])));
order_lemma_on_binomial_sign(m, m[k], m[!k], gt ? 1: -1); order_lemma_on_binomial_sign(m, m.vars()[k], m.vars()[!k], gt ? 1: -1);
} }
/** /**
@ -78,7 +78,7 @@ 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) { void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
SASSERT(!_().mon_has_zero(xy)); SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(vvr(y)); int sy = rat_sign(vvr(y));
add_empty_lemma(); add_empty_lemma();
mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy
@ -89,7 +89,7 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) { void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) {
SASSERT(m1.size() == 2); SASSERT(m1.size() == 2);
lpvar c = m1[k]; lpvar c = m1.vars()[k];
for (monomial const& m2 : _().m_emons.get_factors_of(c)) { for (monomial const& m2 : _().m_emons.get_factors_of(c)) {
order_lemma_on_factor_binomial_rm(m1, k, m2); order_lemma_on_factor_binomial_rm(m1, k, m2);
if (done()) { if (done()) {
@ -99,20 +99,19 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) {
} }
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) { void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
smon const& rm_bd = _().m_emons.canonical[bd]; factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
factor b; factor b;
if (c().divide(rm_bd, d, b)) { if (c().divide(bd, d, b)) {
order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.var()); order_lemma_on_binomial_ac_bd(ac, k, bd, b, d.var());
} }
} }
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const smon& bd, const factor& b, lpvar d) { void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";); tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";);
bool p = !k; bool p = !k;
lpvar a = ac[p]; lpvar a = ac.vars()[p];
lpvar c = ac[k]; lpvar c = ac.vars()[k];
SASSERT(_().m_evars.find(c).var() == d); SASSERT(_().m_evars.find(c).var() == d);
rational acv = vvr(ac); rational acv = vvr(ac);
rational av = vvr(a); rational av = vvr(a);
@ -137,7 +136,7 @@ void order::generate_mon_ol(const monomial& ac,
lpvar a, lpvar a,
const rational& c_sign, const rational& c_sign,
lpvar c, lpvar c,
const smon& bd, const monomial& bd,
const factor& b, const factor& b,
const rational& d_sign, const rational& d_sign,
lpvar d, lpvar d,
@ -159,10 +158,10 @@ void order::generate_mon_ol(const monomial& ac,
// a >< b && c < 0 => ac <> bc // a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c // ac[k] plays the role of c
bool order::order_lemma_on_ac_and_bc(const smon& rm_ac, bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
const factorization& ac_f, const factorization& ac_f,
bool k, bool k,
const smon& rm_bd) { const monomial& rm_bd) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "rm_ac = " << rm_ac << "\n"; tout << "rm_ac = " << rm_ac << "\n";
tout << "rm_bd = " << rm_bd << "\n"; tout << "rm_bd = " << rm_bd << "\n";
@ -176,10 +175,8 @@ bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
// TBD: document what lemma is created here. // TBD: document what lemma is created here.
void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) { void order::order_lemma_on_factorization(const monomial& m, const factorization& ab) {
const monomial& m = _().m_emons[rm]; rational sign = m.rsign();
TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
rational sign = _().m_emons.orig_sign(rm);
for (factor f: ab) for (factor f: ab)
sign *= _().canonize_sign(f); sign *= _().canonize_sign(f);
const rational fv = vvr(ab[0]) * vvr(ab[1]); const rational fv = vvr(ab[0]) * vvr(ab[1]);
@ -194,26 +191,25 @@ void order::order_lemma_on_factorization(const smon& rm, const factorization& ab
for (unsigned j = 0, k = 1; j < 2; j++, k--) { for (unsigned j = 0, k = 1; j < 2; j++, k--) {
order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt); order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
explain(ab); explain(m); explain(ab); explain(m);
explain(rm);
TRACE("nla_solver", _().print_lemma(tout);); TRACE("nla_solver", _().print_lemma(tout););
order_lemma_on_ac_explore(rm, ab, j == 1); order_lemma_on_ac_explore(m, ab, j == 1);
} }
} }
bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, bool k) { bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool k) {
const factor c = ac[k]; const factor c = ac[k];
TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); ); TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
if (c.is_var()) { if (c.is_var()) {
TRACE("nla_solver", tout << "var(c) = " << var(c);); TRACE("nla_solver", tout << "var(c) = " << var(c););
for (monomial const& bc : _().m_emons.get_use_list(c.var())) { for (monomial const& bc : _().m_emons.get_use_list(c.var())) {
if (order_lemma_on_ac_and_bc(rm ,ac, k, _().m_emons.canonical[bc])) { if (order_lemma_on_ac_and_bc(rm ,ac, k, bc)) {
return true; return true;
} }
} }
} }
else { else {
for (monomial const& bc : _().m_emons.get_factors_of(c.var())) { for (monomial const& bc : _().m_emons.get_factors_of(c.var())) {
if (order_lemma_on_ac_and_bc(rm , ac, k, _().m_emons.canonical[bc])) { if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) {
return true; return true;
} }
} }
@ -223,11 +219,11 @@ bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, b
// |c_sign| = 1, and c*c_sign > 0 // |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
void order::generate_ol(const smon& ac, void order::generate_ol(const monomial& ac,
const factor& a, const factor& a,
int c_sign, int c_sign,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b, const factor& b,
llc ab_cmp) { llc ab_cmp) {
add_empty_lemma(); add_empty_lemma();
@ -251,10 +247,10 @@ void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const ra
} }
bool order::order_lemma_on_ac_and_bc_and_factors(const smon& ac, bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
const factor& a, const factor& a,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b) { const factor& b) {
auto cv = vvr(c); auto cv = vvr(c);
int c_sign = nla::rat_sign(cv); int c_sign = nla::rat_sign(cv);

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

@ -31,23 +31,23 @@ public:
private: private:
bool order_lemma_on_ac_and_bc_and_factors(const smon& ac, bool order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
const factor& a, const factor& a,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b); const factor& b);
// a >< b && c > 0 => ac >< bc // a >< b && c > 0 => ac >< bc
// a >< b && c < 0 => ac <> bc // a >< b && c < 0 => ac <> bc
// ac[k] plays the role of c // ac[k] plays the role of c
bool order_lemma_on_ac_and_bc(const smon& rm_ac, bool order_lemma_on_ac_and_bc(const monomial& rm_ac,
const factorization& ac_f, const factorization& ac_f,
bool k, bool k,
const smon& rm_bd); const monomial& rm_bd);
bool order_lemma_on_ac_explore(const smon& rm, const factorization& ac, bool k); bool order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool k);
void order_lemma_on_factorization(const smon& rm, const factorization& ab); void order_lemma_on_factorization(const monomial& rm, const factorization& ab);
/** /**
\brief Add lemma: \brief Add lemma:
@ -65,18 +65,18 @@ private:
void order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt); 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, bool k); void order_lemma_on_factor_binomial_explore(const monomial& m, bool k);
void order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd); void order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd);
void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const smon& bd, const factor& b, lpvar d); void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d);
void order_lemma_on_binomial_k(const monomial& m, bool k, bool gt); void order_lemma_on_binomial_k(const monomial& m, bool k, bool gt);
void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign); 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_binomial(const monomial& ac);
void order_lemma_on_rmonomial(const smon& rm); void order_lemma_on_rmonomial(const monomial& rm);
// |c_sign| = 1, and c*c_sign > 0 // |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
void generate_ol(const smon& ac, void generate_ol(const monomial& ac,
const factor& a, const factor& a,
int c_sign, int c_sign,
const factor& c, const factor& c,
const smon& bc, const monomial& bc,
const factor& b, const factor& b,
llc ab_cmp); llc ab_cmp);
@ -84,7 +84,7 @@ private:
lpvar a, lpvar a,
const rational& c_sign, const rational& c_sign,
lpvar c, lpvar c,
const smon& bd, const monomial& bd,
const factor& b, const factor& b,
const rational& d_sign, const rational& d_sign,
lpvar d, lpvar d,

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

@ -30,13 +30,12 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
return out << "(" << a << ", " << b << ")"; return out << "(" << a << ", " << b << ")";
} }
void tangents::generate_simple_tangent_lemma(const smon* rm) { void tangents::generate_simple_tangent_lemma(const monomial& m) {
if (rm->size() != 2) if (m.size() != 2)
return; return;
TRACE("nla_solver", tout << "rm:" << *rm << std::endl;); TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
m_core->add_empty_lemma(); c().add_empty_lemma();
const monomial & m = c().m_emons[rm->var()]; const rational v = c().product_value(m.vars());
const rational v = c().product_value(m);
const rational mv = vvr(m); const rational mv = vvr(m);
SASSERT(mv != v); SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero()); SASSERT(!mv.is_zero() && !v.is_zero());
@ -47,15 +46,15 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
} }
bool gt = abs(mv) > abs(v); bool gt = abs(mv) > abs(v);
if (gt) { if (gt) {
for (lpvar j : m) { for (lpvar j : m.vars()) {
const rational jv = vvr(j); const rational jv = vvr(j);
rational js = rational(nla::rat_sign(jv)); rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT); c().mk_ineq(js, j, llc::LT);
c().mk_ineq(js, j, llc::GT, jv); c().mk_ineq(js, j, llc::GT, jv);
} }
c().mk_ineq(sign, rm->var(), llc::LE, std::max(v, rational(-1))); c().mk_ineq(sign, m.var(), llc::LE, std::max(v, rational(-1)));
} else { } else {
for (lpvar j : m) { for (lpvar j : m.vars()) {
const rational jv = vvr(j); const rational jv = vvr(j);
rational js = rational(nla::rat_sign(jv)); rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0))); c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
@ -70,18 +69,18 @@ void tangents::tangent_lemma() {
bfc bf; bfc bf;
lpvar j; lpvar j;
rational sign; rational sign;
const smon* rm = nullptr; const monomial* rm = nullptr;
if (c().find_bfc_to_refine(bf, j, sign, rm)) { if (c().find_bfc_to_refine(bf, j, sign, rm)) {
tangent_lemma_bf(bf, j, sign, rm); tangent_lemma_bf(bf, j, sign, rm);
} else { } else {
TRACE("nla_solver", tout << "cannot find a bfc to refine\n"; ); TRACE("nla_solver", tout << "cannot find a bfc to refine\n"; );
if (rm != nullptr) if (rm != nullptr)
generate_simple_tangent_lemma(rm); generate_simple_tangent_lemma(*rm);
} }
} }
void tangents::generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp) { void tangents::generate_explanations_of_tang_lemma(const monomial& rm, const bfc& bf, lp::explanation& exp) {
// here we repeat the same explanation for each lemma // here we repeat the same explanation for each lemma
c().explain(rm, exp); c().explain(rm, exp);
c().explain(bf.m_x, exp); c().explain(bf.m_x, exp);
@ -109,7 +108,7 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
t.add_coeff_var( j_sign, j); t.add_coeff_var( j_sign, j);
c().mk_ineq(t, sbelow? llc::GT : llc::LT, - a*b); 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 smon* rm){ void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* rm){
point a, b; point a, b;
point xy (vvr(bf.m_x), vvr(bf.m_y)); point xy (vvr(bf.m_x), vvr(bf.m_y));
rational correct_mult_val = xy.x * xy.y; rational correct_mult_val = xy.x * xy.y;

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

@ -54,11 +54,11 @@ public:
void tangent_lemma(); void tangent_lemma();
private: private:
void generate_simple_tangent_lemma(const smon* rm); void generate_simple_tangent_lemma(const monomial&);
void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp); void generate_explanations_of_tang_lemma(const monomial& rm, const bfc& bf, lp::explanation& exp);
void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm); void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* 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_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); void generate_two_tang_lines(const bfc & bf, const point& xy, const rational& sign, lpvar j);

7
src/util/lp/nra_solver.cpp
View file

@ -13,7 +13,8 @@
namespace nra { namespace nra {
typedef nla::monomial mon_eq; typedef nla::mon_eq mon_eq;
typedef nla::variable_map_type variable_map_type; typedef nla::variable_map_type variable_map_type;
struct solver::imp { struct solver::imp {
lp::lar_solver& s; lp::lar_solver& s;
@ -136,7 +137,7 @@ typedef nla::variable_map_type variable_map_type;
void add_monomial_eq(mon_eq const& m) { void add_monomial_eq(mon_eq const& m) {
polynomial::manager& pm = m_nlsat->pm(); polynomial::manager& pm = m_nlsat->pm();
svector<polynomial::var> vars; svector<polynomial::var> vars;
for (auto v : m) { for (auto v : m.vars()) {
vars.push_back(lp2nl(v)); vars.push_back(lp2nl(v));
} }
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm); polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
@ -227,7 +228,7 @@ typedef nla::variable_map_type variable_map_type;
std::ostream& display(std::ostream& out) const { std::ostream& display(std::ostream& out) const {
for (auto m : m_monomials) { for (auto m : m_monomials) {
out << "v" << m.var() << " = "; out << "v" << m.var() << " = ";
for (auto v : m) { for (auto v : m.vars()) {
out << "v" << v << " "; out << "v" << v << " ";
} }
out << "\n"; out << "\n";