ASTVector Class Reference

Vectors of ASTs. More...

Inheritance diagram for ASTVector:

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...
AST []	ToArray ()
	Translates an AST vector into an AST[] More...
Expr []	ToExprArray ()
	Translates an ASTVector into an Expr[] More...
BoolExpr []	ToBoolExprArray ()
	Translates an ASTVector into a BoolExpr[] More...
BitVecExpr []	ToBitVecExprArray ()
	Translates an ASTVector into a BitVecExpr[] More...
ArithExpr []	ToArithExprArray ()
	Translates an ASTVector into a ArithExpr[] More...
ArrayExpr []	ToArrayExprArray ()
	Translates an ASTVector into a ArrayExpr[] More...
DatatypeExpr []	ToDatatypeExprArray ()
	Translates an ASTVector into a DatatypeExpr[] More...
FPExpr []	ToFPExprArray ()
	Translates an ASTVector into a FPExpr[] More...
FPRMExpr []	ToFPRMExprArray ()
	Translates an ASTVector into a FPRMExpr[] More...
IntExpr []	ToIntExprArray ()
	Translates an ASTVector into a IntExpr[] More...
RealExpr []	ToRealExprArray ()
	Translates an ASTVector into a RealExpr[] 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

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

        {
            Contract.Requires(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 64 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 153 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 105 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 165 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 141 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 129 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;
        }

Referenced by InterpolationContext.ComputeInterpolant(), InterpolationContext.GetInterpolant(), Fixedpoint.ParseFile(), and Fixedpoint.ParseString().

ToDatatypeExprArray()

DatatypeExpr [] ToDatatypeExprArray ( )

inline

Translates an ASTVector into a DatatypeExpr[]

Definition at line 177 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 117 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;
        }

Referenced by Model.SortUniverse().

ToFPExprArray()

FPExpr [] ToFPExprArray ( )

inline

Translates an ASTVector into a FPExpr[]

Definition at line 189 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 201 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 213 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 225 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 97 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 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

Size

uint Size

get

The size of the vector

Definition at line 34 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 45 of file ASTVector.cs.

        {
            get
            {
                Contract.Ensures(Contract.Result<AST>() != null);

                return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
            }
            set
            {
                Contract.Requires(value != null);

                Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
            }
        }