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

Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

Constructor & Destructor Documentation

◆ ASTVector() [1/2]

ASTVector ( Context  ctx,
long  obj 
)
inline

Definition at line 94 of file ASTVector.java.

95  {
96  super(ctx, obj);
97  }

Referenced by ASTVector.translate().

◆ ASTVector() [2/2]

ASTVector ( Context  ctx)
inline

Definition at line 99 of file ASTVector.java.

100  {
101  super(ctx, Native.mkAstVector(ctx.nCtx()));
102  }

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__(), Goal.as_expr(), and Solver.getConsequences().

◆ 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  }

Referenced by Solver.getConsequences().

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

◆ 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  }
ASTVector(Context ctx, long obj)
Definition: ASTVector.java:94

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