Package com.microsoft.z3

Class ASTVector

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.ASTVector
public class ASTVector extends Z3Object
Vectors of ASTs.

  • Constructor Details

    • ASTVector

      public ASTVector(Context ctx, long obj)

    • ASTVector

      public ASTVector(Context ctx)

  • Method Details

    • size

      public int size()
      The size of the vector

    • get

      public AST get(int i)
      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
      Throws:
      Z3Exception

    • set

      public void set(int i, AST value)

    • resize

      public void resize(int newSize)
      Resize the vector to newSize.
      Parameters:
      newSize - The new size of the vector.

    • push

      public void push(AST a)
      Add the AST a to the back of the vector. The size is increased by 1.
      Parameters:
      a - An AST

    • translate

      public ASTVector translate(Context ctx)
      Translates all ASTs in the vector to ctx.
      Parameters:
      ctx - A context
      Returns:
      A new ASTVector
      Throws:
      Z3Exception

    • toString

      public String toString()
      Retrieves a string representation of the vector.
      Overrides:
      toString in class Object

    • ToArray

      public AST[] ToArray()
      Translates the AST vector into an AST[]

    • ToExprArray

      public Expr<?>[] ToExprArray()
      Translates the AST vector into an Expr[]

    • ToBoolExprArray

      public BoolExpr[] ToBoolExprArray()
      Translates the AST vector into an BoolExpr[]

    • ToBitVecExprArray

      public BitVecExpr[] ToBitVecExprArray()
      Translates the AST vector into an BitVecExpr[]

    • ToArithExprExprArray

      public ArithExpr<?>[] ToArithExprExprArray()
      Translates the AST vector into an ArithExpr[]

    • ToArrayExprArray

      public ArrayExpr<?,?>[] ToArrayExprArray()
      Translates the AST vector into an ArrayExpr[]

    • ToDatatypeExprArray

      public DatatypeExpr<?>[] ToDatatypeExprArray()
      Translates the AST vector into an DatatypeExpr[]

    • ToFPExprArray

      public FPExpr[] ToFPExprArray()
      Translates the AST vector into an FPExpr[]

    • ToFPRMExprArray

      public FPRMExpr[] ToFPRMExprArray()
      Translates the AST vector into an FPRMExpr[]

    • ToIntExprArray

      public IntExpr[] ToIntExprArray()
      Translates the AST vector into an IntExpr[]

    • ToRealExprArray

      public RealExpr[] ToRealExprArray()
      Translates the AST vector into an RealExpr[]