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 }