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

a

An AST

Definition at line 74 of file ASTVector.cs.

        {
            Contract.Requires(a != null);

            Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
        }

void Resize ( uint  newSize )

inline

Resize the vector to newSize .

Parameters

newSize

The new size of the vector.

Definition at line 64 of file ASTVector.cs.

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

override string ToString ( )

inline

Retrieves a string representation of the vector.

Definition at line 97 of file ASTVector.cs.

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

ASTVector Translate ( Context  ctx )

inline

Translates all ASTs in the vector to ctx .

Parameters

ctx

A context

Returns

A new ASTVector

Definition at line 86 of file ASTVector.cs.

        {
            Contract.Requires(ctx != null);
            Contract.Ensures(Contract.Result<ASTVector>() != null);

            return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }

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

i

Index

Returns

An AST

Definition at line 45 of file ASTVector.cs.