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

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

75  {
76  Contract.Requires(a != null);
77 
78  Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
79  }
void Resize ( uint  newSize)
inline

Resize the vector to newSize .

Parameters
newSizeThe new size of the vector.

Definition at line 64 of file ASTVector.cs.

65  {
66  Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
67  }
override string ToString ( )
inline

Retrieves a string representation of the vector.

Definition at line 97 of file ASTVector.cs.

98  {
99  return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
100  }
ASTVector Translate ( Context  ctx)
inline

Translates all ASTs in the vector to ctx .

Parameters
ctxA context
Returns
A new ASTVector

Definition at line 86 of file ASTVector.cs.

87  {
88  Contract.Requires(ctx != null);
89  Contract.Ensures(Contract.Result<ASTVector>() != null);
90 
91  return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
92  }

Property Documentation

uint Size
get

The size of the vector

Definition at line 34 of file ASTVector.cs.

Referenced by InterpolationContext.GetInterpolant(), and Model.SortUniverse().

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