18 package com.microsoft.z3;
23 class ASTVector
extends Z3Object
28 public int size() throws Z3Exception
30 return Native.astVectorSize(getContext().nCtx(), getNativeObject());
41 public AST
get(
int i)
throws Z3Exception
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
47 public void set(
int i, AST value)
throws Z3Exception
50 Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51 value.getNativeObject());
58 public void resize(
int newSize)
throws Z3Exception
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
67 public void push(AST a)
throws Z3Exception
69 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
79 public ASTVector translate(Context ctx)
throws Z3Exception
81 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
82 .nCtx(), getNativeObject(), ctx.nCtx()));
88 public String toString()
92 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
93 }
catch (Z3Exception e)
95 return "Z3Exception: " + e.getMessage();
99 ASTVector(Context ctx,
long obj)
throws Z3Exception
104 ASTVector(Context ctx)
throws Z3Exception
106 super(ctx, Native.mkAstVector(ctx.nCtx()));
109 void incRef(
long o)
throws Z3Exception
111 getContext().astvector_DRQ().incAndClear(getContext(), o);
115 void decRef(
long o)
throws Z3Exception
117 getContext().astvector_DRQ().add(o);