Z3
IntSymbol.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  IntSymbol.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Int Symbols
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-11-23
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
23 
24 namespace Microsoft.Z3
25 {
29  [ContractVerification(true)]
30  public class IntSymbol : Symbol
31  {
36  public int Int
37  {
38  get
39  {
40  if (!IsIntSymbol())
41  throw new Z3Exception("Int requested from non-Int symbol");
42  return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
43  }
44  }
45 
46  #region Internal
47  internal IntSymbol(Context ctx, IntPtr obj)
48  : base(ctx, obj)
49  {
50  Contract.Requires(ctx != null);
51  }
52  internal IntSymbol(Context ctx, int i)
53  : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
54  {
55  Contract.Requires(ctx != null);
56  }
57 
58 #if DEBUG
59  internal override void CheckNativeObject(IntPtr obj)
60  {
61  if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
62  throw new Z3Exception("Symbol is not of integer kind");
63  base.CheckNativeObject(obj);
64  }
65 #endif
66  #endregion
67  }
68 }
using System
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
Definition: Native.cs:3174
def Int(name, ctx=None)
Definition: z3py.py:2742
static IntPtr Z3_mk_int_symbol(Z3_context a0, int a1)
Definition: Native.cs:2138
static int Z3_get_symbol_int(Z3_context a0, IntPtr a1)
Definition: Native.cs:3182
Z3_symbol_kind
Z3_symbol_kind
Definition: Enumerations.cs:17
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Numbered symbols
Definition: IntSymbol.cs:30