mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

add missing complement

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-09 06:21:57 +01:00
parent 0473d2ef56
commit 976fadf771
2 changed files with 20 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2448,30 +2448,19 @@ namespace z3 {
return expr(s.ctx(), r); return expr(s.ctx(), r);
} }
inline expr to_re(expr const& s) { inline expr to_re(expr const& s) {
Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s); MK_EXPR1(Z3_mk_seq_to_re, s);
s.check_error();
return expr(s.ctx(), r);
} }
inline expr in_re(expr const& s, expr const& re) { inline expr in_re(expr const& s, expr const& re) {
check_context(s, re); MK_EXPR2(Z3_mk_seq_in_re, s, re);
Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
s.check_error();
return expr(s.ctx(), r);
} }
inline expr plus(expr const& re) { inline expr plus(expr const& re) {
Z3_ast r = Z3_mk_re_plus(re.ctx(), re); MK_EXPR1(Z3_mk_re_plus, re);
re.check_error();
return expr(re.ctx(), r);
} }
inline expr option(expr const& re) { inline expr option(expr const& re) {
Z3_ast r = Z3_mk_re_option(re.ctx(), re); MK_EXPR1(Z3_mk_re_option, re);
re.check_error();
return expr(re.ctx(), r);
} }
inline expr star(expr const& re) { inline expr star(expr const& re) {
Z3_ast r = Z3_mk_re_star(re.ctx(), re); MK_EXPR1(Z3_mk_re_star, re);
re.check_error();
return expr(re.ctx(), r);
} }
inline expr re_empty(sort const& s) { inline expr re_empty(sort const& s) {
Z3_ast r = Z3_mk_re_empty(s.ctx(), s); Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
@ -2491,6 +2480,9 @@ namespace z3 {
ctx.check_error(); ctx.check_error();
return expr(ctx, r); return expr(ctx, r);
} }
inline expr re_complement(expr const& a) {
MK_EXPR1(Z3_mk_re_complement, a);
}
inline expr range(expr const& lo, expr const& hi) { inline expr range(expr const& lo, expr const& hi) {
check_context(lo, hi); check_context(lo, hi);
Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);

14
src/api/dotnet/Context.cs
View file

@ -2577,7 +2577,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Take the Kleene plus of a regular expression. /// Take the Kleene plus of a regular expression.
/// </summary> /// </summary>
public ReExpr MPlus(ReExpr re) public ReExpr MkPlus(ReExpr re)
{ {
Contract.Requires(re != null); Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null); Contract.Ensures(Contract.Result<ReExpr>() != null);
@ -2587,13 +2587,23 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create the optional regular expression. /// Create the optional regular expression.
/// </summary> /// </summary>
public ReExpr MOption(ReExpr re) public ReExpr MkOption(ReExpr re)
{ {
Contract.Requires(re != null); Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null); Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
} }
/// <summary>
/// Create the complement regular expression.
/// </summary>
public ReExpr MkComplement(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
}
/// <summary> /// <summary>
/// Create the concatenation of regular languages. /// Create the concatenation of regular languages.
/// </summary> /// </summary>