ASTVector.java

Go to the documentation of this file.

package com.microsoft.z3;

public class ASTVector extends Z3Object
{
    public int size()
    {
        return Native.astVectorSize(getContext().nCtx(), getNativeObject());
    }

    public AST get(int i)
    {
        return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
                getNativeObject(), i));
    }

    public void set(int i, AST value)
    {

        Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
                value.getNativeObject());
    }

    public void resize(int newSize)
    {
        Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
    }

    public void push(AST a)
    {
        Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
    }

    public ASTVector translate(Context ctx)
    {
        return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
                .nCtx(), getNativeObject(), ctx.nCtx()));
    }

    public String toString()
    {
        try
        {
            return Native.astVectorToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

    ASTVector(Context ctx, long obj)
    {
        super(ctx, obj);
    }

    ASTVector(Context ctx)
    {
        super(ctx, Native.mkAstVector(ctx.nCtx()));
    }

    void incRef(long o)
    {
        getContext().getASTVectorDRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o)
    {
        getContext().getASTVectorDRQ().add(o);
        super.decRef(o);
    }
    
    public AST[] ToArray()
    {
        int n = size();
        AST[] res = new AST[n];
        for (int i = 0; i < n; i++)
            res[i] = AST.create(getContext(), get(i).getNativeObject());
        return res;
    }
    
    public Expr[] ToExprArray() {
        int n = size();
        Expr[] res = new Expr[n];
        for (int i = 0; i < n; i++)
            res[i] = Expr.create(getContext(), get(i).getNativeObject());
        return res;     
    }

    public BoolExpr[] ToBoolExprArray()
    {
        int n = size();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public BitVecExpr[] ToBitVecExprArray()
    {
        int n = size();
        BitVecExpr[] res = new BitVecExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public ArithExpr[] ToArithExprExprArray()
    {
        int n = size();
        ArithExpr[] res = new ArithExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public ArrayExpr[] ToArrayExprArray()
    {
        int n = size();
        ArrayExpr[] res = new ArrayExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public DatatypeExpr[] ToDatatypeExprArray()
    {
        int n = size();
        DatatypeExpr[] res = new DatatypeExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public FPExpr[] ToFPExprArray()
    {
        int n = size();
        FPExpr[] res = new FPExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public FPRMExpr[] ToFPRMExprArray()
    {
        int n = size();
        FPRMExpr[] res = new FPRMExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public IntExpr[] ToIntExprArray()
    {
        int n = size();
        IntExpr[] res = new IntExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }

    public RealExpr[] ToRealExprArray()
    {
        int n = size();
        RealExpr[] res = new RealExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
        return res;
    }
}