ASTVector Class Reference

Vectors of ASTs. More...

Inheritance diagram for ASTVector:

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.
AST[]	ToArray ()
	Translates an AST vector into an AST[].
Expr[]	ToExprArray ()
	Translates an ASTVector into an Expr[].
BoolExpr[]	ToBoolExprArray ()
	Translates an ASTVector into a BoolExpr[].
BitVecExpr[]	ToBitVecExprArray ()
	Translates an ASTVector into a BitVecExpr[].
ArithExpr[]	ToArithExprArray ()
	Translates an ASTVector into a ArithExpr[].
ArrayExpr[]	ToArrayExprArray ()
	Translates an ASTVector into a ArrayExpr[].
DatatypeExpr[]	ToDatatypeExprArray ()
	Translates an ASTVector into a DatatypeExpr[].
FPExpr[]	ToFPExprArray ()
	Translates an ASTVector into a FPExpr[].
FPRMExpr[]	ToFPRMExprArray ()
	Translates an ASTVector into a FPRMExpr[].
IntExpr[]	ToIntExprArray ()
	Translates an ASTVector into a IntExpr[].
RealExpr[]	ToRealExprArray ()
	Translates an ASTVector into a RealExpr[].
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

Properties
uint	Size [get]
	The size of the vector.
AST	this[uint i] [get, set]
	Retrieves the i-th object in the vector.
Properties inherited from Z3Object
Context	Context [get]
	Access Context object.

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.

        {
            Debug.Assert(a != null);
 
            Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
        }

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.

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

ToArithExprArray()

ArithExpr[] ToArithExprArray ( )

inline

Translates an ASTVector into a ArithExpr[].

Definition at line 151 of file ASTVector.cs.

        {
            uint n = Size;
            ArithExpr[] res = new ArithExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToArray()

AST[] ToArray ( )

inline

Translates an AST vector into an AST[].

Definition at line 103 of file ASTVector.cs.

        {
            uint n = Size;
            AST[] res = new AST[n];
            for (uint i = 0; i < n; i++)
                res[i] = AST.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToArrayExprArray()

ArrayExpr[] ToArrayExprArray ( )

inline

Translates an ASTVector into a ArrayExpr[].

Definition at line 163 of file ASTVector.cs.

        {
            uint n = Size;
            ArrayExpr[] res = new ArrayExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToBitVecExprArray()

BitVecExpr[] ToBitVecExprArray ( )

inline

Translates an ASTVector into a BitVecExpr[].

Definition at line 139 of file ASTVector.cs.

        {
            uint n = Size;
            BitVecExpr[] res = new BitVecExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToBoolExprArray()

BoolExpr[] ToBoolExprArray ( )

inline

Translates an ASTVector into a BoolExpr[].

Definition at line 127 of file ASTVector.cs.

        {
            uint n = Size;
            BoolExpr[] res = new BoolExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToDatatypeExprArray()

DatatypeExpr[] ToDatatypeExprArray ( )

inline

Translates an ASTVector into a DatatypeExpr[].

Definition at line 175 of file ASTVector.cs.

        {
            uint n = Size;
            DatatypeExpr[] res = new DatatypeExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToExprArray()

Expr[] ToExprArray ( )

inline

Translates an ASTVector into an Expr[].

Definition at line 115 of file ASTVector.cs.

        {
            uint n = Size;
            Expr[] res = new Expr[n];
            for (uint i = 0; i < n; i++)
                res[i] = Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToFPExprArray()

FPExpr[] ToFPExprArray ( )

inline

Translates an ASTVector into a FPExpr[].

Definition at line 187 of file ASTVector.cs.

        {
            uint n = Size;
            FPExpr[] res = new FPExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToFPRMExprArray()

FPRMExpr[] ToFPRMExprArray ( )

inline

Translates an ASTVector into a FPRMExpr[].

Definition at line 199 of file ASTVector.cs.

        {
            uint n = Size;
            FPRMExpr[] res = new FPRMExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToIntExprArray()

IntExpr[] ToIntExprArray ( )

inline

Translates an ASTVector into a IntExpr[].

Definition at line 211 of file ASTVector.cs.

        {
            uint n = Size;
            IntExpr[] res = new IntExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToRealExprArray()

RealExpr[] ToRealExprArray ( )

inline

Translates an ASTVector into a RealExpr[].

Definition at line 223 of file ASTVector.cs.

        {
            uint n = Size;
            RealExpr[] res = new RealExpr[n];
            for (uint i = 0; i < n; i++)
                res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
            return res;
        }

ToString()

override string ToString ( )

inline

Retrieves a string representation of the vector.

Definition at line 95 of file ASTVector.cs.

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

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.

        {
            Debug.Assert(ctx != null);
 
            return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }

Property Documentation

Size

uint Size

get

The size of the vector.

Definition at line 33 of file ASTVector.cs.

        {
            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]

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

        {
            get
            {
 
                return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
            }
            set
            {
                Debug.Assert(value != null);
 
                Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
            }
        }