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 
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 }
static long mkAstVector(long a0)
Definition: Native.java:4452
DatatypeExpr [] ToDatatypeExprArray()
Definition: ASTVector.java:188
static void astVectorIncRef(long a0, long a1)
Definition: Native.java:4461
ArithExpr [] ToArithExprExprArray()
Definition: ASTVector.java:164
static String astVectorToString(long a0, long a1)
Definition: Native.java:4528
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
void storeReference(Context ctx, T obj)
static long astVectorTranslate(long a0, long a1, long a2)
Definition: Native.java:4519
RealExpr [] ToRealExprArray()
Definition: ASTVector.java:236
static int astVectorSize(long a0, long a1)
Definition: Native.java:4477
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:3944
ASTVector translate(Context ctx)
Definition: ASTVector.java:80
static void astVectorSet(long a0, long a1, int a2, long a3)
Definition: Native.java:4495
static long astVectorGet(long a0, long a1, int a2)
Definition: Native.java:4486
void resize(int newSize)
Definition: ASTVector.java:58
ArrayExpr [] ToArrayExprArray()
Definition: ASTVector.java:176
BitVecExpr [] ToBitVecExprArray()
Definition: ASTVector.java:152
static void astVectorPush(long a0, long a1, long a2)
Definition: Native.java:4511
static void astVectorResize(long a0, long a1, int a2)
Definition: Native.java:4503
FPRMExpr [] ToFPRMExprArray()
Definition: ASTVector.java:212
def String(name, ctx=None)
Definition: z3py.py:9443