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) |
Vectors of ASTs.
Definition at line 25 of file ASTVector.java.
Definition at line 96 of file ASTVector.java.
Referenced by ASTVector.translate().
Definition at line 101 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 43 of file ASTVector.java.
Referenced by Goal.__getitem__(), Goal.as_expr(), and Solver.getConsequences().
|
inline |
Add the AST
to the back of the vector. The size is increased by 1.
a | An AST |
Definition at line 70 of file ASTVector.java.
Referenced by Solver.__enter__(), and Solver.getConsequences().
|
inline |
Resize the vector to
.
newSize | The new size of the vector. |
Definition at line 60 of file ASTVector.java.
|
inline |
Definition at line 49 of file ASTVector.java.
|
inline |
The size of the vector
Definition at line 29 of file ASTVector.java.
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().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Translates the AST vector into an BoolExpr[]
Definition at line 132 of file ASTVector.java.
Referenced by Fixedpoint.getAssertions(), Optimize.getAssertions(), Solver.getAssertions(), Fixedpoint.getRules(), Optimize.getUnsatCore(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), and Fixedpoint.ParseString().
|
inline |
|
inline |
Translates the AST vector into an Expr[]
Definition at line 121 of file ASTVector.java.
Referenced by Optimize.getObjectives().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Retrieves a string representation of the vector.
Definition at line 92 of file ASTVector.java.
Translates all ASTs in the vector to
.
ctx | A context |
Z3Exception |
Definition at line 82 of file ASTVector.java.
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__().