mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

add regular expression features to C# API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-09 06:17:13 +01:00
parent a82b5e21fe
commit 0473d2ef56
1 changed files with 43 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2564,6 +2564,16 @@ namespace Microsoft.Z3
return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
}
/// <summary>
/// Take the bounded Kleene star of a regular expression.
/// </summary>
public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
}
/// <summary>
/// Take the Kleene plus of a regular expression.
/// </summary>
@ -2610,6 +2620,39 @@ namespace Microsoft.Z3
return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create the intersection of regular languages.
/// </summary>
public ReExpr MkIntersect(params ReExpr[] t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ReExpr>() != null);
CheckContextMatch<ReExpr>(t);
return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create the empty regular expression.
/// </summary>
public ReExpr MkEmptyRe(Sort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
}
/// <summary>
/// Create the full regular expression.
/// </summary>
public ReExpr MkFullRe(Sort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
}
/// <summary>
/// Create a range expression.