21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
29 internal class ASTMap : Z3Object
36 public bool Contains(AST k)
38 Contract.Requires(k != null);
40 return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
50 public AST Find(AST k)
52 Contract.Requires(k != null);
53 Contract.Ensures(Contract.Result<AST>() != null);
55 return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject));
63 public void Insert(AST k, AST v)
65 Contract.Requires(k != null);
66 Contract.Requires(v != null);
68 Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
75 public void Erase(AST k)
77 Contract.Requires(k != null);
79 Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject);
87 Native.Z3_ast_map_reset(Context.nCtx, NativeObject);
95 get {
return Native.Z3_ast_map_size(Context.nCtx, NativeObject); }
101 public ASTVector Keys
105 return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
112 public override string ToString()
114 return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
118 internal ASTMap(Context ctx, IntPtr obj)
121 Contract.Requires(ctx != null);
123 internal ASTMap(Context ctx)
126 Contract.Requires(ctx != null);
131 public override void IncRef(Context ctx, IntPtr obj)
133 Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
136 public override void DecRef(Context ctx, IntPtr obj)
138 Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
142 internal override void IncRef(IntPtr o)
144 Context.ASTMap_DRQ.IncAndClear(Context, o);
148 internal override void DecRef(IntPtr o)
150 Context.ASTMap_DRQ.Add(o);
Z3_ast_map Z3_API Z3_mk_ast_map(__in Z3_context c)
Return an empty mapping from AST to AST.