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

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object 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 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;
         }

Referenced by Solver.Cube(), Fixedpoint.ParseFile(), Context.ParseSMTLIB2File(), Context.ParseSMTLIB2String(), and Fixedpoint.ParseString().

◆ 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;
         }

Referenced by Model.SortUniverse().

◆ 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);
             }
         }

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Push()

◆ Resize()

◆ ToArithExprArray()

◆ ToArray()

◆ ToArrayExprArray()

◆ ToBitVecExprArray()

◆ ToBoolExprArray()

◆ ToDatatypeExprArray()

◆ ToExprArray()

◆ ToFPExprArray()

◆ ToFPRMExprArray()

◆ ToIntExprArray()

◆ ToRealExprArray()

◆ ToString()

◆ Translate()

Property Documentation

◆ Size

◆ this[uint i]