From a68d5131c7b91b841289f25044511f76f8232eaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 09:00:14 -0800 Subject: [PATCH] add bvsmod Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3d39cdb74..4b5e9d04e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1418,11 +1418,18 @@ namespace z3 { inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); } /** - \brief signed reminder operator for bitvectors + \brief signed remainder operator for bitvectors */ inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); } inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); } inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); } + + /** + \brief signed modulus operator for bitvectors + */ + inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); } + inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); } + inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned reminder operator for bitvectors