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 {
31  public String getString() throws Z3Exception
32  {
33  return Native.getSymbolString(getContext().nCtx(), getNativeObject());
34  }
35 
36  StringSymbol(Context ctx, long obj) throws Z3Exception
37  {
38  super(ctx, obj);
39  }
40 
41  StringSymbol(Context ctx, String s) throws Z3Exception
42  {
43  super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
44  }
45 
46  void checkNativeObject(long obj) throws Z3Exception
47  {
48  if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
49  .toInt())
50  throw new Z3Exception("Symbol is not of String kind");
51 
52  super.checkNativeObject(obj);
53  }
54 }
static String getSymbolString(long a0, long a1)
Definition: Native.java:1949
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