From 2d43ccc4c6a4f63c2c6da58302a02c5610f98a30 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sun, 11 Dec 2022 21:37:25 +0000
Subject: [PATCH] Revert "fix crashes in elim-uncnstr2"
This reverts commit a302c2f15ee0e4d24ce9036050fffd8e827fe053.
---
src/ast/simplifiers/dependent_expr_state.h | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index f9faee549..85b6352ad 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -116,17 +116,20 @@ protected:
unsigned qtail() const { return m_fmls.qtail(); }
struct iterator {
dependent_expr_simplifier& s;
- 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 = m_end; else ++m_index; return *this; }
+ unsigned m_index = 0;
+ bool at_end = false;
+ unsigned index() const { return at_end ? s.qtail() : std::min(m_index, s.qtail()); }
+ iterator(dependent_expr_simplifier& s, unsigned i) : s(s), m_index(i), at_end(i == s.qtail()) {}
+ bool operator==(iterator const& other) const { return index() == other.index(); }
+ bool operator!=(iterator const& other) const { return !(*this == other); }
+ iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent()) at_end = true; 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(), s.qtail()); }
- iterator end() { return iterator(s, s.qtail(), s.qtail()); }
+ iterator begin() { return iterator(s, s.qhead()); }
+ iterator end() { return iterator(s, s.qtail()); }
index_set(dependent_expr_simplifier& s) : s(s) {}
};