RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_a_s_t_vector.html below:

Z3: ASTVector Class Reference

Vectors of ASTs. More...

Vectors of ASTs.

Definition at line 28 of file ASTVector.cs.

◆ Push()

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

Parameters

Definition at line 73 of file ASTVector.cs.

75

Debug.Assert(a !=

null

);

77

Native.Z3_ast_vector_push(

Context

.nCtx, NativeObject, a.NativeObject);

Context Context

Access Context object

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

65

Native.Z3_ast_vector_resize(

Context

.nCtx, NativeObject, newSize);

◆ ToArithExprArray()

Translates an ASTVector into a ArithExpr[]

Definition at line 151 of file ASTVector.cs.

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

uint Size

The size of the vector

◆ ToArray()

Translates an AST vector into an AST[]

Definition at line 103 of file ASTVector.cs.

106

AST[] res =

new

AST[n];

107 for

(uint i = 0; i < n; i++)

108

res[i] = AST.Create(

this

.Context,

this

[i].NativeObject);

◆ ToArrayExprArray()

Translates an ASTVector into a ArrayExpr[]

Definition at line 163 of file ASTVector.cs.

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

◆ ToBitVecExprArray()

Translates an ASTVector into a BitVecExpr[]

Definition at line 139 of file ASTVector.cs.

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

◆ ToBoolExprArray() ◆ ToDatatypeExprArray()

Translates an ASTVector into a DatatypeExpr[]

Definition at line 175 of file ASTVector.cs.

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

◆ ToExprArray()

Translates an ASTVector into an Expr[]

Definition at line 115 of file ASTVector.cs.

118

Expr[] res =

new

Expr[n];

119 for

(uint i = 0; i < n; i++)

120

res[i] = Expr.Create(

this

.Context,

this

[i].NativeObject);

Referenced by Model.SortUniverse().

◆ ToFPExprArray()

Translates an ASTVector into a FPExpr[]

Definition at line 187 of file ASTVector.cs.

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

◆ ToFPRMExprArray()

Translates an ASTVector into a FPRMExpr[]

Definition at line 199 of file ASTVector.cs.

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

◆ ToIntExprArray()

Translates an ASTVector into a IntExpr[]

Definition at line 211 of file ASTVector.cs.

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

◆ ToRealExprArray()

Translates an ASTVector into a RealExpr[]

Definition at line 223 of file ASTVector.cs.

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

◆ ToString() override string ToString ( ) inline

Retrieves a string representation of the vector.

Definition at line 95 of file ASTVector.cs.

97 return

Native.Z3_ast_vector_to_string(

Context

.nCtx, NativeObject);

◆ Translate()

Translates all ASTs in the vector to ctx .

Parameters

Returns: A new ASTVector

Definition at line 85 of file ASTVector.cs.

87

Debug.Assert(ctx !=

null

);

89 return new

ASTVector(

Context

, Native.Z3_ast_vector_translate(

Context

.nCtx, NativeObject, ctx.nCtx));

◆ Size

The size of the vector

Definition at line 33 of file ASTVector.cs.

35 get

{

return

Native.Z3_ast_vector_size(

Context

.nCtx, NativeObject); }

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]

Retrieves the i-th object in the vector.

May throw an IndexOutOfBoundsException when i is out of range.

Parameters

Returns: An AST

Definition at line 44 of file ASTVector.cs.

49 return new

AST(

Context

, Native.Z3_ast_vector_get(

Context

.nCtx, NativeObject, i));

53

Debug.Assert(value !=

null

);

55

Native.Z3_ast_vector_set(

Context

.nCtx, NativeObject, i, value.NativeObject);

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4