mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

tidy^2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 17:04:07 -07:00 • committed by Lev Nachmanson
parent 2e2c42f7c8
commit 2b98c7e157
1 changed files with 6 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/lp/lar_term.h
View file

@ -129,23 +129,15 @@ public:
class const_iterator { class const_iterator {
u_map< mpq>::iterator m_it; u_map< mpq>::iterator m_it;
typedef const_iterator self_type;
typedef ival value_type;
typedef ival reference;
typedef int difference_type;
typedef std::forward_iterator_tag iterator_category;
public: public:
reference operator*() const { return ival(m_it->m_key, m_it->m_value); } ival operator*() const { return ival(m_it->m_key, m_it->m_value); }
self_type operator++() { self_type i = *this; m_it++; return i; } const_iterator operator++() { const_iterator i = *this; m_it++; return i; }
self_type operator++(int) { m_it++; return *this; } const_iterator operator++(int) { m_it++; return *this; }
const_iterator(u_map<mpq>::iterator it) : m_it(it) {} const_iterator(u_map<mpq>::iterator it) : m_it(it) {}
bool operator==(const self_type &other) const { return m_it == other.m_it; } bool operator==(const const_iterator &other) const { return m_it == other.m_it; }
bool operator!=(const self_type &other) const { return !(*this == other); } bool operator!=(const const_iterator &other) const { return !(*this == other); }
}; };
bool is_normalized() const { bool is_normalized() const {
lpvar min_var = -1; lpvar min_var = -1;
mpq c; mpq c;