From 542878dea3fd3d89d9ef8a1664925431b512e1b1 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Mon, 19 Apr 2021 08:53:43 -0700 Subject: [PATCH] Add sge and sgt to API; now has sge,sgt,sle,slt, and unsigned counterparts (#5194) --- src/api/c++/z3++.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5386c4fe6..aecffc31d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1824,6 +1824,18 @@ namespace z3 { inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); } inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); } inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); } + /** + \brief signed greater than or equal to operator for bitvectors. + */ + inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); } + inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); } + inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); } + /** + \brief signed greater than operator for bitvectors. + */ + inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); } + inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); } + inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); } /**