diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index b32965c07..f3335d80f 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2159,6 +2159,7 @@ namespace test_mapi Console.Write("Z3 Full Version: "); Console.WriteLine(Microsoft.Z3.Version.ToString()); + SimpleExample(); // These examples need model generation turned on. diff --git a/src/api/dotnet/Symbol.cs b/src/api/dotnet/Symbol.cs index 783647d3f..2a1fdf6c5 100644 --- a/src/api/dotnet/Symbol.cs +++ b/src/api/dotnet/Symbol.cs @@ -66,6 +66,47 @@ namespace Microsoft.Z3 throw new Z3Exception("Unknown symbol kind encountered"); } + + /// + /// Equality overloading. + /// + public static bool operator ==(Symbol s1, Symbol s2) + { + + return Object.ReferenceEquals(s1, s2) || + (!Object.ReferenceEquals(s1, null) && + !Object.ReferenceEquals(s2, null) && + s1.NativeObject == s2.NativeObject); + } + + /// + /// Equality overloading. + /// + public static bool operator !=(Symbol s1, Symbol s2) + { + return !(s1.NativeObject == s2.NativeObject); + } + + /// + /// Object comparison. + /// + public override bool Equals(object o) + { + Symbol casted = o as Symbol; + if (casted == null) return false; + return this == casted; + } + + /// + /// The Symbols's hash code. + /// + /// A hash code + public override int GetHashCode() + { + return (int)NativeObject; + } + + #region Internal /// /// Symbol constructor