Z3
src
api
dotnet
Symbol.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2012 Microsoft Corporation
3
4
Module Name:
5
6
Symbol.cs
7
8
Abstract:
9
10
Z3 Managed API: Symbols
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2012-03-16
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
Symbol
:
Z3Object
31
{
35
protected
Z3_symbol_kind
Kind
36
{
37
get
{
return
(
Z3_symbol_kind
)
Native
.
Z3_get_symbol_kind
(
Context
.nCtx, NativeObject); }
38
}
39
43
public
bool
IsIntSymbol
()
44
{
45
return
Kind ==
Z3_symbol_kind
.Z3_INT_SYMBOL;
46
}
47
51
public
bool
IsStringSymbol
()
52
{
53
return
Kind ==
Z3_symbol_kind
.Z3_STRING_SYMBOL;
54
}
55
59
public
override
string
ToString
()
60
{
61
if
(IsIntSymbol())
62
return
((
IntSymbol
)
this
).Int.ToString();
63
else
if
(IsStringSymbol())
64
return
((
StringSymbol
)
this
).String;
65
else
66
throw
new
Z3Exception
(
"Unknown symbol kind encountered"
);
67
}
68
69
#region Internal
70
internal
protected
Symbol
(
Context
ctx, IntPtr obj) : base(ctx, obj)
74
{
75
Contract.Requires(ctx != null);
76
}
77
78
internal
static
Symbol Create(Context ctx, IntPtr obj)
79
{
80
Contract.Requires(ctx != null);
81
Contract.Ensures(Contract.Result<Symbol>() != null);
82
83
switch
((
Z3_symbol_kind
)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
84
{
85
case
Z3_symbol_kind
.Z3_INT_SYMBOL:
return
new
IntSymbol(ctx, obj);
86
case
Z3_symbol_kind
.Z3_STRING_SYMBOL:
return
new
StringSymbol(ctx, obj);
87
default
:
88
throw
new
Z3Exception(
"Unknown symbol kind encountered"
);
89
}
90
}
91
#endregion
92
}
93
}
Microsoft.Z3.Native
Definition:
Native.cs:39
System
Microsoft.Z3.Native.Z3_get_symbol_kind
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
Definition:
Native.cs:3101
Microsoft
Microsoft.Z3.Symbol.ToString
override string ToString()
A string representation of the symbol.
Definition:
Symbol.cs:59
Microsoft.Z3.Symbol.IsIntSymbol
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition:
Symbol.cs:43
Microsoft.Z3.StringSymbol
Named symbols
Definition:
StringSymbol.cs:31
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:150
Microsoft.Z3.Z3_symbol_kind
Z3_symbol_kind
Z3_symbol_kind
Definition:
Enumerations.cs:17
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:31
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition:
Z3Exception.cs:27
Microsoft.Z3.Symbol.IsStringSymbol
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition:
Symbol.cs:51
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition:
Z3Object.cs:31
Microsoft.Z3.Symbol
Symbols are used to name several term and type constructors.
Definition:
Symbol.cs:30
Microsoft.Z3.IntSymbol
Numbered symbols
Definition:
IntSymbol.cs:30
Generated on Thu Jun 25 2015 08:00:56 for Z3 by
1.8.9.1