Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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;
22 using System.Diagnostics.Contracts;
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  #region Internal
70  internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj)
74  {
75  Contract.Requires(ctx != null);
76  }
77 
78  internal static Symbol Create(Context ctx, IntPtr obj)
79  {
80  Contract.Requires(ctx != null);
81  Contract.Ensures(Contract.Result<Symbol>() != null);
82 
83  switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
84  {
85  case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
86  case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
87  default:
88  throw new Z3Exception("Unknown symbol kind encountered");
89  }
90  }
91  #endregion
92  }
93 }
static uint Z3_get_symbol_kind(Z3_context a0, IntPtr a1)
Definition: Native.cs:2894
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:150
Z3_symbol_kind
Z3_symbol_kind
Definition: Enumerations.cs:17
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
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:31
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30