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.Diagnostics;
22 using System.Runtime.InteropServices;
23
24 namespace Microsoft.Z3
25{
29 public class IntSymbol : Symbol
30 {
35 public int Int
36 {
37 get
38 {
39 if (!IsIntSymbol())
40 throw new Z3Exception("Int requested from non-Int symbol");
41 return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
42 }
43 }
44
45 #region Internal
46 internal IntSymbol(Context ctx, IntPtr obj)
47 : base(ctx, obj)
48 {
49 Debug.Assert(ctx != null);
50 }
51 internal IntSymbol(Context ctx, int i)
52 : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
53 {
54 Debug.Assert(ctx != null);
55 }
56
57#if DEBUG
58 internal override void CheckNativeObject(IntPtr obj)
59 {
60 if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
61 throw new Z3Exception("Symbol is not of integer kind");
62 base.CheckNativeObject(obj);
63 }
64#endif
65 #endregion
66 }
67}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.IntSymbol
Numbered symbols
Definition: IntSymbol.cs:30
Microsoft.Z3.IntSymbol.Int
int Int
The int value of the symbol.
Definition: IntSymbol.cs:36
Microsoft.Z3.Symbol
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Microsoft.Z3.Symbol.IsIntSymbol
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition: Symbol.cs:42
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3
Definition: AlgebraicNum.cs:27
Z3_symbol_kind
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:116
Z3_mk_int_symbol
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.