Z3
Public Member Functions
ASTVector Class Reference
+ Inheritance diagram for ASTVector:

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 ()
 

Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

Member Function Documentation

◆ get()

AST get ( int  i)
inline

Retrieves the i-th object in the vector. Remarks: May throw an IndexOutOfBoundsException when i is out of range.

Parameters
iIndex
Returns
An AST
Exceptions
Z3Exception

Definition at line 41 of file ASTVector.java.

42 {
43 return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44 getNativeObject(), i));
45 }

Referenced by Goal.__getitem__(), and Goal.as_expr().

◆ push()

void push ( AST  a)
inline

Add the AST a to the back of the vector. The size is increased by 1.

Parameters
aAn AST

Definition at line 68 of file ASTVector.java.

69 {
70 Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
71 }

◆ resize()

void resize ( int  newSize)
inline

Resize the vector to newSize.

Parameters
newSizeThe new size of the vector.

Definition at line 58 of file ASTVector.java.

59 {
60 Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
61 }

◆ set()

void set ( int  i,
AST  value 
)
inline

Definition at line 47 of file ASTVector.java.

48 {
49
50 Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51 value.getNativeObject());
52 }

◆ size()

int size ( )
inline

◆ ToArithExprExprArray()

ArithExpr[] ToArithExprExprArray ( )
inline

Translates the AST vector into an ArithExpr[]

Definition at line 164 of file ASTVector.java.

165 {
166 int n = size();
167 ArithExpr[] res = new ArithExpr[n];
168 for (int i = 0; i < n; i++)
169 res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
170 return res;
171 }

◆ ToArray()

AST[] ToArray ( )
inline

Translates the AST vector into an AST[]

Definition at line 117 of file ASTVector.java.

118 {
119 int n = size();
120 AST[] res = new AST[n];
121 for (int i = 0; i < n; i++)
122 res[i] = AST.create(getContext(), get(i).getNativeObject());
123 return res;
124 }

◆ ToArrayExprArray()

ArrayExpr[] ToArrayExprArray ( )
inline

Translates the AST vector into an ArrayExpr[]

Definition at line 176 of file ASTVector.java.

177 {
178 int n = size();
179 ArrayExpr[] res = new ArrayExpr[n];
180 for (int i = 0; i < n; i++)
181 res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
182 return res;
183 }

◆ ToBitVecExprArray()

BitVecExpr[] ToBitVecExprArray ( )
inline

Translates the AST vector into an BitVecExpr[]

Definition at line 152 of file ASTVector.java.

153 {
154 int n = size();
155 BitVecExpr[] res = new BitVecExpr[n];
156 for (int i = 0; i < n; i++)
157 res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
158 return res;
159 }

◆ ToBoolExprArray()

BoolExpr[] ToBoolExprArray ( )
inline

Translates the AST vector into an BoolExpr[]

Definition at line 140 of file ASTVector.java.

141 {
142 int n = size();
143 BoolExpr[] res = new BoolExpr[n];
144 for (int i = 0; i < n; i++)
145 res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
146 return res;
147 }

Referenced by Fixedpoint.getAssertions(), Optimize.getAssertions(), Solver.getAssertions(), Fixedpoint.getRules(), Optimize.getUnsatCore(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), and Fixedpoint.ParseString().

◆ ToDatatypeExprArray()

DatatypeExpr[] ToDatatypeExprArray ( )
inline

Translates the AST vector into an DatatypeExpr[]

Definition at line 188 of file ASTVector.java.

189 {
190 int n = size();
191 DatatypeExpr[] res = new DatatypeExpr[n];
192 for (int i = 0; i < n; i++)
193 res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
194 return res;
195 }

◆ ToExprArray()

Expr[] ToExprArray ( )
inline

Translates the AST vector into an Expr[]

Definition at line 129 of file ASTVector.java.

129 {
130 int n = size();
131 Expr[] res = new Expr[n];
132 for (int i = 0; i < n; i++)
133 res[i] = Expr.create(getContext(), get(i).getNativeObject());
134 return res;
135 }

Referenced by Optimize.getObjectives(), and Model.getSortUniverse().

◆ ToFPExprArray()

FPExpr[] ToFPExprArray ( )
inline

Translates the AST vector into an FPExpr[]

Definition at line 200 of file ASTVector.java.

201 {
202 int n = size();
203 FPExpr[] res = new FPExpr[n];
204 for (int i = 0; i < n; i++)
205 res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
206 return res;
207 }

◆ ToFPRMExprArray()

FPRMExpr[] ToFPRMExprArray ( )
inline

Translates the AST vector into an FPRMExpr[]

Definition at line 212 of file ASTVector.java.

213 {
214 int n = size();
215 FPRMExpr[] res = new FPRMExpr[n];
216 for (int i = 0; i < n; i++)
217 res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
218 return res;
219 }

◆ ToIntExprArray()

IntExpr[] ToIntExprArray ( )
inline

Translates the AST vector into an IntExpr[]

Definition at line 224 of file ASTVector.java.

225 {
226 int n = size();
227 IntExpr[] res = new IntExpr[n];
228 for (int i = 0; i < n; i++)
229 res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
230 return res;
231 }

◆ ToRealExprArray()

RealExpr[] ToRealExprArray ( )
inline

Translates the AST vector into an RealExpr[]

Definition at line 236 of file ASTVector.java.

237 {
238 int n = size();
239 RealExpr[] res = new RealExpr[n];
240 for (int i = 0; i < n; i++)
241 res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
242 return res;
243 }

◆ toString()

String toString ( )
inline

Retrieves a string representation of the vector.

Definition at line 90 of file ASTVector.java.

90 {
91 return Native.astVectorToString(getContext().nCtx(), getNativeObject());
92 }

◆ translate()

ASTVector translate ( Context  ctx)
inline

Translates all ASTs in the vector to ctx.

Parameters
ctxA context
Returns
A new ASTVector
Exceptions
Z3Exception

Definition at line 80 of file ASTVector.java.

81 {
82 return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
83 .nCtx(), getNativeObject(), ctx.nCtx()));
84 }

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__().