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 
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 }
static String getSymbolString(long a0, long a1)
Definition: Native.java:2303
static long mkStringSymbol(long a0, String a1)
Definition: Native.java:876
static int getSymbolKind(long a0, long a1)
Definition: Native.java:2285
def String(name, ctx=None)
Definition: z3py.py:9443