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 () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
Vectors of ASTs.
Definition at line 23 of file ASTVector.java.
|
inline |
Retrieves the i-th object in the vector. Remarks: May throw an
when
is out of range.
i | Index |
Z3Exception |
Definition at line 42 of file ASTVector.java.
Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), InterpolationContext.GetInterpolant(), Fixedpoint.getRules(), Model.getSortUniverse(), and Solver.getUnsatCore().
|
inline |
Add the AST
to the back of the vector. The size is increased by 1.
a | An AST |
Definition at line 69 of file ASTVector.java.
|
inline |
Resize the vector to
.
newSize | The new size of the vector. |
Definition at line 59 of file ASTVector.java.
|
inline |
Definition at line 48 of file ASTVector.java.
|
inline |
The size of the vector
Definition at line 28 of file ASTVector.java.
Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), InterpolationContext.GetInterpolant(), Solver.getNumAssertions(), Fixedpoint.getRules(), Model.getSortUniverse(), and Solver.getUnsatCore().
|
inline |
Retrieves a string representation of the vector.
Definition at line 90 of file ASTVector.java.
Translates all ASTs in the vector to
.
ctx | A context |
Z3Exception |
Definition at line 81 of file ASTVector.java.