mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add range constructor to .NET API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
feb801564b
commit
4e25bffab6
|
@ -2609,6 +2609,19 @@ namespace Microsoft.Z3
|
|||
CheckContextMatch<ReExpr>(t);
|
||||
return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Create a range expression.
|
||||
/// </summary>
|
||||
public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
|
||||
{
|
||||
Contract.Requires(lo != null);
|
||||
Contract.Requires(hi != null);
|
||||
Contract.Ensures(Contract.Result<ReExpr>() != null);
|
||||
CheckContextMatch(lo, hi);
|
||||
return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
|
||||
}
|
||||
|
||||
#endregion
|
||||
|
||||
|
|
Loading…
Reference in a new issue