From 7eeba3a917f7937b59302649d2a4b15453c6d257 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 21 Apr 2019 14:05:36 -0700 Subject: [PATCH] renaming the smon fields to distingush them from monomial fields Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.h | 620 ++++++++++++++-------------- src/util/lp/nla_common.cpp | 6 - src/util/lp/nla_monotone_lemmas.cpp | 2 +- 3 files changed, 312 insertions(+), 316 deletions(-) diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 3e65a23a5..fe4db08d3 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -33,13 +33,13 @@ namespace nla { */ class smon { lpvar m_var; // variable representing original monomial - svector m_vars; - bool m_sign; + svector 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_sign(false), m_next(idx), m_prev(idx), m_visited(0) {} + 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; } @@ -47,332 +47,334 @@ public: unsigned& prev() { return m_prev; } unsigned visited() const { return m_visited; } unsigned& visited() { return m_visited; } - svector const& vars() const { return m_vars; } + svector const& vars() const { return m_rvars; } svector::const_iterator begin() const { return vars().begin(); } svector::const_iterator end() const { return vars().end(); } - unsigned size() const { return m_vars.size(); } - lpvar operator[](unsigned i) const { return m_vars[i]; } - bool sign() const { return m_sign; } - rational rsign() const { return rational(m_sign ? -1 : 1); } - void reset() { m_sign = false; m_vars.reset(); } - void push_var(signed_var sv) { m_sign ^= sv.sign(); m_vars.push_back(sv.var()); } + 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_vars.begin(), m_vars.end()); + 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 << " "; + // 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 { - /** - \brief singly-lined cyclic list of monomial indices where variable occurs. - Each variable points to the head and tail of the cyclic list. - Initially, head and tail are nullptr. - New elements are inserted in the beginning of the list. - Two lists are merged when equivalence class representatives are merged, - and the merge is undone when the representative variables are unmerged. - */ - struct cell { - cell(unsigned mIndex, cell* c): m_next(c), m_index(mIndex) {} - cell* m_next; - unsigned m_index; - }; - struct head_tail { - head_tail(): m_head(nullptr), m_tail(nullptr) {} - cell* m_head; - cell* m_tail; - }; - struct hash_canonical { - emonomials& em; - hash_canonical(emonomials& em): em(em) {} + /** + \brief singly-lined cyclic list of monomial indices where variable occurs. + Each variable points to the head and tail of the cyclic list. + Initially, head and tail are nullptr. + New elements are inserted in the beginning of the list. + Two lists are merged when equivalence class representatives are merged, + and the merge is undone when the representative variables are unmerged. + */ + struct cell { + cell(unsigned mIndex, cell* c): m_next(c), m_index(mIndex) {} + cell* m_next; + unsigned m_index; + }; + struct head_tail { + head_tail(): m_head(nullptr), m_tail(nullptr) {} + cell* m_head; + cell* m_tail; + }; + struct hash_canonical { + emonomials& em; + hash_canonical(emonomials& em): em(em) {} - unsigned operator()(lpvar v) const { - auto const& vec = em.m_canonized[em.m_var2index[v]].vars(); - return string_hash(reinterpret_cast(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10); - } - }; - - - - /** - \brief private fields used by emonomials for maintaining state of canonized monomials. - */ - - struct eq_canonical { - emonomials& em; - eq_canonical(emonomials& em): em(em) {} - bool operator()(lpvar u, lpvar v) const { - auto const& uvec = em.m_canonized[em.m_var2index[u]].vars(); - auto const& vvec = em.m_canonized[em.m_var2index[v]].vars(); - return uvec == vvec; - } - }; - - var_eqs& m_ve; - mutable vector m_monomials; // set of monomials - mutable unsigned_vector m_var2index; // var_mIndex -> mIndex - unsigned_vector m_lim; // backtracking point - mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator - region m_region; // region for allocating linked lists - mutable vector m_canonized; // canonized versions of signed variables - mutable svector m_use_lists; // use list of monomials where variables occur. - hash_canonical m_cg_hash; - eq_canonical m_cg_eq; - hashtable m_cg_table; // congruence (canonical) table. - - void inc_visited() const; - - void remove_cell(head_tail& v, unsigned mIndex); - void insert_cell(head_tail& v, unsigned mIndex); - void merge_cells(head_tail& root, head_tail& other); - void unmerge_cells(head_tail& root, head_tail& other); - - void remove_cg(lpvar v); - void insert_cg(lpvar v); - void insert_cg(unsigned idx, monomial const& m); - void remove_cg(unsigned idx, monomial const& m); - void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } - - void do_canonize(monomial const& m) const; - - cell* head(lpvar v) const; - void set_visited(monomial const& m) const; - bool is_visited(monomial const& m) const; - - public: - /** - \brief emonomials builds on top of var_eqs. - push and pop on emonomials calls push/pop on var_eqs, so no - other calls to push/pop to the var_eqs should take place. - */ - emonomials(var_eqs& ve): - m_ve(ve), - m_visited(0), - m_cg_hash(*this), - m_cg_eq(*this), - m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq), - canonical(*this) { - m_ve.set_merge_handler(this); + unsigned operator()(lpvar v) const { + auto const& vec = em.m_canonized[em.m_var2index[v]].vars(); + return string_hash(reinterpret_cast(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10); } - - /** - \brief push/pop scopes. - The life-time of a merge is local within a scope. - */ - void push(); - - void pop(unsigned n); - - /** - \brief create a monomial from an equality v := vs - */ - void add(lpvar v, unsigned sz, lpvar const* vs); - void add(lpvar v, svector const& vs) { add(v, vs.size(), vs.c_ptr()); } - void add(lpvar v, lpvar x, lpvar y) { lpvar vs[2] = { x, y }; add(v, 2, vs); } - void add(lpvar v, lpvar x, lpvar y, lpvar z) { lpvar vs[3] = { x, y, z }; add(v, 3, 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 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. - */ - //smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; } - smon const& rep(smon const& sv) const { - unsigned j = -1; - m_cg_table.find(sv.var(), j); - return m_canonized[m_var2index[j]]; + /** + \brief private fields used by emonomials for maintaining state of canonized monomials. + */ + + struct eq_canonical { + emonomials& em; + eq_canonical(emonomials& em): em(em) {} + bool operator()(lpvar u, lpvar v) const { + auto const& uvec = em.m_canonized[em.m_var2index[u]].vars(); + auto const& vvec = em.m_canonized[em.m_var2index[v]].vars(); + return uvec == vvec; } - - /** - \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. - */ - bool canonize_divides(monomial const& m1, monomial const& m2) const; - - /** - \brief produce explanation for monomial canonization. - */ - void explain_canonized(monomial const& m, lp::explanation& exp); - - /** - \brief iterator over monomials that are declared. - */ - vector::const_iterator begin() const { return m_monomials.begin(); } - vector::const_iterator end() const { return m_monomials.end(); } - - /** - \brief iterators over monomials where an equivalent variable is used - */ - class iterator { - emonomials const& m; - cell* m_cell; - bool m_touched; - public: - 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]; } - iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; } - 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; } - }; - - class use_list { - emonomials const& m; - lpvar m_var; - cell* head() { return m.head(m_var); } - public: - use_list(emonomials const& m, lpvar v): m(m), m_var(v) {} - iterator begin() { return iterator(m, head(), false); } - iterator end() { return iterator(m, head(), true); } - }; - - use_list get_use_list(lpvar v) const { return use_list(*this, v); } - - /** - \brief retrieve monomials m' where m is a proper factor of modulo current equalities. - */ - class pf_iterator { - emonomials const& m; - monomial const* m_mon; // monomial - iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors. - iterator m_end; - - void fast_forward(); - public: - pf_iterator(emonomials const& m, monomial const& mon, bool at_end); - pf_iterator(emonomials const& m, lpvar v, bool at_end); - monomial const& operator*() { return *m_it; } - pf_iterator& operator++() { ++m_it; fast_forward(); return *this; } - 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; } - }; - - class factors_of { - emonomials const& m; - monomial const* mon; - lpvar m_var; - public: - factors_of(emonomials const& m, monomial const& mon): m(m), mon(&mon), m_var(UINT_MAX) {} - 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 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(lpvar v) const { inc_visited(); return factors_of(*this, v); } - - smon const* find_canonical(svector const& vars) const; - - /** - \brief iterator over sign equivalent monomials. - These are monomials that are equivalent modulo m_var_eqs amd modulo signs. - */ - class sign_equiv_monomials_it { - emonomials const& m; - unsigned m_index; - bool m_touched; - public: - sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end): - m(m), m_index(idx), m_touched(at_end) {} - - monomial const& operator*() { return m.m_monomials[m_index]; } - - sign_equiv_monomials_it& operator++() { - m_touched = true; - m_index = m.m_canonized[m_index].next(); - return *this; - } - - sign_equiv_monomials_it operator++(int) { - sign_equiv_monomials_it tmp = *this; - ++*this; - return tmp; - } - - bool operator==(sign_equiv_monomials_it const& other) const { - return m_index == other.m_index && m_touched == other.m_touched; - } - - bool operator!=(sign_equiv_monomials_it const& other) const { - return m_index != other.m_index || m_touched != other.m_touched; - } - }; - - class sign_equiv_monomials { - emonomials& em; - monomial const& m; - unsigned index() const { return em.m_var2index[m.var()]; } - public: - sign_equiv_monomials(emonomials & em, monomial const& m): em(em), m(m) {} - sign_equiv_monomials_it begin() { return sign_equiv_monomials_it(em, index(), false); } - sign_equiv_monomials_it end() { return sign_equiv_monomials_it(em, index(), true); } - }; - - 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(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); } - - /** - \brief display state of emonomials - */ - std::ostream& display(std::ostream& out) const; - - /** - \brief - these are merge event handlers to interect the union-find handlers. - r2 becomes the new root. r2 is the root of v2, r1 is the old root of v1 - */ - void merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; - - void after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; - - void unmerge_eh(signed_var r2, signed_var r1) override; - }; - inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); } + var_eqs& m_ve; + mutable vector m_monomials; // set of monomials + mutable unsigned_vector m_var2index; // var_mIndex -> mIndex + unsigned_vector m_lim; // backtracking point + mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator + region m_region; // region for allocating linked lists + mutable vector m_canonized; // canonized versions of signed variables + mutable svector m_use_lists; // use list of monomials where variables occur. + hash_canonical m_cg_hash; + eq_canonical m_cg_eq; + hashtable m_cg_table; // congruence (canonical) table. + + void inc_visited() const; + + void remove_cell(head_tail& v, unsigned mIndex); + void insert_cell(head_tail& v, unsigned mIndex); + void merge_cells(head_tail& root, head_tail& other); + void unmerge_cells(head_tail& root, head_tail& other); + + void remove_cg(lpvar v); + void insert_cg(lpvar v); + void insert_cg(unsigned idx, monomial const& m); + void remove_cg(unsigned idx, monomial const& m); + void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } + + void do_canonize(monomial const& m) const; + + cell* head(lpvar v) const; + void set_visited(monomial const& m) const; + bool is_visited(monomial const& m) const; + +public: + /** + \brief emonomials builds on top of var_eqs. + push and pop on emonomials calls push/pop on var_eqs, so no + other calls to push/pop to the var_eqs should take place. + */ + emonomials(var_eqs& ve): + m_ve(ve), + m_visited(0), + m_cg_hash(*this), + m_cg_eq(*this), + m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq), + canonical(*this) { + m_ve.set_merge_handler(this); + } + + /** + \brief push/pop scopes. + The life-time of a merge is local within a scope. + */ + void push(); + + void pop(unsigned n); + + /** + \brief create a monomial from an equality v := vs + */ + void add(lpvar v, unsigned sz, lpvar const* vs); + void add(lpvar v, svector const& vs) { add(v, vs.size(), vs.c_ptr()); } + void add(lpvar v, lpvar x, lpvar y) { lpvar vs[2] = { x, y }; add(v, 2, vs); } + void add(lpvar v, lpvar x, lpvar y, lpvar z) { lpvar vs[3] = { x, y, z }; add(v, 3, 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 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. + */ + //smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; } + smon const& rep(smon const& sv) const { + unsigned j = -1; + m_cg_table.find(sv.var(), j); + return m_canonized[m_var2index[j]]; + } + + /** + \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. + */ + bool canonize_divides(monomial const& m1, monomial const& m2) const; + + /** + \brief produce explanation for monomial canonization. + */ + void explain_canonized(monomial const& m, lp::explanation& exp); + + /** + \brief iterator over monomials that are declared. + */ + vector::const_iterator begin() const { return m_monomials.begin(); } + vector::const_iterator end() const { return m_monomials.end(); } + + /** + \brief iterators over monomials where an equivalent variable is used + */ + class iterator { + emonomials const& m; + cell* m_cell; + bool m_touched; + public: + 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]; } + iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; } + 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; } + }; + + class use_list { + emonomials const& m; + lpvar m_var; + cell* head() { return m.head(m_var); } + public: + use_list(emonomials const& m, lpvar v): m(m), m_var(v) {} + iterator begin() { return iterator(m, head(), false); } + iterator end() { return iterator(m, head(), true); } + }; + + use_list get_use_list(lpvar v) const { return use_list(*this, v); } + + /** + \brief retrieve monomials m' where m is a proper factor of modulo current equalities. + */ + class pf_iterator { + emonomials const& m; + monomial const* m_mon; // monomial + iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors. + iterator m_end; + + void fast_forward(); + public: + pf_iterator(emonomials const& m, monomial const& mon, bool at_end); + pf_iterator(emonomials const& m, lpvar v, bool at_end); + monomial const& operator*() { return *m_it; } + pf_iterator& operator++() { ++m_it; fast_forward(); return *this; } + 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; } + }; + + class factors_of { + emonomials const& m; + monomial const* mon; + lpvar m_var; + public: + factors_of(emonomials const& m, monomial const& mon): m(m), mon(&mon), m_var(UINT_MAX) {} + 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 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(lpvar v) const { inc_visited(); return factors_of(*this, v); } + + smon const* find_canonical(svector const& vars) const; + + /** + \brief iterator over sign equivalent monomials. + These are monomials that are equivalent modulo m_var_eqs amd modulo signs. + */ + class sign_equiv_monomials_it { + emonomials const& m; + unsigned m_index; + bool m_touched; + public: + sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end): + m(m), m_index(idx), m_touched(at_end) {} + + monomial const& operator*() { return m.m_monomials[m_index]; } + + sign_equiv_monomials_it& operator++() { + m_touched = true; + m_index = m.m_canonized[m_index].next(); + return *this; + } + + sign_equiv_monomials_it operator++(int) { + sign_equiv_monomials_it tmp = *this; + ++*this; + return tmp; + } + + bool operator==(sign_equiv_monomials_it const& other) const { + return m_index == other.m_index && m_touched == other.m_touched; + } + + bool operator!=(sign_equiv_monomials_it const& other) const { + return m_index != other.m_index || m_touched != other.m_touched; + } + }; + + class sign_equiv_monomials { + emonomials& em; + monomial const& m; + unsigned index() const { return em.m_var2index[m.var()]; } + public: + sign_equiv_monomials(emonomials & em, monomial const& m): em(em), m(m) {} + sign_equiv_monomials_it begin() { return sign_equiv_monomials_it(em, index(), false); } + sign_equiv_monomials_it end() { return sign_equiv_monomials_it(em, index(), true); } + }; + + 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(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); } + + /** + \brief display state of emonomials + */ + std::ostream& display(std::ostream& out) const; + + /** + \brief + these are merge event handlers to interect the union-find handlers. + r2 becomes the new root. r2 is the root of v2, r1 is the old root of v1 + */ + void merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; + + void after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; + + void unmerge_eh(signed_var r2, signed_var r1) override; + +}; + +inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); } } diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp index be36f51a7..dbb949808 100644 --- a/src/util/lp/nla_common.cpp +++ b/src/util/lp/nla_common.cpp @@ -107,12 +107,6 @@ std::ostream& common::print_monomial(const monomial & m, std::ostream& out) cons return c().print_monomial(m, out); } -//std::ostream& common::print_rooted_monomial(const smon& rm, std::ostream& out) const { -// return c().print_rooted_monomial(rm, out); -//} -//std::ostream& common::print_rooted_monomial_with_vars(const smon& rm, std::ostream& out) const { -// return c().print_rooted_monomial_with_vars(rm, out); -//} std::ostream& common::print_factor(const factor & f, std::ostream& out) const { return c().print_factor(f, out); } diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/util/lp/nla_monotone_lemmas.cpp index 36b0014b7..a39eb4215 100644 --- a/src/util/lp/nla_monotone_lemmas.cpp +++ b/src/util/lp/nla_monotone_lemmas.cpp @@ -48,7 +48,7 @@ void monotone::print_monotone_array(const monotone_array_t& lex_sorted, 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;); + 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];