Z3
src/api/dotnet/ASTMap.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     ASTMap.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: AST Maps
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines