From 26af694d2c9e3e1ef7a6e605c025626c7a751f4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Dec 2020 14:04:01 -0800 Subject: [PATCH] add overloads to != and == based on #4906 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index bb3c977fc..8b175a15c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1469,6 +1469,8 @@ namespace z3 { } 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); @@ -1479,6 +1481,8 @@ namespace z3 { } 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);