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 ()
| ASTVector (Context ctx, long obj)
| ASTVector (Context ctx)
AST[] | ToArray ()
Expr<?>[] | ToExprArray ()
BoolExpr[] | ToBoolExprArray ()
BitVecExpr[] | ToBitVecExprArray ()
ArithExpr<?>[] | ToArithExprExprArray ()
ArrayExpr<?, ?>[] | ToArrayExprArray ()
DatatypeExpr<?>[] | ToDatatypeExprArray ()
FPExpr[] | ToFPExprArray ()
FPRMExpr[] | ToFPRMExprArray ()
IntExpr[] | ToIntExprArray ()
RealExpr[] | ToRealExprArray ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

## Constructor & Destructor Documentation

## ◆ ASTVector() [1/2]

ASTVector | ( | Context | ctx,
|  | long | obj
| ) |  |
| inline

Definition at line 94 of file ASTVector.java.

95 {
96 super(ctx, obj);
97 }

Referenced by ASTVector.translate().

## ◆ ASTVector() [2/2]

ASTVector | ( | Context | ctx | ) |
| inline

Definition at line 99 of file ASTVector.java.

100 {
101 super(ctx, Native.mkAstVector(ctx.nCtx()));
102 }

## Member Function Documentation

## ◆ get()

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

  i | Index

Returns
  An AST

Exceptions

  Z3Exception |

Definition at line 41 of file ASTVector.java.

42 {
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
45 }

Referenced by Goal.__getitem__(), Goal.as_expr(), and Solver.getConsequences().

## ◆ push()

void push | ( | AST | a | ) |
| inline

Add the AST `a` to the back of the vector. The size is increased by 1.

Parameters

  a | An AST

Definition at line 68 of file ASTVector.java.

69 {
70 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
71 }

Referenced by Solver.getConsequences().

## ◆ resize()

void resize | ( | int | newSize | ) |
| inline

Resize the vector to `newSize`.

Parameters

  newSize | The new size of the vector.

Definition at line 58 of file ASTVector.java.

59 {
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
61 }

## ◆ set()

void set | ( | int | i,
|  | AST | value
| ) |  |
| inline

Definition at line 47 of file ASTVector.java.

48 {
49
50 Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51 value.getNativeObject());
52 }

## ◆ size()

int size | ( |  | ) |
| inline

The size of the vector

Definition at line 27 of file ASTVector.java.

28 {
29 return Native.astVectorSize(getContext().nCtx(), getNativeObject());
30 }

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Solver.getConsequences(), Solver.getNumAssertions(), BitVecSortRef.subsort(), ASTVector.ToArithExprExprArray(), ASTVector.ToArray(), ASTVector.ToArrayExprArray(), ASTVector.ToBitVecExprArray(), ASTVector.ToBoolExprArray(), ASTVector.ToDatatypeExprArray(), ASTVector.ToExprArray(), ASTVector.ToFPExprArray(), ASTVector.ToFPRMExprArray(), ASTVector.ToIntExprArray(), and ASTVector.ToRealExprArray().

## ◆ ToArithExprExprArray()

ArithExpr<?>[] ToArithExprExprArray | ( |  | ) |
| inline

Translates the AST vector into an ArithExpr[]

Definition at line 164 of file ASTVector.java.

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 }
com.microsoft.z3.ASTVector.size
int size()
Definition: ASTVector.java:27

## ◆ ToArray()

AST[] ToArray | ( |  | ) |
| inline

Translates the AST vector into an AST[]

Definition at line 117 of file ASTVector.java.

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 }

## ◆ ToArrayExprArray()

ArrayExpr<?, ?>[] ToArrayExprArray | ( |  | ) |
| inline

Translates the AST vector into an ArrayExpr[]

Definition at line 176 of file ASTVector.java.

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 }

## ◆ ToBitVecExprArray()

BitVecExpr[] ToBitVecExprArray | ( |  | ) |
| inline

Translates the AST vector into an BitVecExpr[]

Definition at line 152 of file ASTVector.java.

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 }

## ◆ ToBoolExprArray()

BoolExpr[] ToBoolExprArray | ( |  | ) |
| inline

Translates the AST vector into an BoolExpr[]

Definition at line 140 of file ASTVector.java.

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 }

Referenced by Fixedpoint.getAssertions(), Optimize.getAssertions(), Solver.getAssertions(), Fixedpoint.getRules(), Optimize.getUnsatCore(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), and Fixedpoint.ParseString().

## ◆ ToDatatypeExprArray()

DatatypeExpr<?>[] ToDatatypeExprArray | ( |  | ) |
| inline

Translates the AST vector into an DatatypeExpr[]

Definition at line 188 of file ASTVector.java.

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 }

## ◆ ToExprArray()

Expr<?>[] ToExprArray | ( |  | ) |
| inline

Translates the AST vector into an Expr[]

Definition at line 129 of file ASTVector.java.

129 {
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 }

Referenced by Optimize.getObjectives().

## ◆ ToFPExprArray()

FPExpr[] ToFPExprArray | ( |  | ) |
| inline

Translates the AST vector into an FPExpr[]

Definition at line 200 of file ASTVector.java.

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 }

## ◆ ToFPRMExprArray()

FPRMExpr[] ToFPRMExprArray | ( |  | ) |
| inline

Translates the AST vector into an FPRMExpr[]

Definition at line 212 of file ASTVector.java.

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 }

## ◆ ToIntExprArray()

IntExpr[] ToIntExprArray | ( |  | ) |
| inline

Translates the AST vector into an IntExpr[]

Definition at line 224 of file ASTVector.java.

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 }

## ◆ ToRealExprArray()

RealExpr[] ToRealExprArray | ( |  | ) |
| inline

Translates the AST vector into an RealExpr[]

Definition at line 236 of file ASTVector.java.

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 }

## ◆ toString()

String toString | ( |  | ) |
| inline

Retrieves a string representation of the vector.

Definition at line 90 of file ASTVector.java.

90 {
91 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
92 }

## ◆ translate()

ASTVector translate | ( | Context | ctx | ) |
| inline

Translates all ASTs in the vector to `ctx`.

Parameters

  ctx | A context

Returns
  A new ASTVector

Exceptions

  Z3Exception |

Definition at line 80 of file ASTVector.java.

81 {
82 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
83 .nCtx(), getNativeObject(), ctx.nCtx()));
84 }
com.microsoft.z3.ASTVector.ASTVector
ASTVector(Context ctx, long obj)
Definition: ASTVector.java:94

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().