Z3 |

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.Diagnostics;
22 using System.Runtime.InteropServices;
23
24 namespace Microsoft.Z3
25{
29 public class Symbol : Z3Object
30 {
34 protected Z3_symbol_kind Kind
35 {
36 get { return (Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, NativeObject); }
37 }
38
42 public bool IsIntSymbol()
43 {
44 return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
45 }
46
50 public bool IsStringSymbol()
51 {
52 return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
53 }
54
58 public override string ToString()
59 {
60 if (IsIntSymbol())
61 return ((IntSymbol)this).Int.ToString();
62 else if (IsStringSymbol())
63 return ((StringSymbol)this).String;
64 else
65 throw new Z3Exception("Unknown symbol kind encountered");
66 }
67
68
72 public static bool operator ==(Symbol s1, Symbol s2)
73 {
74
75 return Object.ReferenceEquals(s1, s2) ||
76 (!Object.ReferenceEquals(s1, null) &&
77 !Object.ReferenceEquals(s2, null) &&
78 s1.NativeObject == s2.NativeObject);
79 }
80
84 public static bool operator !=(Symbol s1, Symbol s2)
85 {
86 return !(s1 == s2);
87 }
88
92 public override bool Equals(object o)
93 {
94 Symbol casted = o as Symbol;
95 if (casted == null) return false;
96 return this == casted;
97 }
98
103 public override int GetHashCode()
104 {
105 if (IsIntSymbol())
106 return ((IntSymbol)this).Int;
107 else
108 return ((StringSymbol)this).String.GetHashCode();
109 }
110
111
112 #region Internal
116 internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj)
117 {
118 Debug.Assert(ctx != null);
119 }
120
121 internal static Symbol Create(Context ctx, IntPtr obj)
122 {
123 Debug.Assert(ctx != null);
124
125 switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
126 {
127 case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
128 case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
129 default:
130 throw new Z3Exception("Unknown symbol kind encountered");
131 }
132 }
133 #endregion
134 }
135}
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.StringSymbol
Named symbols
Definition: StringSymbol.cs:31
Microsoft.Z3.Symbol
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Microsoft.Z3.Symbol.Equals
override bool Equals(object o)
Object comparison.
Definition: Symbol.cs:92
Microsoft.Z3.Symbol.operator==
static bool operator==(Symbol s1, Symbol s2)
Equality overloading.
Definition: Symbol.cs:72
Microsoft.Z3.Symbol.operator!=
static bool operator!=(Symbol s1, Symbol s2)
Equality overloading.
Definition: Symbol.cs:84
Microsoft.Z3.Symbol.IsStringSymbol
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition: Symbol.cs:50
Microsoft.Z3.Symbol.GetHashCode
override int GetHashCode()
The Symbols's hash code.
Definition: Symbol.cs:103
Microsoft.Z3.Symbol.IsIntSymbol
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition: Symbol.cs:42
Microsoft.Z3.Symbol.Kind
Z3_symbol_kind Kind
The kind of the symbol (int or string)
Definition: Symbol.cs:35
Microsoft.Z3.Symbol.ToString
override string ToString()
A string representation of the symbol.
Definition: Symbol.cs:58
Microsoft.Z3.Symbol.Symbol
Symbol(Context ctx, IntPtr obj)
Symbol constructor
Definition: Symbol.cs:116
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
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