Z3 |

Symbol.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.enumerations.Z3_symbol_kind;
21
25 public class Symbol extends Z3Object {
29 protected Z3_symbol_kind getKind()
30 {
31 return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
32 getNativeObject()));
33 }
34
38 public boolean isIntSymbol()
39 {
40 return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL;
41 }
42
46 public boolean isStringSymbol()
47 {
48 return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
49 }
50
51 @Override
52 public boolean equals(Object o)
53 {
54 if (o == this) return true;
55 if (!(o instanceof Symbol)) return false;
56 Symbol other = (Symbol) o;
57 return this.getNativeObject() == other.getNativeObject();
58 }
59
63 @Override
64 public String toString() {
65 if (isIntSymbol()) {
66 return Integer.toString(((IntSymbol) this).getInt());
67 } else if (isStringSymbol()) {
68 return ((StringSymbol) this).getString();
69 } else {
70 return "Z3Exception: Unknown symbol kind encountered.";
71 }
72 }
73
77 protected Symbol(Context ctx, long obj)
78 {
79 super(ctx, obj);
80 }
81
82 @Override
83 void incRef() {
84 // Symbol does not require tracking.
85 }
86
87 @Override
88 void addToReferenceQueue() {
89
90 // Symbol does not require tracking.
91 }
92
93 static Symbol create(Context ctx, long obj)
94 {
95 switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
96 {
97 case Z3_INT_SYMBOL:
98 return new IntSymbol(ctx, obj);
99 case Z3_STRING_SYMBOL:
100 return new StringSymbol(ctx, obj);
101 default:
102 throw new Z3Exception("Unknown symbol kind encountered");
103 }
104 }
105}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.IntSymbol
Definition: IntSymbol.java:26
com.microsoft.z3.StringSymbol
Definition: StringSymbol.java:26
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Symbol.equals
boolean equals(Object o)
Definition: Symbol.java:52
com.microsoft.z3.Symbol.getKind
Z3_symbol_kind getKind()
Definition: Symbol.java:29
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition: Symbol.java:77
com.microsoft.z3.Symbol.toString
String toString()
Definition: Symbol.java:64
com.microsoft.z3.Symbol.isStringSymbol
boolean isStringSymbol()
Definition: Symbol.java:46
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition: Symbol.java:38
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
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:116
Z3_STRING_SYMBOL
@ Z3_STRING_SYMBOL
Definition: z3_api.h:118
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:117