21using System.Diagnostics;
22using System.Runtime.InteropServices;
65 throw new Z3Exception(
"Unknown symbol kind encountered");
75 return Object.ReferenceEquals(s1, s2) ||
76 (!Object.ReferenceEquals(s1,
null) &&
77 !Object.ReferenceEquals(s2,
null) &&
78 s1.NativeObject == s2.NativeObject);
92 public override bool Equals(
object o)
95 if (casted ==
null)
return false;
96 return this == casted;
118 Debug.Assert(ctx !=
null);
123 Debug.Assert(ctx !=
null);
130 throw new Z3Exception(
"Unknown symbol kind encountered");
The main interaction with Z3 happens via the Context.
Symbols are used to name several term and type constructors.
override bool Equals(object o)
Object comparison.
static bool operator==(Symbol s1, Symbol s2)
Equality overloading.
static bool operator!=(Symbol s1, Symbol s2)
Equality overloading.
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
override int GetHashCode()
The Symbols's hash code.
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Z3_symbol_kind Kind
The kind of the symbol (int or string)
override string ToString()
A string representation of the symbol.
Symbol(Context ctx, IntPtr obj)
Symbol constructor
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...