Z3
ASTVector.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class ASTVector extends Z3Object
24 {
28  public int size()
29  {
30  return Native.astVectorSize(getContext().nCtx(), getNativeObject());
31  }
32 
42  public AST get(int i)
43  {
44  return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
45  getNativeObject(), i));
46  }
47 
48  public void set(int i, AST value)
49  {
50 
51  Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
52  value.getNativeObject());
53  }
54 
59  public void resize(int newSize)
60  {
61  Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
62  }
63 
69  public void push(AST a)
70  {
71  Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
72  }
73 
82  {
83  return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
84  .nCtx(), getNativeObject(), ctx.nCtx()));
85  }
86 
90  public String toString()
91  {
92  try
93  {
94  return Native.astVectorToString(getContext().nCtx(), getNativeObject());
95  } catch (Z3Exception e)
96  {
97  return "Z3Exception: " + e.getMessage();
98  }
99  }
100 
101  ASTVector(Context ctx, long obj)
102  {
103  super(ctx, obj);
104  }
105 
106  ASTVector(Context ctx)
107  {
108  super(ctx, Native.mkAstVector(ctx.nCtx()));
109  }
110 
111  void incRef(long o)
112  {
113  getContext().getASTVectorDRQ().incAndClear(getContext(), o);
114  super.incRef(o);
115  }
116 
117  void decRef(long o)
118  {
119  getContext().getASTVectorDRQ().add(o);
120  super.decRef(o);
121  }
122 
126  public AST[] ToArray()
127  {
128  int n = size();
129  AST[] res = new AST[n];
130  for (int i = 0; i < n; i++)
131  res[i] = AST.create(getContext(), get(i).getNativeObject());
132  return res;
133  }
134 
138  public Expr[] ToExprArray() {
139  int n = size();
140  Expr[] res = new Expr[n];
141  for (int i = 0; i < n; i++)
142  res[i] = Expr.create(getContext(), get(i).getNativeObject());
143  return res;
144  }
145 
150  {
151  int n = size();
152  BoolExpr[] res = new BoolExpr[n];
153  for (int i = 0; i < n; i++)
154  res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
155  return res;
156  }
157 
162  {
163  int n = size();
164  BitVecExpr[] res = new BitVecExpr[n];
165  for (int i = 0; i < n; i++)
166  res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
167  return res;
168  }
169 
174  {
175  int n = size();
176  ArithExpr[] res = new ArithExpr[n];
177  for (int i = 0; i < n; i++)
178  res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
179  return res;
180  }
181 
186  {
187  int n = size();
188  ArrayExpr[] res = new ArrayExpr[n];
189  for (int i = 0; i < n; i++)
190  res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
191  return res;
192  }
193 
198  {
199  int n = size();
200  DatatypeExpr[] res = new DatatypeExpr[n];
201  for (int i = 0; i < n; i++)
202  res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
203  return res;
204  }
205 
210  {
211  int n = size();
212  FPExpr[] res = new FPExpr[n];
213  for (int i = 0; i < n; i++)
214  res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
215  return res;
216  }
217 
222  {
223  int n = size();
224  FPRMExpr[] res = new FPRMExpr[n];
225  for (int i = 0; i < n; i++)
226  res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
227  return res;
228  }
229 
234  {
235  int n = size();
236  IntExpr[] res = new IntExpr[n];
237  for (int i = 0; i < n; i++)
238  res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
239  return res;
240  }
241 
246  {
247  int n = size();
248  RealExpr[] res = new RealExpr[n];
249  for (int i = 0; i < n; i++)
250  res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
251  return res;
252  }
253 }
static long mkAstVector(long a0)
Definition: Native.java:3731
DatatypeExpr[] ToDatatypeExprArray()
Definition: ASTVector.java:197
ArithExpr[] ToArithExprExprArray()
Definition: ASTVector.java:173
static String astVectorToString(long a0, long a1)
Definition: Native.java:3807
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:149
static long astVectorTranslate(long a0, long a1, long a2)
Definition: Native.java:3798
RealExpr[] ToRealExprArray()
Definition: ASTVector.java:245
static int astVectorSize(long a0, long a1)
Definition: Native.java:3756
IDecRefQueue getASTVectorDRQ()
Definition: Context.java:3694
void incAndClear(Context ctx, long o)
ASTVector translate(Context ctx)
Definition: ASTVector.java:81
static void astVectorSet(long a0, long a1, int a2, long a3)
Definition: Native.java:3774
static long astVectorGet(long a0, long a1, int a2)
Definition: Native.java:3765
void resize(int newSize)
Definition: ASTVector.java:59
ArrayExpr[] ToArrayExprArray()
Definition: ASTVector.java:185
BitVecExpr[] ToBitVecExprArray()
Definition: ASTVector.java:161
static void astVectorPush(long a0, long a1, long a2)
Definition: Native.java:3790
static void astVectorResize(long a0, long a1, int a2)
Definition: Native.java:3782
FPRMExpr[] ToFPRMExprArray()
Definition: ASTVector.java:221