Z3
StringSymbol.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class StringSymbol extends Symbol
26 {
32  public String getString()
33  {
34  return Native.getSymbolString(getContext().nCtx(), getNativeObject());
35  }
36 
37  StringSymbol(Context ctx, long obj)
38  {
39  super(ctx, obj);
40  }
41 
42  StringSymbol(Context ctx, String s)
43  {
44  super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
45  }
46 
47  @Override
48  void checkNativeObject(long obj)
49  {
50  if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
51  .toInt()) {
52  throw new Z3Exception("Symbol is not of String kind");
53  }
54  super.checkNativeObject(obj);
55  }
56 }
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.StringSymbol
Definition: StringSymbol.java:25
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.getSymbolString
static String getSymbolString(long a0, long a1)
Definition: Native.java:2650
Z3_symbol_kind
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:113
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition: Z3_symbol_kind.java:13
com
com.microsoft.z3.StringSymbol.getString
String getString()
Definition: StringSymbol.java:32
com.microsoft.z3.Context
Definition: Context.java:35
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111