Z3
Public Member Functions
ASTVector Class Reference
+ 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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Vectors of ASTs.

Definition at line 23 of file ASTVector.java.

Member Function Documentation

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
iIndex
Returns
An AST
Exceptions
Z3Exception

Definition at line 42 of file ASTVector.java.

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

43  {
44  return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
45  getNativeObject(), i));
46  }
void push ( AST  a)
inline

Add the AST

a

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

Parameters
aAn AST

Definition at line 69 of file ASTVector.java.

70  {
71  Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
72  }
void resize ( int  newSize)
inline

Resize the vector to

newSize

.

Parameters
newSizeThe new size of the vector.

Definition at line 59 of file ASTVector.java.

60  {
61  Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
62  }
void set ( int  i,
AST  value 
)
inline

Definition at line 48 of file ASTVector.java.

49  {
50 
51  Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
52  value.getNativeObject());
53  }
int size ( )
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().

29  {
30  return Native.astVectorSize(getContext().nCtx(), getNativeObject());
31  }
String toString ( )
inline

Retrieves a string representation of the vector.

Definition at line 90 of file ASTVector.java.

91  {
92  try
93  {
94  return Native.astVectorToString(getContext().nCtx(), getNativeObject());
95  } catch (Z3Exception e)
96  {
97  return "Z3Exception: " + e.getMessage();
98  }
99  }
ASTVector translate ( Context  ctx)
inline

Translates all ASTs in the vector to

ctx

.

Parameters
ctxA context
Returns
A new ASTVector
Exceptions
Z3Exception

Definition at line 81 of file ASTVector.java.

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