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 () |
![]() | |
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.
|
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.getNumAssertions(), ASTVector.ToArithExprExprArray(), ASTVector.ToArray(), ASTVector.ToArrayExprArray(), ASTVector.ToBitVecExprArray(), ASTVector.ToBoolExprArray(), ASTVector.ToDatatypeExprArray(), ASTVector.ToExprArray(), ASTVector.ToFPExprArray(), ASTVector.ToFPRMExprArray(), ASTVector.ToIntExprArray(), and ASTVector.ToRealExprArray().
|
inline |
|
inline |
|
inline |
|
inline |
|
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().
|
inline |
|
inline |
Translates the AST vector into an Expr[]
Definition at line 138 of file ASTVector.java.
Referenced by Model.getSortUniverse().
|
inline |
|
inline |
|
inline |
|
inline |
|
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.