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 |
Vectors of ASTs.
Definition at line 23 of file ASTVector.java.
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())); }
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.
i | Index |
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.
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 .
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 .
ctx | A context |
Z3Exception |
Definition at line 79 of file ASTVector.java.
{ return new ASTVector(getContext(), Native.astVectorTranslate(getContext() .nCtx(), getNativeObject(), ctx.nCtx())); }