mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix build

Browse source
This commit is contained in:
Nuno Lopes 2022-12-11 22:17:11 +00:00
parent d308b8f555
commit cb8603177e
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/simplifiers/dependent_expr_state.h
View file

@ -119,14 +119,14 @@ protected:
unsigned m_index, m_end;
iterator(dependent_expr_simplifier& s, unsigned i, unsigned end) : s(s), m_index(i), m_end(end) {}
bool operator!=(iterator const& other) const { return m_index != other.m_index; }
iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent() || m_index > s.qtail()) m_index = m_end; else ++m_index; return *this; }
iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent() || m_index >= s.qtail()) m_index = m_end; else ++m_index; return *this; }
unsigned operator*() const { return m_index; }
};
struct index_set {
dependent_expr_simplifier& s;
iterator begin() { return iterator(s, s.qhead()); }
iterator end() { return iterator(s, s.qtail()); }
iterator begin() { return iterator(s, s.qhead(), s.qtail()); }
iterator end() { return iterator(s, s.qtail(), s.qtail()); }
index_set(dependent_expr_simplifier& s) : s(s) {}
};