From a82b5e21fe98817604f6bda5dfd016fde972c05a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 06:11:36 +0100 Subject: [PATCH] add regular expression operations to C and C++ API Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 36 +++++++++++++++++++++++-------- src/api/c++/z3++.h | 48 +++++++++++++++++++++++++++++++++++------ src/api/z3_api.h | 52 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 121 insertions(+), 15 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 0fde6303a..e80d98553 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -116,15 +116,18 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) { - Z3_TRY; - LOG_Z3_mk_seq_empty(c, seq); - RESET_ERROR_CODE(); - app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq)); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - Z3_CATCH_RETURN(0); - } +#define MK_SORTED(NAME, FN ) \ + Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) { \ + Z3_TRY; \ + LOG_ ## NAME(c, s); \ + RESET_ERROR_CODE(); \ + app* a = FN(to_sort(s)); \ + mk_c(c)->save_ast_trail(a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(0); \ + } + + MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty); MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP); MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP); @@ -139,13 +142,28 @@ extern "C" { MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP); MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP); + Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { + Z3_TRY; + LOG_Z3_mk_re_loop(c, r, lo, hi); + RESET_ERROR_CODE(); + app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP); MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); + MK_UNARY(Z3_mk_re_complement, 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_intersect, 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); + MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty); + MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full); + + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 14702a4ea..f8c1c57dc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -934,9 +934,20 @@ namespace z3 { check_error(); return expr(ctx(), r); } - friend expr range(expr const& lo, expr const& hi); - - + friend expr range(expr const& lo, expr const& hi); + /** + \brief create a looping regular expression. + */ + expr loop(unsigned lo) { + Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0); + check_error(); + return expr(ctx(), r); + } + expr loop(unsigned lo, unsigned hi) { + Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi); + check_error(); + return expr(ctx(), r); + } /** @@ -1227,9 +1238,6 @@ 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); } - - /** @@ -2465,6 +2473,34 @@ namespace z3 { re.check_error(); return expr(re.ctx(), r); } + inline expr re_empty(sort const& s) { + Z3_ast r = Z3_mk_re_empty(s.ctx(), s); + s.check_error(); + return expr(s.ctx(), r); + } + inline expr re_full(sort const& s) { + Z3_ast r = Z3_mk_re_full(s.ctx(), s); + s.check_error(); + return expr(s.ctx(), r); + } + inline expr re_intersect(expr_vector const& args) { + assert(args.size() > 0); + context& ctx = args[0].ctx(); + array _args(args); + Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr()); + ctx.check_error(); + return expr(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); + } + + + + inline expr interpolant(expr const& a) { return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a)); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d8570b852..356f933d4 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1154,6 +1154,12 @@ typedef enum { Z3_OP_RE_OPTION, Z3_OP_RE_CONCAT, Z3_OP_RE_UNION, + Z3_OP_RE_RANGE, + Z3_OP_RE_LOOP, + Z3_OP_RE_INTERSECT, + Z3_OP_RE_EMPTY_SET, + Z3_OP_RE_FULL_SET, + Z3_OP_RE_COMPLEMENT, // Auxiliary Z3_OP_LABEL = 0x700, @@ -3375,6 +3381,52 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); + /** + \brief Create a regular expression loop. The supplied regular expression \c r is repated + between \c lo and \c hi times. The \c lo should be below \c hi with one exection: when + supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least + \c lo number of times, and with an unbounded upper bound. + + def_API('Z3_mk_re_loop', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in(UINT))) + */ + Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi); + + /** + \brief Create the intersection of the regular languages. + + \pre n > 0 + + def_API('Z3_mk_re_intersect' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + */ + Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Create the complement of the regular language \c re. + + def_API('Z3_mk_re_complement' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re); + + /** + \brief Create an empty regular expression of sort \c re. + + \pre re is a regular expression sort. + + def_API('Z3_mk_re_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re); + + + /** + \brief Create an universal regular expression of sort \c re. + + \pre re is a regular expression sort. + + def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); + + /*@}*/