mirror of
https://github.com/Z3Prover/z3
synced 2025-06-20 12:53:38 +00:00
Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality.
Fixes #103
This commit is contained in:
parent
a361e4dcef
commit
e33ff42766
2 changed files with 27 additions and 2 deletions
|
@ -98,11 +98,12 @@ namespace Microsoft.Z3
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// The keys stored in the map.
|
/// The keys stored in the map.
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public ASTVector Keys
|
public AST[] Keys
|
||||||
{
|
{
|
||||||
get
|
get
|
||||||
{
|
{
|
||||||
return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
|
ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
|
||||||
|
return res.ToArray();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -99,6 +99,30 @@ namespace Microsoft.Z3
|
||||||
return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
|
return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// <summary>
|
||||||
|
/// Translates an AST vector into an AST[]
|
||||||
|
/// </summary>
|
||||||
|
public AST[] ToArray()
|
||||||
|
{
|
||||||
|
uint n = Size;
|
||||||
|
AST[] res = new AST[n];
|
||||||
|
for (uint i = 0; i < n; i++)
|
||||||
|
res[i] = AST.Create(this.Context, this[i].NativeObject);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
/// <summary>
|
||||||
|
/// Translates an AST vector into an Expr[]
|
||||||
|
/// </summary>
|
||||||
|
public Expr[] ToExprArray()
|
||||||
|
{
|
||||||
|
uint n = Size;
|
||||||
|
Expr[] res = new Expr[n];
|
||||||
|
for (uint i = 0; i < n; i++)
|
||||||
|
res[i] = Expr.Create(this.Context, this[i].NativeObject);
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
#region Internal
|
#region Internal
|
||||||
internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
|
internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
|
||||||
internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
|
internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue