Z3
src
api
dotnet
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.
Generated on Sat Jun 4 2022 07:10:05 for Z3 by
1.9.3