Z3 |

Public Member Functions
AST Class Reference
Inheritance diagram for AST:

## Public Member Functions
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

The abstract syntax tree (AST) class.

Definition at line 25 of file AST.java.

## Member Function Documentation

## ◆ compareTo()

int compareTo | ( | AST | other | ) |
| inline

Object Comparison.

Parameters

  other | Another AST

Returns
  Negative if the object should be sorted before `other`, positive if after else zero.

Exceptions

  Z3Exception | on error

Definition at line 53 of file AST.java.

54 {
55 if (other == null) {
56 return 1;
57 }
58 return Integer.compare(getId(), other.getId());
59 }
com.microsoft.z3.AST.getId
int getId()
Definition: AST.java:76

## ◆ equals()

boolean equals | ( | Object | o | ) |
| inline

Object comparison.

Parameters

  o | another AST

Reimplemented in FuncDecl< R extends Sort >, and Sort.

Definition at line 33 of file AST.java.

34 {
35 if (o == this) return true;
36 if (!(o instanceof AST)) return false;
37 AST casted = (AST) o;
38
39 return
40 (getContext().nCtx() == casted.getContext().nCtx()) &&
41 (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
42 }
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008

## ◆ getASTKind()

Z3_ast_kind getASTKind | ( |  | ) |
| inline

The kind of the AST.

Exceptions

  Z3Exception | on error

Definition at line 101 of file AST.java.

102 {
103 return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
104 getNativeObject()));
105 }
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180

Referenced by AST.isApp(), AST.isExpr(), AST.isFuncDecl(), AST.isQuantifier(), AST.isSort(), and AST.isVar().

## ◆ getId()

int getId | ( |  | ) |
| inline

A unique identifier for the AST (unique among all ASTs).

Exceptions

  Z3Exception | on error

Reimplemented in FuncDecl< R extends Sort >, and Sort.

Definition at line 76 of file AST.java.

77 {
78 return Native.getAstId(getContext().nCtx(), getNativeObject());
79 }

Referenced by AST.compareTo().

## ◆ getSExpr()

String getSExpr | ( |  | ) |
| inline

A string representation of the AST in s-expression notation.

Definition at line 183 of file AST.java.

184 {
185 return Native.astToString(getContext().nCtx(), getNativeObject());
186 }

## ◆ hashCode()

int hashCode | ( |  | ) |
| inline

The AST's hash code.

Returns
  A hash code

Reimplemented in Sort.

Definition at line 67 of file AST.java.

68 {
69 return Native.getAstHash(getContext().nCtx(), getNativeObject());
70 }

## ◆ isApp()

boolean isApp | ( |  | ) |
| inline

Indicates whether the AST is an application

Returns
  a boolean

Exceptions

  Z3Exception | on error

Definition at line 131 of file AST.java.

132 {
133 return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
134 }
com.microsoft.z3.AST.getASTKind
Z3_ast_kind getASTKind()
Definition: AST.java:101

## ◆ isExpr()

boolean isExpr | ( |  | ) |
| inline

Indicates whether the AST is an Expr

Exceptions

  Z3Exception | on error
  Z3Exception | on error

Definition at line 112 of file AST.java.

113 {
114 switch (getASTKind())
115 {
116 case Z3_APP_AST:
117 case Z3_NUMERAL_AST:
118 case Z3_QUANTIFIER_AST:
119 case Z3_VAR_AST:
120 return true;
121 default:
122 return false;
123 }
124 }
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:182
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:183
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:181
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184

## ◆ isFuncDecl()

boolean isFuncDecl | ( |  | ) |
| inline

Indicates whether the AST is a FunctionDeclaration

Definition at line 167 of file AST.java.

168 {
169 return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
170 }

## ◆ isQuantifier()

boolean isQuantifier | ( |  | ) |
| inline

Indicates whether the AST is a Quantifier

Returns
  a boolean

Exceptions

  Z3Exception | on error

Definition at line 151 of file AST.java.

152 {
153 return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
154 }

## ◆ isSort()

boolean isSort | ( |  | ) |
| inline

Indicates whether the AST is a Sort

Definition at line 159 of file AST.java.

160 {
161 return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
162 }

## ◆ isVar()

boolean isVar | ( |  | ) |
| inline

Indicates whether the AST is a BoundVariable.

Returns
  a boolean

Exceptions

  Z3Exception | on error

Definition at line 141 of file AST.java.

142 {
143 return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
144 }

## ◆ toString()

String toString | ( |  | ) |
| inline

A string representation of the AST.

Reimplemented in Expr< R extends Sort >, FuncDecl< R extends Sort >, Pattern, and Sort.

Definition at line 176 of file AST.java.

176 {
177 return Native.astToString(getContext().nCtx(), getNativeObject());
178 }

## ◆ translate()

AST translate | ( | Context | ctx | ) |
| inline

Translates (copies) the AST to the Context `ctx`.

Parameters

  ctx | A context

Returns
  A copy of the AST which is associated with `ctx`

Exceptions

  Z3Exception | on error

Reimplemented in Expr< R extends Sort >, FuncDecl< R extends Sort >, and Sort.

Definition at line 88 of file AST.java.

89 {
90 if (getContext() == ctx) {
91 return this;
92 } else {
93 return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
94 }
95 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().