Z3 |

ASTMap.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 ASTMap.cs
7
8 Abstract:
9
10 Z3 Managed API: AST Maps
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16 Notes:
17
18--*/
19
20 using System.Diagnostics;
21 using System;
22
23 namespace Microsoft.Z3
24{
28 internal class ASTMap : Z3Object
29 {
35 public bool Contains(AST k)
36 {
37 Debug.Assert(k != null);
38
39 return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject);
40 }
41
49 public AST Find(AST k)
50 {
51 Debug.Assert(k != null);
52
53 return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject));
54 }
55
61 public void Insert(AST k, AST v)
62 {
63 Debug.Assert(k != null);
64 Debug.Assert(v != null);
65
66 Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
67 }
68
73 public void Erase(AST k)
74 {
75 Debug.Assert(k != null);
76
77 Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject);
78 }
79
83 public void Reset()
84 {
85 Native.Z3_ast_map_reset(Context.nCtx, NativeObject);
86 }
87
91 public uint Size
92 {
93 get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); }
94 }
95
99 public AST[] Keys
100 {
101 get
102 {
103 ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
104 return res.ToArray();
105 }
106 }
107
111 public override string ToString()
112 {
113 return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
114 }
115
116 #region Internal
117 internal ASTMap(Context ctx, IntPtr obj)
118 : base(ctx, obj)
119 {
120 Debug.Assert(ctx != null);
121 }
122 internal ASTMap(Context ctx)
123 : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx))
124 {
125 Debug.Assert(ctx != null);
126 }
127
128 internal class DecRefQueue : IDecRefQueue
129 {
130 public DecRefQueue() : base() { }
131 public DecRefQueue(uint move_limit) : base(move_limit) { }
132 internal override void IncRef(Context ctx, IntPtr obj)
133 {
134 Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
135 }
136
137 internal override void DecRef(Context ctx, IntPtr obj)
138 {
139 Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
140 }
141 };
142
143 internal override void IncRef(IntPtr o)
144 {
145 Context.ASTMap_DRQ.IncAndClear(Context, o);
146 base.IncRef(o);
147 }
148
149 internal override void DecRef(IntPtr o)
150 {
151 Context.ASTMap_DRQ.Add(o);
152 base.DecRef(o);
153 }
154 #endregion
155 }
156}
Microsoft.Z3.Context.ASTMap_DRQ
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
Definition: Context.cs:4730
Microsoft.Z3
Definition: AlgebraicNum.cs:27
z3py.Contains
def Contains(a, b)
Definition: z3py.py:10789
Z3_mk_ast_map
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c)
Return an empty mapping from AST to AST.