Z3
Public Member Functions | Static Public Member Functions | Data Fields
Z3_ast_kind Enum Reference

Public Member Functions

 Z3_ast_kind (int v)
 
final int toInt ()
 

Static Public Member Functions

static final Z3_ast_kind fromInt (int v)
 

Data Fields

 Z3_VAR_AST =(2)
 
 Z3_SORT_AST =(4)
 
 Z3_QUANTIFIER_AST =(3)
 
 Z3_UNKNOWN_AST =(1000)
 
 Z3_FUNC_DECL_AST =(5)
 
 Z3_NUMERAL_AST =(0)
 
 Z3_APP_AST =(1)
 

Detailed Description

Z3_ast_kind

Definition at line 10 of file Z3_ast_kind.java.

Constructor & Destructor Documentation

Z3_ast_kind ( int  v)
inline

Definition at line 21 of file Z3_ast_kind.java.

21  {
22  this.intValue = v;
23  }

Member Function Documentation

static final Z3_ast_kind fromInt ( int  v)
inlinestatic

Definition at line 25 of file Z3_ast_kind.java.

Referenced by Expr.Expr(), AST.getASTKind(), and AST.getSExpr().

25  {
26  for (Z3_ast_kind k: values())
27  if (k.intValue == v) return k;
28  return values()[0];
29  }
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
final int toInt ( )
inline

Definition at line 31 of file Z3_ast_kind.java.

31 { return this.intValue; }

Field Documentation

Z3_APP_AST =(1)

Definition at line 17 of file Z3_ast_kind.java.

Referenced by AST.isApp().

Z3_FUNC_DECL_AST =(5)

Definition at line 15 of file Z3_ast_kind.java.

Referenced by FuncDecl.Parameter.getParameterKind(), and AST.isFuncDecl().

Z3_NUMERAL_AST =(0)

Definition at line 16 of file Z3_ast_kind.java.

Z3_QUANTIFIER_AST =(3)

Definition at line 13 of file Z3_ast_kind.java.

Referenced by Expr.Expr(), Quantifier.getBody(), and AST.isQuantifier().

Z3_SORT_AST =(4)

Definition at line 12 of file Z3_ast_kind.java.

Referenced by AST.isSort(), and Sort.toString().

Z3_UNKNOWN_AST =(1000)

Definition at line 14 of file Z3_ast_kind.java.

Z3_VAR_AST =(2)

Definition at line 11 of file Z3_ast_kind.java.

Referenced by Expr.Expr(), and AST.isVar().