Z3
Public Member Functions
ASTVector Class Reference
+ Inheritance diagram for ASTVector:

Public Member Functions

int size ()
 
AST get (int i)
 
void set (int i, AST value)
 
void resize (int newSize)
 
void push (AST a)
 
ASTVector translate (Context ctx)
 
String toString ()
 
AST[] ToArray ()
 
Expr[] ToExprArray ()
 
BoolExpr[] ToBoolExprArray ()
 
BitVecExpr[] ToBitVecExprArray ()
 
ArithExpr[] ToArithExprExprArray ()
 
ArrayExpr[] ToArrayExprArray ()
 
DatatypeExpr[] ToDatatypeExprArray ()
 
FPExpr[] ToFPExprArray ()
 
FPRMExpr[] ToFPRMExprArray ()
 
IntExpr[] ToIntExprArray ()
 
RealExpr[] ToRealExprArray ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

Member Function Documentation

AST get ( int  i)
inline

Retrieves the i-th object in the vector. Remarks: May throw an

IndexOutOfBoundsException

when

i

is out of range.

Parameters
iIndex
Returns
An AST
Exceptions
Z3Exception

Definition at line 42 of file ASTVector.java.

43  {
44  return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
45  getNativeObject(), i));
46  }
void push ( AST  a)
inline

Add the AST

a

to the back of the vector. The size is increased by 1.

Parameters
aAn AST

Definition at line 69 of file ASTVector.java.

70  {
71  Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
72  }
void resize ( int  newSize)
inline

Resize the vector to

newSize

.

Parameters
newSizeThe new size of the vector.

Definition at line 59 of file ASTVector.java.

60  {
61  Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
62  }
void set ( int  i,
AST  value 
)
inline

Definition at line 48 of file ASTVector.java.

49  {
50 
51  Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
52  value.getNativeObject());
53  }
int size ( )
inline
ArithExpr [] ToArithExprExprArray ( )
inline

Translates the AST vector into an ArithExpr[]

Definition at line 173 of file ASTVector.java.

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  }
AST [] ToArray ( )
inline

Translates the AST vector into an AST[]

Definition at line 126 of file ASTVector.java.

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  }
ArrayExpr [] ToArrayExprArray ( )
inline

Translates the AST vector into an ArrayExpr[]

Definition at line 185 of file ASTVector.java.

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  }
BitVecExpr [] ToBitVecExprArray ( )
inline

Translates the AST vector into an BitVecExpr[]

Definition at line 161 of file ASTVector.java.

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  }
BoolExpr [] ToBoolExprArray ( )
inline

Translates the AST vector into an BoolExpr[]

Definition at line 149 of file ASTVector.java.

Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), InterpolationContext.GetInterpolant(), Fixedpoint.getRules(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), and Fixedpoint.ParseString().

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  }
DatatypeExpr [] ToDatatypeExprArray ( )
inline

Translates the AST vector into an DatatypeExpr[]

Definition at line 197 of file ASTVector.java.

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  }
Expr [] ToExprArray ( )
inline

Translates the AST vector into an Expr[]

Definition at line 138 of file ASTVector.java.

Referenced by Model.getSortUniverse().

138  {
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  }
FPExpr [] ToFPExprArray ( )
inline

Translates the AST vector into an FPExpr[]

Definition at line 209 of file ASTVector.java.

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  }
FPRMExpr [] ToFPRMExprArray ( )
inline

Translates the AST vector into an FPRMExpr[]

Definition at line 221 of file ASTVector.java.

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  }
IntExpr [] ToIntExprArray ( )
inline

Translates the AST vector into an IntExpr[]

Definition at line 233 of file ASTVector.java.

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  }
RealExpr [] ToRealExprArray ( )
inline

Translates the AST vector into an RealExpr[]

Definition at line 245 of file ASTVector.java.

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  }
String toString ( )
inline

Retrieves a string representation of the vector.

Definition at line 90 of file ASTVector.java.

91  {
92  try
93  {
94  return Native.astVectorToString(getContext().nCtx(), getNativeObject());
95  } catch (Z3Exception e)
96  {
97  return "Z3Exception: " + e.getMessage();
98  }
99  }
ASTVector translate ( Context  ctx)
inline

Translates all ASTs in the vector to

ctx

.

Parameters
ctxA context
Returns
A new ASTVector
Exceptions
Z3Exception

Definition at line 81 of file ASTVector.java.

82  {
83  return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
84  .nCtx(), getNativeObject(), ctx.nCtx()));
85  }