mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Add const qualifiers to comparison operators and update iterator equality checks in various classes

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-23 11:45:11 +01:00
parent a62fede64b
commit 4b4a28239f
4 changed files with 19 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/api/c++/z3++.h
View file

@ -1603,10 +1603,10 @@ namespace z3 {
unsigned i; unsigned i;
public: public:
iterator(expr& e, unsigned i): e(e), i(i) {} 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; return i == other.i;
} }
bool operator!=(iterator const& other) noexcept { bool operator!=(iterator const& other) const noexcept {
return i != other.i; return i != other.i;
} }
expr operator*() const { return e.arg(i); } expr operator*() const { return e.arg(i); }
@ -1703,28 +1703,28 @@ namespace z3 {
inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; } 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); check_context(a, b);
Z3_ast r = Z3_mk_eq(a.ctx(), a, b); Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
a.check_error(); a.check_error();
return expr(a.ctx(), r); 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==(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==(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) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == 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); check_context(a, b);
Z3_ast args[2] = { a, b }; Z3_ast args[2] = { a, b };
Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args); Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
a.check_error(); a.check_error();
return expr(a.ctx(), r); 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!=(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) { assert(a.is_fpa()); return a != a.ctx().fpa_val(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) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != 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) {
check_context(a, b); check_context(a, b);
@ -2957,10 +2957,10 @@ namespace z3 {
expr_vector const * operator->() const { return &(operator*()); } expr_vector const * operator->() const { return &(operator*()); }
expr_vector const& operator*() const noexcept { return m_cube; } 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; 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; return other.m_end != m_end;
}; };

16
src/muz/rel/dl_base.h
View file

@ -1113,7 +1113,7 @@ namespace datalog {
virtual row_interface & operator*() = 0; virtual row_interface & operator*() = 0;
virtual void 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 //we worry about the equality operator only because of checking
//the equality with the end() iterator //the equality with the end() iterator
return is_finished() && it.is_finished(); return is_finished() && it.is_finished();
@ -1142,7 +1142,7 @@ namespace datalog {
virtual table_element operator*() = 0; virtual table_element operator*() = 0;
virtual void 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 //we worry about the equality operator only because of checking
//the equality with the end() iterator //the equality with the end() iterator
return is_finished() && it.is_finished(); return is_finished() && it.is_finished();
@ -1169,10 +1169,8 @@ namespace datalog {
{ return &(*(*m_core)); } { return &(*(*m_core)); }
iterator & operator++() iterator & operator++()
{ ++(*m_core); return *this; } { ++(*m_core); return *this; }
bool operator==(const iterator & it) bool operator==(const iterator & it) const { return (*m_core)==(*it.m_core); }
{ return (*m_core)==(*it.m_core); } bool operator!=(const iterator & it) const { return !operator==(it); }
bool operator!=(const iterator & it)
{ return !operator==(it); }
}; };
class row_iterator { class row_iterator {
@ -1187,10 +1185,8 @@ namespace datalog {
{ return *(*m_core); } { return *(*m_core); }
row_iterator & operator++() row_iterator & operator++()
{ ++(*m_core); return *this; } { ++(*m_core); return *this; }
bool operator==(const row_iterator & it) bool operator==(const row_iterator & it) const { return (*m_core)==(*it.m_core); }
{ return (*m_core)==(*it.m_core); } bool operator!=(const row_iterator & it) const { return !operator==(it); }
bool operator!=(const row_iterator & it)
{ return !operator==(it); }
}; };
virtual iterator begin() const = 0; virtual iterator begin() const = 0;

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -179,8 +179,6 @@ public:
void initialize_values() { void initialize_values() {
if (m_mcs.back()) if (m_mcs.back())
m_mcs.back()->convert_initialize_value(m_var2value); m_mcs.back()->convert_initialize_value(m_var2value);
if (m_mcs.back())
m_mcs.back()->display(verbose_stream());
for (auto & [var, value] : m_var2value) { for (auto & [var, value] : m_var2value) {
sat::bool_var b = m_map.to_bool_var(var); sat::bool_var b = m_map.to_bool_var(var);

1
src/sat/tactic/sat_tactic.cpp
View file

@ -265,7 +265,6 @@ public:
} }
void user_propagate_initialize_value(expr* var, expr* value) override { 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) }); m_var2value.push_back({ expr_ref(var, m), expr_ref(value, m) });
} }