Package com.microsoft.z3

Class AST

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

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      int compareTo​(AST other)
      Object Comparison.
      boolean equals​(java.lang.Object o)
      Object comparison.
      Z3_ast_kind getASTKind()
      The kind of the AST.
      int getId()
      A unique identifier for the AST (unique among all ASTs).
      java.lang.String getSExpr()
      A string representation of the AST in s-expression notation.
      int hashCode()
      The AST's hash code.
      boolean isApp()
      Indicates whether the AST is an application
      boolean isExpr()
      Indicates whether the AST is an Expr
      boolean isFuncDecl()
      Indicates whether the AST is a FunctionDeclaration
      boolean isQuantifier()
      Indicates whether the AST is a Quantifier
      boolean isSort()
      Indicates whether the AST is a Sort
      boolean isVar()
      Indicates whether the AST is a BoundVariable.
      java.lang.String toString()
      A string representation of the AST.
      AST translate​(Context ctx)
      Translates (copies) the AST to the Context ctx.

      • Methods inherited from class java.lang.Object

        clone, finalize, getClass, notify, notifyAll, wait, wait, wait

    • Method Detail

      • equals

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

      • compareTo

        public int compareTo​(AST other)
        Object Comparison.
        Specified by:
        compareTo in interface java.lang.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 java.lang.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

      • 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 java.lang.String toString()
        A string representation of the AST.
        Overrides:
        toString in class java.lang.Object

      • getSExpr

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