21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
29 [ContractVerification(
true)]
63 else if (IsStringSymbol())
66 throw new Z3Exception(
"Unknown symbol kind encountered");
76 return Object.ReferenceEquals(s1, s2) ||
77 (!Object.ReferenceEquals(s1, null) &&
78 !Object.ReferenceEquals(s2, null) &&
79 s1.NativeObject == s2.NativeObject);
87 return !(s1.NativeObject == s2.NativeObject);
93 public override bool Equals(
object o)
96 if (casted == null)
return false;
97 return this == casted;
106 return (
int)NativeObject;
111 internal protected Symbol(
Context ctx, IntPtr obj) : base(ctx, obj)
116 Contract.Requires(ctx != null);
121 Contract.Requires(ctx != null);
122 Contract.Ensures(Contract.Result<
Symbol>() != null);
129 throw new Z3Exception(
"Unknown symbol kind encountered");
override bool Equals(object o)
Object comparison.
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
override int GetHashCode()
The Symbols's hash code.
override string ToString()
A string representation of the symbol.
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Z3_symbol_kind
Z3_symbol_kind
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.