Skip to content

Commit

Permalink
fix crashes in elim-uncnstr2
Browse files Browse the repository at this point in the history
This would crash before:
(declare-fun x () (_ BitVec 4))
(assert (not (bvule x #x1)))
(apply elim-uncnstr2)

That's because the index_set iterator was querying qtail to compute the end of the iteration
But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case.
The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals
Solve the issue by freezing the qtail for the iteration loop.
This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before

@NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you
  • Loading branch information
nunoplopes committed Dec 11, 2022
1 parent ee307dd commit a302c2f
Showing 1 changed file with 6 additions and 9 deletions.
15 changes: 6 additions & 9 deletions src/ast/simplifiers/dependent_expr_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -116,20 +116,17 @@ class dependent_expr_simplifier {
unsigned qtail() const { return m_fmls.qtail(); }
struct iterator {
dependent_expr_simplifier& s;
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 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 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) {}
};

Expand Down

1 comment on commit a302c2f

@NikolajBjorner
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

doesn't work with tactics: if you add "false" to a goal it truncates.

Please sign in to comment.