Package com.microsoft.z3

Class AST

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.AST
All Implemented Interfaces:
Comparable<AST>
Direct Known Subclasses:
Expr, FuncDecl, Pattern, Sort
public class AST extends Z3Object implements Comparable<AST>
The abstract syntax tree (AST) class.

  • Method Details

    • equals

      public boolean equals(Object o)
      Object comparison.
      Overrides:
      equals in class Object
      Parameters:
      o - another AST

    • compareTo

      public int compareTo(AST other)
      Object Comparison.
      Specified by:
      compareTo in interface Comparable<AST>
      Parameters:
      other - Another AST
      Returns:
      Negative if the object should be sorted before other, positive if after else zero.
      Throws:
      Z3Exception - on error

    • hashCode

      public int hashCode()
      The AST's hash code.
      Overrides:
      hashCode in class Object
      Returns:
      A hash code

    • getId

      public int getId()
      A unique identifier for the AST (unique among all ASTs).
      Throws:
      Z3Exception - on error

    • translate

      public AST translate(Context ctx)
      Translates (copies) the AST to the Context ctx.
      Parameters:
      ctx - A context
      Returns:
      A copy of the AST which is associated with ctx
      Throws:
      Z3Exception - on error

    • getASTKind

      public Z3_ast_kind getASTKind()
      The kind of the AST.
      Throws:
      Z3Exception - on error

    • isExpr

      public boolean isExpr()
      Indicates whether the AST is an Expr
      Throws:
      Z3Exception - on error
      Z3Exception - on error

    • isApp

      public boolean isApp()
      Indicates whether the AST is an application
      Returns:
      a boolean
      Throws:
      Z3Exception - on error

    • isVar

      public boolean isVar()
      Indicates whether the AST is a BoundVariable.
      Returns:
      a boolean
      Throws:
      Z3Exception - on error

    • isQuantifier

      public boolean isQuantifier()
      Indicates whether the AST is a Quantifier
      Returns:
      a boolean
      Throws:
      Z3Exception - on error

    • isSort

      public boolean isSort()
      Indicates whether the AST is a Sort

    • isFuncDecl

      public boolean isFuncDecl()
      Indicates whether the AST is a FunctionDeclaration

    • toString

      public String toString()
      A string representation of the AST.
      Overrides:
      toString in class Object

    • getSExpr

      public String getSExpr()
      A string representation of the AST in s-expression notation.