Symbol.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_symbol_kind;
 
public class Symbol extends Z3Object {
    protected Z3_symbol_kind getKind()
    {
        return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
                getNativeObject()));
    }
 
    public boolean isIntSymbol()
    {
        return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL;
    }
 
    public boolean isStringSymbol()
    {
        return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
    }
 
    @Override
    public boolean equals(Object o)
    {
        if (o == this) return true;
        if (!(o instanceof Symbol)) return false;
        Symbol other = (Symbol) o;
        return this.getNativeObject() == other.getNativeObject();
    }
 
    @Override
    public String toString() {
        if (isIntSymbol()) {
            return Integer.toString(((IntSymbol) this).getInt());
        } else if (isStringSymbol()) {
            return ((StringSymbol) this).getString();
        } else {
            return "Z3Exception: Unknown symbol kind encountered.";
        }
    }
 
    protected Symbol(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        // Symbol does not require tracking.
    }
 
    @Override
    void addToReferenceQueue() {
 
        // Symbol does not require tracking.
    }
 
    static Symbol create(Context ctx, long obj)
    {
        switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
        {
        case Z3_INT_SYMBOL:
            return new IntSymbol(ctx, obj);
        case Z3_STRING_SYMBOL:
            return new StringSymbol(ctx, obj);
        default:
            throw new Z3Exception("Unknown symbol kind encountered");
        }
    }
}