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;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  internal class ASTMap : Z3Object
30  {
36  public bool Contains(AST k)
37  {
38  Contract.Requires(k != null);
39 
40  return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
41  }
42 
50  public AST Find(AST k)
51  {
52  Contract.Requires(k != null);
53  Contract.Ensures(Contract.Result<AST>() != null);
54 
55  return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject));
56  }
57 
63  public void Insert(AST k, AST v)
64  {
65  Contract.Requires(k != null);
66  Contract.Requires(v != null);
67 
68  Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
69  }
70 
75  public void Erase(AST k)
76  {
77  Contract.Requires(k != null);
78 
79  Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject);
80  }
81 
85  public void Reset()
86  {
87  Native.Z3_ast_map_reset(Context.nCtx, NativeObject);
88  }
89 
93  public uint Size
94  {
95  get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); }
96  }
97 
101  public AST[] Keys
102  {
103  get
104  {
105  ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
106  return res.ToArray();
107  }
108  }
109 
113  public override string ToString()
114  {
115  return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
116  }
117 
118  #region Internal
119  internal ASTMap(Context ctx, IntPtr obj)
120  : base(ctx, obj)
121  {
122  Contract.Requires(ctx != null);
123  }
124  internal ASTMap(Context ctx)
125  : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx))
126  {
127  Contract.Requires(ctx != null);
128  }
129 
130  internal class DecRefQueue : IDecRefQueue
131  {
132  public DecRefQueue() : base() { }
133  public DecRefQueue(uint move_limit) : base(move_limit) { }
134  internal override void IncRef(Context ctx, IntPtr obj)
135  {
136  Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
137  }
138 
139  internal override void DecRef(Context ctx, IntPtr obj)
140  {
141  Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
142  }
143  };
144 
145  internal override void IncRef(IntPtr o)
146  {
147  Context.ASTMap_DRQ.IncAndClear(Context, o);
148  base.IncRef(o);
149  }
150 
151  internal override void DecRef(IntPtr o)
152  {
153  Context.ASTMap_DRQ.Add(o);
154  base.DecRef(o);
155  }
156  #endregion
157  }
158 }
def Contains(a, b)
Definition: z3py.py:9504