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 () |
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 41 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 68 of file ASTVector.java.
|
inline |
Resize the vector to
.
newSize | The new size of the vector. |
Definition at line 58 of file ASTVector.java.
|
inline |
Definition at line 47 of file ASTVector.java.
|
inline |
The size of the vector
Definition at line 27 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 140 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 129 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 80 of file ASTVector.java.