Z3
Public Member Functions | Properties
ASTVector Class Reference

Vectors of ASTs. More...

+ Inheritance diagram for ASTVector:

Public Member Functions

void Resize (uint newSize)
 Resize the vector to newSize . More...
 
void Push (AST a)
 Add the AST a to the back of the vector. The size is increased by 1. More...
 
ASTVector Translate (Context ctx)
 Translates all ASTs in the vector to ctx . More...
 
override string ToString ()
 Retrieves a string representation of the vector. More...
 
AST[] ToArray ()
 Translates an AST vector into an AST[] More...
 
Expr[] ToExprArray ()
 Translates an ASTVector into an Expr[] More...
 
BoolExpr[] ToBoolExprArray ()
 Translates an ASTVector into a BoolExpr[] More...
 
BitVecExpr[] ToBitVecExprArray ()
 Translates an ASTVector into a BitVecExpr[] More...
 
ArithExpr[] ToArithExprArray ()
 Translates an ASTVector into a ArithExpr[] More...
 
ArrayExpr[] ToArrayExprArray ()
 Translates an ASTVector into a ArrayExpr[] More...
 
DatatypeExpr[] ToDatatypeExprArray ()
 Translates an ASTVector into a DatatypeExpr[] More...
 
FPExpr[] ToFPExprArray ()
 Translates an ASTVector into a FPExpr[] More...
 
FPRMExpr[] ToFPRMExprArray ()
 Translates an ASTVector into a FPRMExpr[] More...
 
IntExpr[] ToIntExprArray ()
 Translates an ASTVector into a IntExpr[] More...
 
RealExpr[] ToRealExprArray ()
 Translates an ASTVector into a RealExpr[] More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

uint Size [get]
 The size of the vector More...
 
AST this[uint i] [get, set]
 Retrieves the i-th object in the vector. More...
 
- Properties inherited from Z3Object
Context Context [get]
 Access Context object More...
 

Detailed Description

Vectors of ASTs.

Definition at line 28 of file ASTVector.cs.

Member Function Documentation

◆ 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 73 of file ASTVector.cs.

74  {
75  Debug.Assert(a != null);
76 
77  Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
78  }
Context Context
Access Context object
Definition: Z3Object.cs:111

◆ Resize()

void Resize ( uint  newSize)
inline

Resize the vector to newSize .

Parameters
newSizeThe new size of the vector.

Definition at line 63 of file ASTVector.cs.

64  {
65  Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
66  }

◆ ToArithExprArray()

ArithExpr [] ToArithExprArray ( )
inline

Translates an ASTVector into a ArithExpr[]


Definition at line 151 of file ASTVector.cs.

152  {
153  uint n = Size;
154  ArithExpr[] res = new ArithExpr[n];
155  for (uint i = 0; i < n; i++)
156  res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
157  return res;
158  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

◆ ToArray()

AST [] ToArray ( )
inline

Translates an AST vector into an AST[]


Definition at line 103 of file ASTVector.cs.

104  {
105  uint n = Size;
106  AST[] res = new AST[n];
107  for (uint i = 0; i < n; i++)
108  res[i] = AST.Create(this.Context, this[i].NativeObject);
109  return res;
110  }

◆ ToArrayExprArray()

ArrayExpr [] ToArrayExprArray ( )
inline

Translates an ASTVector into a ArrayExpr[]


Definition at line 163 of file ASTVector.cs.

164  {
165  uint n = Size;
166  ArrayExpr[] res = new ArrayExpr[n];
167  for (uint i = 0; i < n; i++)
168  res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
169  return res;
170  }

◆ ToBitVecExprArray()

BitVecExpr [] ToBitVecExprArray ( )
inline

Translates an ASTVector into a BitVecExpr[]


Definition at line 139 of file ASTVector.cs.

140  {
141  uint n = Size;
142  BitVecExpr[] res = new BitVecExpr[n];
143  for (uint i = 0; i < n; i++)
144  res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
145  return res;
146  }

◆ ToBoolExprArray()

BoolExpr [] ToBoolExprArray ( )
inline

Translates an ASTVector into a BoolExpr[]


Definition at line 127 of file ASTVector.cs.

128  {
129  uint n = Size;
130  BoolExpr[] res = new BoolExpr[n];
131  for (uint i = 0; i < n; i++)
132  res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
133  return res;
134  }

Referenced by Solver.Cube(), Fixedpoint.ParseFile(), Context.ParseSMTLIB2File(), Context.ParseSMTLIB2String(), and Fixedpoint.ParseString().

◆ ToDatatypeExprArray()

DatatypeExpr [] ToDatatypeExprArray ( )
inline

Translates an ASTVector into a DatatypeExpr[]


Definition at line 175 of file ASTVector.cs.

176  {
177  uint n = Size;
178  DatatypeExpr[] res = new DatatypeExpr[n];
179  for (uint i = 0; i < n; i++)
180  res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
181  return res;
182  }

◆ ToExprArray()

Expr [] ToExprArray ( )
inline

Translates an ASTVector into an Expr[]


Definition at line 115 of file ASTVector.cs.

116  {
117  uint n = Size;
118  Expr[] res = new Expr[n];
119  for (uint i = 0; i < n; i++)
120  res[i] = Expr.Create(this.Context, this[i].NativeObject);
121  return res;
122  }

Referenced by Model.SortUniverse().

◆ ToFPExprArray()

FPExpr [] ToFPExprArray ( )
inline

Translates an ASTVector into a FPExpr[]


Definition at line 187 of file ASTVector.cs.

188  {
189  uint n = Size;
190  FPExpr[] res = new FPExpr[n];
191  for (uint i = 0; i < n; i++)
192  res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
193  return res;
194  }

◆ ToFPRMExprArray()

FPRMExpr [] ToFPRMExprArray ( )
inline

Translates an ASTVector into a FPRMExpr[]


Definition at line 199 of file ASTVector.cs.

200  {
201  uint n = Size;
202  FPRMExpr[] res = new FPRMExpr[n];
203  for (uint i = 0; i < n; i++)
204  res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
205  return res;
206  }

◆ ToIntExprArray()

IntExpr [] ToIntExprArray ( )
inline

Translates an ASTVector into a IntExpr[]


Definition at line 211 of file ASTVector.cs.

212  {
213  uint n = Size;
214  IntExpr[] res = new IntExpr[n];
215  for (uint i = 0; i < n; i++)
216  res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
217  return res;
218  }

◆ ToRealExprArray()

RealExpr [] ToRealExprArray ( )
inline

Translates an ASTVector into a RealExpr[]


Definition at line 223 of file ASTVector.cs.

224  {
225  uint n = Size;
226  RealExpr[] res = new RealExpr[n];
227  for (uint i = 0; i < n; i++)
228  res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
229  return res;
230  }

◆ ToString()

override string ToString ( )
inline

Retrieves a string representation of the vector.


Definition at line 95 of file ASTVector.cs.

96  {
97  return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
98  }

◆ Translate()

ASTVector Translate ( Context  ctx)
inline

Translates all ASTs in the vector to ctx .

Parameters
ctxA context
Returns
A new ASTVector

Definition at line 85 of file ASTVector.cs.

86  {
87  Debug.Assert(ctx != null);
88 
89  return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
90  }

Property Documentation

◆ Size

uint Size
get

◆ this[uint i]

AST this[uint i]
getset

Retrieves the i-th object in the vector.

May throw an IndexOutOfBoundsException when i is out of range.

Parameters
iIndex
Returns
An AST

Definition at line 44 of file ASTVector.cs.

45  {
46  get
47  {
48 
49  return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
50  }
51  set
52  {
53  Debug.Assert(value != null);
54 
55  Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
56  }
57  }