Z3
Data Structures | 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 25 of file ASTVector.java.

Constructor & Destructor Documentation

◆ ASTVector() [1/2]

ASTVector ( Context  ctx,
long  obj 
)
inline

Definition at line 96 of file ASTVector.java.

97  {
98  super(ctx, obj);
99  }

Referenced by ASTVector.translate().

◆ ASTVector() [2/2]

ASTVector ( Context  ctx)
inline

Definition at line 101 of file ASTVector.java.

102  {
103  super(ctx, Native.mkAstVector(ctx.nCtx()));
104  }

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 43 of file ASTVector.java.

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

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 70 of file ASTVector.java.

71  {
72  Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
73  }

Referenced by Solver.__enter__(), and Solver.getConsequences().

◆ resize()

void resize ( int  newSize)
inline

Resize the vector to

newSize

.

Parameters
newSizeThe new size of the vector.

Definition at line 60 of file ASTVector.java.

61  {
62  Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
63  }

◆ set()

void set ( int  i,
AST  value 
)
inline

Definition at line 49 of file ASTVector.java.

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

◆ size()

int size ( )
inline

◆ ToArithExprExprArray()

ArithExpr<?> [] ToArithExprExprArray ( )
inline

Translates the AST vector into an ArithExpr[]

Definition at line 156 of file ASTVector.java.

157  {
158  int n = size();
159  ArithExpr<?>[] res = new ArithExpr[n];
160  for (int i = 0; i < n; i++)
161  res[i] = (ArithExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
162  return res;
163  }

◆ ToArray()

AST [] ToArray ( )
inline

Translates the AST vector into an AST[]

Definition at line 109 of file ASTVector.java.

110  {
111  int n = size();
112  AST[] res = new AST[n];
113  for (int i = 0; i < n; i++)
114  res[i] = AST.create(getContext(), get(i).getNativeObject());
115  return res;
116  }

◆ ToArrayExprArray()

ArrayExpr<?, ?> [] ToArrayExprArray ( )
inline

Translates the AST vector into an ArrayExpr[]

Definition at line 168 of file ASTVector.java.

169  {
170  int n = size();
171  ArrayExpr<?, ?>[] res = new ArrayExpr[n];
172  for (int i = 0; i < n; i++)
173  res[i] = (ArrayExpr<?, ?>)Expr.create(getContext(), get(i).getNativeObject());
174  return res;
175  }

◆ ToBitVecExprArray()

BitVecExpr [] ToBitVecExprArray ( )
inline

Translates the AST vector into an BitVecExpr[]

Definition at line 144 of file ASTVector.java.

145  {
146  int n = size();
147  BitVecExpr[] res = new BitVecExpr[n];
148  for (int i = 0; i < n; i++)
149  res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
150  return res;
151  }

◆ ToBoolExprArray()

BoolExpr [] ToBoolExprArray ( )
inline

Translates the AST vector into an BoolExpr[]

Definition at line 132 of file ASTVector.java.

133  {
134  int n = size();
135  BoolExpr[] res = new BoolExpr[n];
136  for (int i = 0; i < n; i++)
137  res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
138  return res;
139  }

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 180 of file ASTVector.java.

181  {
182  int n = size();
183  DatatypeExpr<?>[] res = new DatatypeExpr[n];
184  for (int i = 0; i < n; i++)
185  res[i] = (DatatypeExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
186  return res;
187  }

◆ ToExprArray()

Expr<?> [] ToExprArray ( )
inline

Translates the AST vector into an Expr[]

Definition at line 121 of file ASTVector.java.

121  {
122  int n = size();
123  Expr<?>[] res = new Expr[n];
124  for (int i = 0; i < n; i++)
125  res[i] = Expr.create(getContext(), get(i).getNativeObject());
126  return res;
127  }

Referenced by Optimize.getObjectives().

◆ ToFPExprArray()

FPExpr [] ToFPExprArray ( )
inline

Translates the AST vector into an FPExpr[]

Definition at line 192 of file ASTVector.java.

193  {
194  int n = size();
195  FPExpr[] res = new FPExpr[n];
196  for (int i = 0; i < n; i++)
197  res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
198  return res;
199  }

◆ ToFPRMExprArray()

FPRMExpr [] ToFPRMExprArray ( )
inline

Translates the AST vector into an FPRMExpr[]

Definition at line 204 of file ASTVector.java.

205  {
206  int n = size();
207  FPRMExpr[] res = new FPRMExpr[n];
208  for (int i = 0; i < n; i++)
209  res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
210  return res;
211  }

◆ ToIntExprArray()

IntExpr [] ToIntExprArray ( )
inline

Translates the AST vector into an IntExpr[]

Definition at line 216 of file ASTVector.java.

217  {
218  int n = size();
219  IntExpr[] res = new IntExpr[n];
220  for (int i = 0; i < n; i++)
221  res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
222  return res;
223  }

◆ ToRealExprArray()

RealExpr [] ToRealExprArray ( )
inline

Translates the AST vector into an RealExpr[]

Definition at line 228 of file ASTVector.java.

229  {
230  int n = size();
231  RealExpr[] res = new RealExpr[n];
232  for (int i = 0; i < n; i++)
233  res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
234  return res;
235  }

◆ toString()

String toString ( )
inline

Retrieves a string representation of the vector.

Definition at line 92 of file ASTVector.java.

92  {
93  return Native.astVectorToString(getContext().nCtx(), getNativeObject());
94  }

◆ 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 82 of file ASTVector.java.

83  {
84  return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
85  .nCtx(), getNativeObject(), ctx.nCtx()));
86  }
ASTVector(Context ctx, long obj)
Definition: ASTVector.java:96

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