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
otherAnother AST
Returns
Negative if the object should be sorted before
other
, positive if after else zero.
Exceptions
Z3Exceptionon 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  }

◆ equals()

boolean equals ( Object  o)
inline

Object comparison.

Parameters
oanother AST

Reimplemented in Sort, and FuncDecl< R extends 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  }

◆ getASTKind()

Z3_ast_kind getASTKind ( )
inline

The kind of the AST.

Exceptions
Z3Exceptionon 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
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:139

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
Z3Exceptionon error

Reimplemented in Sort, and FuncDecl< R extends 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
Z3Exceptionon error

Definition at line 131 of file AST.java.

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

◆ isExpr()

boolean isExpr ( )
inline

Indicates whether the AST is an Expr

Exceptions
Z3Exceptionon error
Z3Exceptionon 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
Definition: z3_api.h:141
@ Z3_VAR_AST
Definition: z3_api.h:142
@ Z3_NUMERAL_AST
Definition: z3_api.h:140
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:143

◆ 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
Z3Exceptionon 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
Z3Exceptionon 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 Sort, Pattern, FuncDecl< R extends Sort >, and Expr< R extends 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
ctxA context
Returns
A copy of the AST which is associated with
ctx
Exceptions
Z3Exceptionon error

Reimplemented in Sort, FuncDecl< R extends Sort >, and Expr< R extends 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__().