Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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 .
void Push (AST a)
 Add the AST a to the back of the vector. The size is increased by 1.
ASTVector Translate (Context ctx)
 Translates all ASTs in the vector to ctx .
override string ToString ()
 Retrieves a string representation of the vector.

Properties

uint Size [get]
 The size of the vector.
AST this[uint i] [get, set]
 Retrieves the i-th object in the vector.

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.

        {
            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:
newSizeThe 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:
ctxA 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 Model.SortUniverse().

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:
iIndex
Returns:
An AST

Definition at line 45 of file ASTVector.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines