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;
21 using System.Diagnostics.Contracts;
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 ASTVector Keys
102  {
103  get
104  {
105  return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
106  }
107  }
108 
112  public override string ToString()
113  {
114  return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
115  }
116 
117  #region Internal
118  internal ASTMap(Context ctx, IntPtr obj)
119  : base(ctx, obj)
120  {
121  Contract.Requires(ctx != null);
122  }
123  internal ASTMap(Context ctx)
124  : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx))
125  {
126  Contract.Requires(ctx != null);
127  }
128 
129  internal class DecRefQueue : IDecRefQueue
130  {
131  public override void IncRef(Context ctx, IntPtr obj)
132  {
133  Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
134  }
135 
136  public override void DecRef(Context ctx, IntPtr obj)
137  {
138  Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
139  }
140  };
141 
142  internal override void IncRef(IntPtr o)
143  {
144  Context.ASTMap_DRQ.IncAndClear(Context, o);
145  base.IncRef(o);
146  }
147 
148  internal override void DecRef(IntPtr o)
149  {
150  Context.ASTMap_DRQ.Add(o);
151  base.DecRef(o);
152  }
153  #endregion
154  }
155 }
Z3_ast_map Z3_API Z3_mk_ast_map(__in Z3_context c)
Return an empty mapping from AST to AST.