Z3
StringSymbol.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 StringSymbol.cs
7
8Abstract:
9
10 Z3 Managed API: String Symbols
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Runtime.InteropServices;
23
24namespace Microsoft.Z3
25{
26
30 public class StringSymbol : Symbol
31 {
36 public string String
37 {
38 get
39 {
40
41 if (!IsStringSymbol())
42 throw new Z3Exception("String requested from non-String symbol");
43 return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
44 }
45 }
46
47 #region Internal
48 internal StringSymbol(Context ctx, IntPtr obj)
49 : base(ctx, obj)
50 {
51 Debug.Assert(ctx != null);
52 }
53
54 internal StringSymbol(Context ctx, string s)
55 : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
56 {
57 Debug.Assert(ctx != null);
58 }
59
60#if DEBUG
61 internal override void CheckNativeObject(IntPtr obj)
62 {
63 if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
64 throw new Z3Exception("Symbol is not of string kind");
65
66 base.CheckNativeObject(obj);
67 }
68#endif
69 #endregion
70 }
71}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
string String
The string value of the symbol.
Definition: StringSymbol.cs:37
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition: Symbol.cs:50
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
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_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.