Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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:
iIndex
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:
aAn 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:
newSizeThe 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]
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:
ctxA 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()));
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines