Vectors of ASTs.
Definition at line 23 of file ASTVector.java.
◆ get()
Retrieves the i-th object in the vector. Remarks: May throw an
IndexOutOfBoundsException
when
is out of range.
- Parameters
-
- Returns
- An AST
- Exceptions
-
Definition at line 41 of file ASTVector.java.
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
◆ push()
Add the AST
to the back of the vector. The size is increased by 1.
- Parameters
-
Definition at line 68 of file ASTVector.java.
70 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
◆ resize()
void resize |
( |
int |
newSize | ) |
|
|
inline |
Resize the vector to
.
- Parameters
-
newSize | The new size of the vector. |
Definition at line 58 of file ASTVector.java.
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
◆ set()
void set |
( |
int |
i, |
|
|
AST |
value |
|
) |
| |
|
inline |
Definition at line 47 of file ASTVector.java.
50 Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51 value.getNativeObject());
◆ size()
The size of the vector
Definition at line 27 of file ASTVector.java.
29 return Native.astVectorSize(getContext().nCtx(), getNativeObject());
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().
◆ ToArithExprExprArray()
Translates the AST vector into an ArithExpr[]
Definition at line 164 of file ASTVector.java.
167 ArithExpr[] res =
new ArithExpr[n];
168 for (
int i = 0; i < n; i++)
169 res[i] = (ArithExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToArray()
Translates the AST vector into an AST[]
Definition at line 117 of file ASTVector.java.
120 AST[] res =
new AST[n];
121 for (
int i = 0; i < n; i++)
122 res[i] = AST.create(getContext(),
get(i).getNativeObject());
◆ ToArrayExprArray()
Translates the AST vector into an ArrayExpr[]
Definition at line 176 of file ASTVector.java.
179 ArrayExpr[] res =
new ArrayExpr[n];
180 for (
int i = 0; i < n; i++)
181 res[i] = (ArrayExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToBitVecExprArray()
Translates the AST vector into an BitVecExpr[]
Definition at line 152 of file ASTVector.java.
155 BitVecExpr[] res =
new BitVecExpr[n];
156 for (
int i = 0; i < n; i++)
157 res[i] = (BitVecExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToBoolExprArray()
Translates the AST vector into an BoolExpr[]
Definition at line 140 of file ASTVector.java.
143 BoolExpr[] res =
new BoolExpr[n];
144 for (
int i = 0; i < n; i++)
145 res[i] = (BoolExpr) Expr.create(getContext(),
get(i).getNativeObject());
Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), Optimize.getAssertions(), Fixedpoint.getRules(), Optimize.getUnsatCore(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), and Fixedpoint.ParseString().
◆ ToDatatypeExprArray()
Translates the AST vector into an DatatypeExpr[]
Definition at line 188 of file ASTVector.java.
191 DatatypeExpr[] res =
new DatatypeExpr[n];
192 for (
int i = 0; i < n; i++)
193 res[i] = (DatatypeExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToExprArray()
◆ ToFPExprArray()
Translates the AST vector into an FPExpr[]
Definition at line 200 of file ASTVector.java.
203 FPExpr[] res =
new FPExpr[n];
204 for (
int i = 0; i < n; i++)
205 res[i] = (FPExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToFPRMExprArray()
Translates the AST vector into an FPRMExpr[]
Definition at line 212 of file ASTVector.java.
215 FPRMExpr[] res =
new FPRMExpr[n];
216 for (
int i = 0; i < n; i++)
217 res[i] = (FPRMExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToIntExprArray()
Translates the AST vector into an IntExpr[]
Definition at line 224 of file ASTVector.java.
227 IntExpr[] res =
new IntExpr[n];
228 for (
int i = 0; i < n; i++)
229 res[i] = (IntExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ ToRealExprArray()
Translates the AST vector into an RealExpr[]
Definition at line 236 of file ASTVector.java.
239 RealExpr[] res =
new RealExpr[n];
240 for (
int i = 0; i < n; i++)
241 res[i] = (RealExpr)Expr.create(getContext(),
get(i).getNativeObject());
◆ toString()
Retrieves a string representation of the vector.
Definition at line 90 of file ASTVector.java.
91 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
◆ translate()
Translates all ASTs in the vector to
.
- Parameters
-
- Returns
- A new ASTVector
- Exceptions
-
Definition at line 80 of file ASTVector.java.
82 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
83 .nCtx(), getNativeObject(), ctx.nCtx()));