Z3 |

ASTVector.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public 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
80 public ASTVector translate(Context ctx)
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 public ASTVector(Context ctx, long obj)
95 {
96 super(ctx, obj);
97 }
98
99 public 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
140 public BoolExpr[] ToBoolExprArray()
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
152 public BitVecExpr[] ToBitVecExprArray()
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
164 public ArithExpr<?>[] ToArithExprExprArray()
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
176 public ArrayExpr<?, ?>[] ToArrayExprArray()
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
188 public DatatypeExpr<?>[] ToDatatypeExprArray()
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
200 public FPExpr[] ToFPExprArray()
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
212 public FPRMExpr[] ToFPRMExprArray()
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
224 public IntExpr[] ToIntExprArray()
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
236 public RealExpr[] ToRealExprArray()
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.ASTVector.push
void push(AST a)
Definition: ASTVector.java:68
com.microsoft.z3.ASTVector.ToArithExprExprArray
ArithExpr<?>[] ToArithExprExprArray()
Definition: ASTVector.java:164
com.microsoft.z3.ASTVector.ToFPExprArray
FPExpr[] ToFPExprArray()
Definition: ASTVector.java:200
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.ASTVector.ToExprArray
Expr<?>[] ToExprArray()
Definition: ASTVector.java:129
com.microsoft.z3.ASTVector.ToBitVecExprArray
BitVecExpr[] ToBitVecExprArray()
Definition: ASTVector.java:152
com.microsoft.z3.ASTVector.ASTVector
ASTVector(Context ctx)
Definition: ASTVector.java:99
com.microsoft.z3.ASTVector.ToRealExprArray
RealExpr[] ToRealExprArray()
Definition: ASTVector.java:236
com.microsoft.z3.ASTVector.ToFPRMExprArray
FPRMExpr[] ToFPRMExprArray()
Definition: ASTVector.java:212
com.microsoft.z3.ASTVector.ToIntExprArray
IntExpr[] ToIntExprArray()
Definition: ASTVector.java:224
com.microsoft.z3.ASTVector.ToArray
AST[] ToArray()
Definition: ASTVector.java:117
com.microsoft.z3.ASTVector.resize
void resize(int newSize)
Definition: ASTVector.java:58
com.microsoft.z3.ASTVector.ToArrayExprArray
ArrayExpr<?, ?>[] ToArrayExprArray()
Definition: ASTVector.java:176
com.microsoft.z3.ASTVector.toString
String toString()
Definition: ASTVector.java:90
com.microsoft.z3.ASTVector.ToDatatypeExprArray
DatatypeExpr<?>[] ToDatatypeExprArray()
Definition: ASTVector.java:188
com.microsoft.z3.ASTVector.ASTVector
ASTVector(Context ctx, long obj)
Definition: ASTVector.java:94
com.microsoft.z3.ASTVector.translate
ASTVector translate(Context ctx)
Definition: ASTVector.java:80
com.microsoft.z3.ASTVector.size
int size()
Definition: ASTVector.java:27
com.microsoft.z3.ArithExpr
Definition: ArithExpr.java:24
com.microsoft.z3.ArrayExpr
Definition: ArrayExpr.java:25
com.microsoft.z3.BitVecExpr
Definition: BitVecExpr.java:24
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Context.getASTVectorDRQ
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:4080
com.microsoft.z3.DatatypeExpr
Definition: DatatypeExpr.java:24
com.microsoft.z3.Expr
Definition: Expr.java:35
com.microsoft.z3.FPExpr
Definition: FPExpr.java:23
com.microsoft.z3.FPRMExpr
Definition: FPRMExpr.java:23
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.IntExpr
Definition: IntExpr.java:24
com.microsoft.z3.RealExpr
Definition: RealExpr.java:24
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693