18package com.microsoft.z3;
29 return Native.astVectorSize(getContext().nCtx(), getNativeObject());
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
47 public void set(
int i,
AST value)
50 Native.astVectorSet(getContext().
nCtx(), getNativeObject(), i,
51 value.getNativeObject());
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
70 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
82 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
83 .nCtx(), getNativeObject(), ctx.
nCtx()));
91 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
101 super(ctx, Native.mkAstVector(ctx.
nCtx()));
106 Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
110 void addToReferenceQueue() {
121 for (
int i = 0; i < n; i++)
122 res[i] =
AST.create(getContext(),
get(i).getNativeObject());
132 for (
int i = 0; i < n; i++)
133 res[i] =
Expr.create(getContext(),
get(i).getNativeObject());
144 for (
int i = 0; i < n; i++)
145 res[i] = (
BoolExpr)
Expr.create(getContext(),
get(i).getNativeObject());
156 for (
int i = 0; i < n; i++)
157 res[i] = (
BitVecExpr)
Expr.create(getContext(),
get(i).getNativeObject());
168 for (
int i = 0; i < n; i++)
180 for (
int i = 0; i < n; i++)
192 for (
int i = 0; i < n; i++)
204 for (
int i = 0; i < n; i++)
205 res[i] = (
FPExpr)
Expr.create(getContext(),
get(i).getNativeObject());
216 for (
int i = 0; i < n; i++)
217 res[i] = (
FPRMExpr)
Expr.create(getContext(),
get(i).getNativeObject());
228 for (
int i = 0; i < n; i++)
229 res[i] = (
IntExpr)
Expr.create(getContext(),
get(i).getNativeObject());
240 for (
int i = 0; i < n; i++)
241 res[i] = (
RealExpr)
Expr.create(getContext(),
get(i).getNativeObject());
ArithExpr<?>[] ToArithExprExprArray()
BoolExpr[] ToBoolExprArray()
BitVecExpr[] ToBitVecExprArray()
RealExpr[] ToRealExprArray()
FPRMExpr[] ToFPRMExprArray()
IntExpr[] ToIntExprArray()
ArrayExpr<?, ?>[] ToArrayExprArray()
DatatypeExpr<?>[] ToDatatypeExprArray()
ASTVector(Context ctx, long obj)
ASTVector translate(Context ctx)
IDecRefQueue< ASTVector > getASTVectorDRQ()
void storeReference(Context ctx, T obj)
def String(name, ctx=None)