Z3 |

Data Structures | Public Member Functions | Properties
ASTVector Class Reference

Vectors of ASTs. More...

Inheritance diagram for ASTVector:

## Data Structures
class | DecRefQueue

## 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...

## 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

  a | An 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 }

## ◆ Resize()

void Resize | ( | uint | newSize | ) |
| inline

Resize the vector to newSize .

Parameters

  newSize | The 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 }
Microsoft.Z3.ASTVector.Size
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

  ctx | A 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

The size of the vector

Definition at line 33 of file ASTVector.cs.

34 {
35 get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); }
36 }

Referenced by ASTVector.ToArithExprArray(), ASTVector.ToArray(), ASTVector.ToArrayExprArray(), ASTVector.ToBitVecExprArray(), ASTVector.ToBoolExprArray(), ASTVector.ToDatatypeExprArray(), ASTVector.ToExprArray(), ASTVector.ToFPExprArray(), ASTVector.ToFPRMExprArray(), ASTVector.ToIntExprArray(), and ASTVector.ToRealExprArray().

## ◆ this[uint i]

AST this[uint i]
| get set

Retrieves the i-th object in the vector.

May throw an IndexOutOfBoundsException when i is out of range.

Parameters

  i | Index

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 }