Skip to content

Commit

Permalink
Add const qualifiers to comparison operators and update iterator equa…
Browse files Browse the repository at this point in the history 
…lity checks in various classes
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Sep 23, 2024
1 parent a62fede commit 4b4a282
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 26 deletions.
26 changes: 13 additions & 13 deletions src/api/c++/z3++.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1603,10 +1603,10 @@ namespace z3 {
unsigned i;
public:
iterator(expr& e, unsigned i): e(e), i(i) {}
bool operator==(iterator const& other) noexcept {
bool operator==(iterator const& other) const noexcept {
return i == other.i;
}
bool operator!=(iterator const& other) noexcept {
bool operator!=(iterator const& other) const noexcept {
return i != other.i;
}
expr operator*() const { return e.arg(i); }
Expand Down Expand Up @@ -1703,28 +1703,28 @@ namespace z3 {

inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }

inline expr operator==(expr const & a, expr const & b) {
inline expr operator==(expr const & a, expr const & b) const {
check_context(a, b);
Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
inline expr operator==(expr const & a, int b) const { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
inline expr operator==(expr const & a, double b) const { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
inline expr operator==(double a, expr const & b) const { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }

inline expr operator!=(expr const & a, expr const & b) {
inline expr operator!=(expr const & a, expr const & b) const {
check_context(a, b);
Z3_ast args[2] = { a, b };
Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
a.check_error();
return expr(a.ctx(), r);
}
inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
inline expr operator!=(expr const & a, int b) const { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
inline expr operator!=(int a, expr const & b) const { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
inline expr operator!=(expr const & a, double b) const { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
inline expr operator!=(double a, expr const & b) const { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }

inline expr operator+(expr const & a, expr const & b) {
check_context(a, b);
Expand Down Expand Up @@ -2957,10 +2957,10 @@ namespace z3 {
expr_vector const * operator->() const { return &(operator*()); }
expr_vector const& operator*() const noexcept { return m_cube; }

bool operator==(cube_iterator const& other) noexcept {
bool operator==(cube_iterator const& other) const noexcept {
return other.m_end == m_end;
};
bool operator!=(cube_iterator const& other) noexcept {
bool operator!=(cube_iterator const& other) const noexcept {
return other.m_end != m_end;
};

Expand Down
16 changes: 6 additions & 10 deletions src/muz/rel/dl_base.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1113,7 +1113,7 @@ namespace datalog {

virtual row_interface & operator*() = 0;
virtual void operator++() = 0;
virtual bool operator==(const iterator_core & it) {
virtual bool operator==(const iterator_core & it) const {
//we worry about the equality operator only because of checking
//the equality with the end() iterator
return is_finished() && it.is_finished();
Expand Down Expand Up @@ -1142,7 +1142,7 @@ namespace datalog {

virtual table_element operator*() = 0;
virtual void operator++() = 0;
virtual bool operator==(const row_iterator_core & it) {
virtual bool operator==(const row_iterator_core & it) const {
//we worry about the equality operator only because of checking
//the equality with the end() iterator
return is_finished() && it.is_finished();
Expand All @@ -1169,10 +1169,8 @@ namespace datalog {
{ return &(*(*m_core)); }
iterator & operator++()
{ ++(*m_core); return *this; }
bool operator==(const iterator & it)
{ return (*m_core)==(*it.m_core); }
bool operator!=(const iterator & it)
{ return !operator==(it); }
bool operator==(const iterator & it) const { return (*m_core)==(*it.m_core); }
bool operator!=(const iterator & it) const { return !operator==(it); }
};

class row_iterator {
Expand All @@ -1187,10 +1185,8 @@ namespace datalog {
{ return *(*m_core); }
row_iterator & operator++()
{ ++(*m_core); return *this; }
bool operator==(const row_iterator & it)
{ return (*m_core)==(*it.m_core); }
bool operator!=(const row_iterator & it)
{ return !operator==(it); }
bool operator==(const row_iterator & it) const { return (*m_core)==(*it.m_core); }
bool operator!=(const row_iterator & it) const { return !operator==(it); }
};

virtual iterator begin() const = 0;
Expand Down
2 changes: 0 additions & 2 deletions src/sat/sat_solver/inc_sat_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,8 +179,6 @@ class inc_sat_solver : public solver {
void initialize_values() {
if (m_mcs.back())
m_mcs.back()->convert_initialize_value(m_var2value);
if (m_mcs.back())
m_mcs.back()->display(verbose_stream());

for (auto & [var, value] : m_var2value) {
sat::bool_var b = m_map.to_bool_var(var);
Expand Down
1 change: 0 additions & 1 deletion src/sat/tactic/sat_tactic.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,6 @@ class sat_tactic : public tactic {
}

void user_propagate_initialize_value(expr* var, expr* value) override {
verbose_stream() << "initialize-value\n";
m_var2value.push_back({ expr_ref(var, m), expr_ref(value, m) });
}

Expand Down

0 comments on commit 4b4a282

Please sign in to comment.