21 using System.Runtime.InteropServices;
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");
expr operator!=(expr const &a, expr const &b)
override bool Equals(object o)
Object comparison.
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
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
expr operator==(expr const &a, expr const &b)
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.