ASTVector Class Reference

Inheritance diagram for ASTVector:

Public Member Functions
int	size () throws Z3Exception
AST	get (int i) throws Z3Exception
void	set (int i, AST value) throws Z3Exception
void	resize (int newSize) throws Z3Exception
void	push (AST a) throws Z3Exception
ASTVector	translate (Context ctx) throws Z3Exception
String	toString ()
Package Functions
	ASTVector (Context ctx, long obj) throws Z3Exception
	ASTVector (Context ctx) throws Z3Exception
void	incRef (long o) throws Z3Exception
void	decRef (long o) throws Z3Exception

---

Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

---

Constructor & Destructor Documentation

ASTVector	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 99 of file ASTVector.java.

Referenced by ASTVector.translate().

    {
        super(ctx, obj);
    }

ASTVector

(

Context

ctx

)

throws Z3Exception [inline, package]

Definition at line 104 of file ASTVector.java.

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

---

Member Function Documentation

void decRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 115 of file ASTVector.java.

    {
        getContext().astvector_DRQ().add(o);
        super.decRef(o);
    }

AST get

(

int

i

)

throws Z3Exception [inline]

Retrieves the i-th object in the vector. May throw an IndexOutOfBoundsException when i is out of range.

Parameters:

i

Index

Returns:

An AST

Exceptions:

Z3Exception

Definition at line 41 of file ASTVector.java.

Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), InterpolationContext.GetInterpolant(), Fixedpoint.getRules(), Model.getSortUniverse(), and Solver.getUnsatCore().

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

void incRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 109 of file ASTVector.java.

    {
        getContext().astvector_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

void push

(

AST

a

)

throws Z3Exception [inline]

Add the AST a to the back of the vector. The size is increased by 1.

Parameters:

a

An AST

Definition at line 67 of file ASTVector.java.

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

void resize

(

int

newSize

)

throws Z3Exception [inline]

Resize the vector to newSize .

Parameters:

newSize

The new size of the vector.

Definition at line 58 of file ASTVector.java.

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

void set	(	int	i,
		AST	value
	)		throws Z3Exception [inline]

Definition at line 47 of file ASTVector.java.

    {

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

int size

(

)

throws Z3Exception [inline]

The size of the vector

Definition at line 28 of file ASTVector.java.

Referenced by Solver.getAssertions(), Fixedpoint.getAssertions(), InterpolationContext.GetInterpolant(), Solver.getNumAssertions(), Fixedpoint.getRules(), Model.getSortUniverse(), and Solver.getUnsatCore().

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

String toString

(

)

[inline]

Retrieves a string representation of the vector.

Definition at line 88 of file ASTVector.java.

    {
        try
        {
            return Native.astVectorToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

ASTVector translate

(

Context

ctx

)

throws Z3Exception [inline]

Translates all ASTs in the vector to ctx .

Parameters:

ctx

A context

Returns:

A new ASTVector

Exceptions:

Z3Exception

Definition at line 79 of file ASTVector.java.

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