Z3
StringSymbol.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  StringSymbol.cs
7 
8 Abstract:
9 
10  Z3 Managed API: String Symbols
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-11-23
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Runtime.InteropServices;
23 
24 namespace Microsoft.Z3
25 {
26 
30  [ContractVerification(true)]
31  public class StringSymbol : Symbol
32  {
37  public string String
38  {
39  get
40  {
41  Contract.Ensures(Contract.Result<string>() != null);
42 
43  if (!IsStringSymbol())
44  throw new Z3Exception("String requested from non-String symbol");
45  return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
46  }
47  }
48 
49  #region Internal
50  internal StringSymbol(Context ctx, IntPtr obj)
51  : base(ctx, obj)
52  {
53  Contract.Requires(ctx != null);
54  }
55 
56  internal StringSymbol(Context ctx, string s)
57  : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
58  {
59  Contract.Requires(ctx != null);
60  }
61 
62 #if DEBUG
63  internal override void CheckNativeObject(IntPtr obj)
64  {
65  if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
66  throw new Z3Exception("Symbol is not of string kind");
67 
68  base.CheckNativeObject(obj);
69  }
70 #endif
71  #endregion
72  }
73 }
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
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
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
def String(name, ctx=None)
Definition: z3py.py:9443