Inheritance diagram for ASTVector:

Public Member Functions
int	size ()

AST	get (int i)

void	set (int i, AST value)

void	resize (int newSize)

void	push (AST a)

ASTVector	translate (Context ctx)

String	toString ()

	ASTVector (Context ctx, long obj)

	ASTVector (Context ctx)

AST[]	ToArray ()

Expr<?>[]	ToExprArray ()

BoolExpr[]	ToBoolExprArray ()

BitVecExpr[]	ToBitVecExprArray ()

ArithExpr<?>[]	ToArithExprExprArray ()

ArrayExpr<?, ?>[]	ToArrayExprArray ()

DatatypeExpr<?>[]	ToDatatypeExprArray ()

FPExpr[]	ToFPExprArray ()

FPRMExpr[]	ToFPRMExprArray ()

IntExpr[]	ToIntExprArray ()

RealExpr[]	ToRealExprArray ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)

static int	arrayLength (Z3Object[] a)

Detailed Description

Vectors of ASTs.

Definition at line 25 of file ASTVector.java.

Constructor & Destructor Documentation

◆ ASTVector() [1/2]

ASTVector	(	Context	ctx,
		long	obj
	)

inline

Definition at line 96 of file ASTVector.java.

     {
         super(ctx, obj);
     }

Referenced by ASTVector.translate().

◆ ASTVector() [2/2]

ASTVector ( Context ctx )

inline

Definition at line 101 of file ASTVector.java.

     {
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }

Member Function Documentation

◆ get()

AST get ( int i )

inline

Retrieves the i-th object in the vector. Remarks: May throw an

IndexOutOfBoundsException

when

i

is out of range.

Parameters

i Index

Returns: An AST

Exceptions

Z3Exception

Definition at line 43 of file ASTVector.java.

     {
         return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
                 getNativeObject(), i));
     }

Referenced by Goal.__getitem__(), Goal.as_expr(), and Solver.getConsequences().

◆ 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 70 of file ASTVector.java.

     {
         Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
     }

Referenced by Solver.__enter__(), and Solver.getConsequences().

◆ resize()

void resize ( int newSize )

inline

Resize the vector to

newSize

.

Parameters

newSize The new size of the vector.

Definition at line 60 of file ASTVector.java.

     {
         Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
     }

◆ set()

void set	(	int	i,
		AST	value
	)

inline

Definition at line 49 of file ASTVector.java.

     {
  
         Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
                 value.getNativeObject());
     }

◆ size()

int size ( )

inline

The size of the vector

Definition at line 29 of file ASTVector.java.

     {
         return Native.astVectorSize(getContext().nCtx(), getNativeObject());
     }

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Solver.getConsequences(), Solver.getNumAssertions(), BitVecSortRef.subsort(), ASTVector.ToArithExprExprArray(), ASTVector.ToArray(), ASTVector.ToArrayExprArray(), ASTVector.ToBitVecExprArray(), ASTVector.ToBoolExprArray(), ASTVector.ToDatatypeExprArray(), ASTVector.ToExprArray(), ASTVector.ToFPExprArray(), ASTVector.ToFPRMExprArray(), ASTVector.ToIntExprArray(), and ASTVector.ToRealExprArray().

◆ ToArithExprExprArray()

ArithExpr<?> [] ToArithExprExprArray ( )

inline

Translates the AST vector into an ArithExpr[]

Definition at line 156 of file ASTVector.java.

     {
         int n = size();
         ArithExpr<?>[] res = new ArithExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (ArithExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToArray()

AST [] ToArray ( )

inline

Translates the AST vector into an AST[]

Definition at line 109 of file ASTVector.java.

     {
         int n = size();
         AST[] res = new AST[n];
         for (int i = 0; i < n; i++)
             res[i] = AST.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToArrayExprArray()

ArrayExpr<?, ?> [] ToArrayExprArray ( )

inline

Translates the AST vector into an ArrayExpr[]

Definition at line 168 of file ASTVector.java.

     {
         int n = size();
         ArrayExpr<?, ?>[] res = new ArrayExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (ArrayExpr<?, ?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToBitVecExprArray()

BitVecExpr [] ToBitVecExprArray ( )

inline

Translates the AST vector into an BitVecExpr[]

Definition at line 144 of file ASTVector.java.

     {
         int n = size();
         BitVecExpr[] res = new BitVecExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToBoolExprArray()

BoolExpr [] ToBoolExprArray ( )

inline

Translates the AST vector into an BoolExpr[]

Definition at line 132 of file ASTVector.java.

     {
         int n = size();
         BoolExpr[] res = new BoolExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

Referenced by Fixedpoint.getAssertions(), Optimize.getAssertions(), Solver.getAssertions(), Fixedpoint.getRules(), Optimize.getUnsatCore(), Solver.getUnsatCore(), Fixedpoint.ParseFile(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), and Fixedpoint.ParseString().

◆ ToDatatypeExprArray()

DatatypeExpr<?> [] ToDatatypeExprArray ( )

inline

Translates the AST vector into an DatatypeExpr[]

Definition at line 180 of file ASTVector.java.

     {
         int n = size();
         DatatypeExpr<?>[] res = new DatatypeExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (DatatypeExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToExprArray()

Expr<?> [] ToExprArray ( )

inline

Translates the AST vector into an Expr[]

Definition at line 121 of file ASTVector.java.

                                    {
         int n = size();
         Expr<?>[] res = new Expr[n];
         for (int i = 0; i < n; i++)
             res[i] = Expr.create(getContext(), get(i).getNativeObject());
         return res;    
     }

Referenced by Optimize.getObjectives().

◆ ToFPExprArray()

FPExpr [] ToFPExprArray ( )

inline

Translates the AST vector into an FPExpr[]

Definition at line 192 of file ASTVector.java.

     {
         int n = size();
         FPExpr[] res = new FPExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToFPRMExprArray()

FPRMExpr [] ToFPRMExprArray ( )

inline

Translates the AST vector into an FPRMExpr[]

Definition at line 204 of file ASTVector.java.

     {
         int n = size();
         FPRMExpr[] res = new FPRMExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToIntExprArray()

IntExpr [] ToIntExprArray ( )

inline

Translates the AST vector into an IntExpr[]

Definition at line 216 of file ASTVector.java.

     {
         int n = size();
         IntExpr[] res = new IntExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ ToRealExprArray()

RealExpr [] ToRealExprArray ( )

inline

Translates the AST vector into an RealExpr[]

Definition at line 228 of file ASTVector.java.

     {
         int n = size();
         RealExpr[] res = new RealExpr[n];
         for (int i = 0; i < n; i++)
             res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }

◆ toString()

String toString ( )

inline

Retrieves a string representation of the vector.

Definition at line 92 of file ASTVector.java.

                              {
         return Native.astVectorToString(getContext().nCtx(), getNativeObject());
     }

◆ translate()

ASTVector translate ( Context ctx )

inline

Translates all ASTs in the vector to

ctx

.

Parameters

ctx A context

Returns: A new ASTVector

Exceptions

Z3Exception

Definition at line 82 of file ASTVector.java.

     {
         return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
                 .nCtx(), getNativeObject(), ctx.nCtx()));
     }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ASTVector() [1/2]

◆ ASTVector() [2/2]

Member Function Documentation

◆ get()

◆ push()

◆ resize()

◆ set()

◆ size()

◆ ToArithExprExprArray()

◆ ToArray()

◆ ToArrayExprArray()

◆ ToBitVecExprArray()

◆ ToBoolExprArray()

◆ ToDatatypeExprArray()

◆ ToExprArray()

◆ ToFPExprArray()

◆ ToFPRMExprArray()

◆ ToIntExprArray()

◆ ToRealExprArray()

◆ toString()

◆ translate()