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

Remove unnecessary const qualifiers from comparison operator overloads in z3++.h

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-23 13:38:07 +01:00
parent ee347735be
commit 5c583299f1
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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) const {
inline expr operator==(expr const & a, expr const & b) {
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) const { 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) { 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) 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, 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, expr const & b) const {
inline expr operator!=(expr const & a, expr const & b) {
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) 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, 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, expr const & b) {
check_context(a, b);