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;
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 }
def Int(name, ctx=None)
Definition: z3py.py:2808
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
Definition: z3_api.h:119
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Numbered symbols
Definition: IntSymbol.cs:30