Z3
ASTVector.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class ASTVector extends Z3Object {
27 public int size()
28 {
29 return Native.astVectorSize(getContext().nCtx(), getNativeObject());
30 }
31
41 public AST get(int i)
42 {
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
45 }
46
47 public void set(int i, AST value)
48 {
49
50 Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51 value.getNativeObject());
52 }
53
58 public void resize(int newSize)
59 {
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
61 }
62
68 public void push(AST a)
69 {
70 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
71 }
72
81 {
82 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
83 .nCtx(), getNativeObject(), ctx.nCtx()));
84 }
85
89 @Override
90 public String toString() {
91 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
92 }
93
94 ASTVector(Context ctx, long obj)
95 {
96 super(ctx, obj);
97 }
98
99 ASTVector(Context ctx)
100 {
101 super(ctx, Native.mkAstVector(ctx.nCtx()));
102 }
103
104 @Override
105 void incRef() {
106 Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
107 }
108
109 @Override
110 void addToReferenceQueue() {
111 getContext().getASTVectorDRQ().storeReference(getContext(), this);
112 }
113
117 public AST[] ToArray()
118 {
119 int n = size();
120 AST[] res = new AST[n];
121 for (int i = 0; i < n; i++)
122 res[i] = AST.create(getContext(), get(i).getNativeObject());
123 return res;
124 }
125
129 public Expr[] ToExprArray() {
130 int n = size();
131 Expr[] res = new Expr[n];
132 for (int i = 0; i < n; i++)
133 res[i] = Expr.create(getContext(), get(i).getNativeObject());
134 return res;
135 }
136
141 {
142 int n = size();
143 BoolExpr[] res = new BoolExpr[n];
144 for (int i = 0; i < n; i++)
145 res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
146 return res;
147 }
148
153 {
154 int n = size();
155 BitVecExpr[] res = new BitVecExpr[n];
156 for (int i = 0; i < n; i++)
157 res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
158 return res;
159 }
160
165 {
166 int n = size();
167 ArithExpr[] res = new ArithExpr[n];
168 for (int i = 0; i < n; i++)
169 res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
170 return res;
171 }
172
177 {
178 int n = size();
179 ArrayExpr[] res = new ArrayExpr[n];
180 for (int i = 0; i < n; i++)
181 res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
182 return res;
183 }
184
189 {
190 int n = size();
191 DatatypeExpr[] res = new DatatypeExpr[n];
192 for (int i = 0; i < n; i++)
193 res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
194 return res;
195 }
196
201 {
202 int n = size();
203 FPExpr[] res = new FPExpr[n];
204 for (int i = 0; i < n; i++)
205 res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
206 return res;
207 }
208
213 {
214 int n = size();
215 FPRMExpr[] res = new FPRMExpr[n];
216 for (int i = 0; i < n; i++)
217 res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
218 return res;
219 }
220
225 {
226 int n = size();
227 IntExpr[] res = new IntExpr[n];
228 for (int i = 0; i < n; i++)
229 res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
230 return res;
231 }
232
237 {
238 int n = size();
239 RealExpr[] res = new RealExpr[n];
240 for (int i = 0; i < n; i++)
241 res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
242 return res;
243 }
244}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
BitVecExpr[] ToBitVecExprArray()
Definition: ASTVector.java:152
RealExpr[] ToRealExprArray()
Definition: ASTVector.java:236
FPRMExpr[] ToFPRMExprArray()
Definition: ASTVector.java:212
ArrayExpr[] ToArrayExprArray()
Definition: ASTVector.java:176
DatatypeExpr[] ToDatatypeExprArray()
Definition: ASTVector.java:188
void resize(int newSize)
Definition: ASTVector.java:58
ArithExpr[] ToArithExprExprArray()
Definition: ASTVector.java:164
ASTVector translate(Context ctx)
Definition: ASTVector.java:80
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:4038
void storeReference(Context ctx, T obj)
static long astVectorTranslate(long a0, long a1, long a2)
Definition: Native.java:4966
static String astVectorToString(long a0, long a1)
Definition: Native.java:4975
static long astVectorGet(long a0, long a1, int a2)
Definition: Native.java:4933
static void astVectorPush(long a0, long a1, long a2)
Definition: Native.java:4958
static int astVectorSize(long a0, long a1)
Definition: Native.java:4924
static void astVectorSet(long a0, long a1, int a2, long a3)
Definition: Native.java:4942
static void astVectorResize(long a0, long a1, int a2)
Definition: Native.java:4950
def String(name, ctx=None)
Definition: z3py.py:10085