From feb801564ba6a9a72259f60f854081333e3eda44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2016 18:28:27 +0100 Subject: [PATCH] adding range to C API. Issue #831 Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 2 +- src/api/c++/z3++.h | 4 ++++ src/api/z3_api.h | 8 ++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 5704ffdb0..0fde6303a 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -145,7 +145,7 @@ extern "C" { MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP); - + MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP); }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 2a9c771a1..14702a4ea 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -934,6 +934,8 @@ namespace z3 { check_error(); return expr(ctx(), r); } + friend expr range(expr const& lo, expr const& hi); + @@ -1225,6 +1227,8 @@ namespace z3 { inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); } + inline expr range(expr const& lo, expr const& hi) { check_context(lo, hi); Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); lo.check_error(); return expr(lo.ctx(), r); } + diff --git a/src/api/z3_api.h b/src/api/z3_api.h index c7749ebef..d8570b852 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3367,6 +3367,14 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Create the range regular expression over two sequences of length 1. + + def_API('Z3_mk_re_range' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); + /*@}*/