Module z3::ast

source ·
Expand description

Abstract syntax tree (AST).

Structs

  • Array
    Ast node representing an array value. An array in Z3 is a mapping from indices to values.
  • BV
    Ast node representing a bitvector value.
  • Bool
    Ast node representing a boolean value.
  • Datatype
    Ast node representing a datatype or enumeration value.
  • Dynamic
    A dynamically typed Ast node.
  • Float
    Ast node representing a float value.
  • Int
    Ast node representing an integer value.
  • Real
    Ast node representing a real value.
  • Regexp
    Ast node representing a regular expression.
  • Set
    Ast node representing a set value.
  • String
    Ast node representing a string value.

Enums

  • AstKind
    The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Traits

  • Ast
    Abstract syntax tree (AST) nodes represent terms, constants, or expressions. The Ast trait contains methods common to all AST subtypes.

Functions