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.Runtime.InteropServices;
23 
24 namespace Microsoft.Z3
25 {
29  [ContractVerification(true)]
30  public class Symbol : Z3Object
31  {
35  protected Z3_symbol_kind Kind
36  {
37  get { return (Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, NativeObject); }
38  }
39 
43  public bool IsIntSymbol()
44  {
45  return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
46  }
47 
51  public bool IsStringSymbol()
52  {
53  return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
54  }
55 
59  public override string ToString()
60  {
61  if (IsIntSymbol())
62  return ((IntSymbol)this).Int.ToString();
63  else if (IsStringSymbol())
64  return ((StringSymbol)this).String;
65  else
66  throw new Z3Exception("Unknown symbol kind encountered");
67  }
68 
69 
73  public static bool operator ==(Symbol s1, Symbol s2)
74  {
75 
76  return Object.ReferenceEquals(s1, s2) ||
77  (!Object.ReferenceEquals(s1, null) &&
78  !Object.ReferenceEquals(s2, null) &&
79  s1.NativeObject == s2.NativeObject);
80  }
81 
85  public static bool operator !=(Symbol s1, Symbol s2)
86  {
87  return !(s1.NativeObject == s2.NativeObject);
88  }
89 
93  public override bool Equals(object o)
94  {
95  Symbol casted = o as Symbol;
96  if (casted == null) return false;
97  return this == casted;
98  }
99 
104  public override int GetHashCode()
105  {
106  return (int)NativeObject;
107  }
108 
109 
110  #region Internal
111  internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj)
115  {
116  Contract.Requires(ctx != null);
117  }
118 
119  internal static Symbol Create(Context ctx, IntPtr obj)
120  {
121  Contract.Requires(ctx != null);
122  Contract.Ensures(Contract.Result<Symbol>() != null);
123 
124  switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
125  {
126  case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
127  case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
128  default:
129  throw new Z3Exception("Unknown symbol kind encountered");
130  }
131  }
132  #endregion
133  }
134 }
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1024
override bool Equals(object o)
Object comparison.
Definition: Symbol.cs:93
override int GetHashCode()
The Symbols&#39;s hash code.
Definition: Symbol.cs:104
override string ToString()
A string representation of the symbol.
Definition: Symbol.cs:59
bool IsIntSymbol()
Indicates whether the symbol is of Int kind
Definition: Symbol.cs:43
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:119
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1015
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30
bool IsStringSymbol()
Indicates whether the symbol is of string kind.
Definition: Symbol.cs:51
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Numbered symbols
Definition: IntSymbol.cs:30