diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 6f296147e..596b2943f 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -98,11 +98,12 @@ namespace Microsoft.Z3 /// /// The keys stored in the map. /// - public ASTVector Keys + public AST[] Keys { 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(); } } diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index b70ff13b6..f858c7862 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -99,6 +99,30 @@ namespace Microsoft.Z3 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject); } + /// + /// Translates an AST vector into an AST[] + /// + 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; + } + + /// + /// Translates an AST vector into an Expr[] + /// + 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 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); }