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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-11 14:03:22 -08:00
parent 2d43ccc4c6
commit 2520dcb04b
2 changed files with 5 additions and 8 deletions
.github/workflows
coverage.yml
src/ast/simplifiers
dependent_expr_state.h

2
.github/workflows/coverage.yml vendored
View file

@ -58,7 +58,7 @@ jobs:
- name: Run examples
run: |
${{github.workspace}}/build/examples/c_example_build_dir/c_example
# Disabled: ${{github.workspace}}/build/examples/c_example_build_dir/c_example
${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example
${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help
${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt

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

@ -116,13 +116,10 @@ protected:
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 > s.qtail()) m_index = m_end; else ++m_index; return *this; }
unsigned operator*() const { return m_index; }
};