mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

add regular expression operations to C and C++ API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-09 06:11:36 +01:00
parent 4e25bffab6
commit a82b5e21fe
3 changed files with 121 additions and 15 deletions

36
src/api/api_seq.cpp
View file

@ -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);
};

48
src/api/c++/z3++.h
View file

@ -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<Z3_ast> _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));

52
src/api/z3_api.h
View file

@ -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);
/*@}*/