Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 internal class ASTMap : Z3Object
00030 {
00036 public bool Contains(AST k)
00037 {
00038 Contract.Requires(k != null);
00039
00040 return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
00041 }
00042
00050 public AST Find(AST k)
00051 {
00052 Contract.Requires(k != null);
00053 Contract.Ensures(Contract.Result<AST>() != null);
00054
00055 return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject));
00056 }
00057
00063 public void Insert(AST k, AST v)
00064 {
00065 Contract.Requires(k != null);
00066 Contract.Requires(v != null);
00067
00068 Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
00069 }
00070
00075 public void Erase(AST k)
00076 {
00077 Contract.Requires(k != null);
00078
00079 Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject);
00080 }
00081
00085 public void Reset()
00086 {
00087 Native.Z3_ast_map_reset(Context.nCtx, NativeObject);
00088 }
00089
00093 public uint Size
00094 {
00095 get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); }
00096 }
00097
00101 public ASTVector Keys
00102 {
00103 get
00104 {
00105 return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
00106 }
00107 }
00108
00112 public override string ToString()
00113 {
00114 return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
00115 }
00116
00117 #region Internal
00118 internal ASTMap(Context ctx, IntPtr obj)
00119 : base(ctx, obj)
00120 {
00121 Contract.Requires(ctx != null);
00122 }
00123 internal ASTMap(Context ctx)
00124 : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx))
00125 {
00126 Contract.Requires(ctx != null);
00127 }
00128
00129 internal class DecRefQueue : IDecRefQueue
00130 {
00131 public override void IncRef(Context ctx, IntPtr obj)
00132 {
00133 Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
00134 }
00135
00136 public override void DecRef(Context ctx, IntPtr obj)
00137 {
00138 Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
00139 }
00140 };
00141
00142 internal override void IncRef(IntPtr o)
00143 {
00144 Context.ASTMap_DRQ.IncAndClear(Context, o);
00145 base.IncRef(o);
00146 }
00147
00148 internal override void DecRef(IntPtr o)
00149 {
00150 Context.ASTMap_DRQ.Add(o);
00151 base.DecRef(o);
00152 }
00153 #endregion
00154 }
00155 }