Z3
src/api/java/ASTVector.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00023 class ASTVector extends Z3Object
00024 {
00028     public int size() throws Z3Exception
00029     {
00030         return Native.astVectorSize(getContext().nCtx(), getNativeObject());
00031     }
00032 
00041     public AST get(int i) throws Z3Exception
00042     {
00043         return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
00044                 getNativeObject(), i));
00045     }
00046 
00047     public void set(int i, AST value) throws Z3Exception
00048     {
00049 
00050         Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
00051                 value.getNativeObject());
00052     }
00053 
00058     public void resize(int newSize) throws Z3Exception
00059     {
00060         Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
00061     }
00062 
00067     public void push(AST a) throws Z3Exception
00068     {
00069         Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
00070     }
00071 
00079     public ASTVector translate(Context ctx) throws Z3Exception
00080     {
00081         return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
00082                 .nCtx(), getNativeObject(), ctx.nCtx()));
00083     }
00084 
00088     public String toString()
00089     {
00090         try
00091         {
00092             return Native.astVectorToString(getContext().nCtx(), getNativeObject());
00093         } catch (Z3Exception e)
00094         {
00095             return "Z3Exception: " + e.getMessage();
00096         }
00097     }
00098 
00099     ASTVector(Context ctx, long obj) throws Z3Exception
00100     {
00101         super(ctx, obj);
00102     }
00103 
00104     ASTVector(Context ctx) throws Z3Exception
00105     {
00106         super(ctx, Native.mkAstVector(ctx.nCtx()));
00107     }
00108 
00109     void incRef(long o) throws Z3Exception
00110     {
00111         getContext().astvector_DRQ().incAndClear(getContext(), o);
00112         super.incRef(o);
00113     }
00114 
00115     void decRef(long o) throws Z3Exception
00116     {
00117         getContext().astvector_DRQ().add(o);
00118         super.decRef(o);
00119     }
00120 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines