Z3_ast_kind class abstract

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

  • Z3_APP_AST: constant and applications
  • Z3_NUMERAL_AST: numeral constants
  • Z3_VAR_AST: bound variables
  • Z3_QUANTIFIER_AST: quantifiers
  • Z3_SORT_AST: sort
  • Z3_FUNC_DECL_AST: function declaration
  • Z3_UNKNOWN_AST: internal

Constructors

Z3_ast_kind()

Properties

hashCode int
The hash code for this object.
no setterinherited
runtimeType Type
A representation of the runtime type of the object.
no setterinherited

Methods

noSuchMethod(Invocation invocation) → dynamic
Invoked when a nonexistent method or property is accessed.
inherited
toString() String
A string representation of this object.
inherited

Operators

operator ==(Object other) bool
The equality operator.
inherited

Constants

APP_AST → const int
FUNC_DECL_AST → const int
NUMERAL_AST → const int
QUANTIFIER_AST → const int
SORT_AST → const int
UNKNOWN_AST → const int
VAR_AST → const int