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.

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  }

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.

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  }

Referenced by Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.isBVSRem(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConcat(), Expr.isConst(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), FPRMNum.isRNA(), FPRMNum.isRNE(), FPRMNum.isRoundNearestTiesToAway(), FPRMNum.isRoundNearestTiesToEven(), FPRMNum.isRoundTowardNegative(), FPRMNum.isRoundTowardPositive(), FPRMNum.isRoundTowardZero(), FPRMNum.isRTN(), FPRMNum.isRTP(), FPRMNum.isRTZ(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isString(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), Expr.isXor(), and Expr.update().

◆ 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  }

Referenced by Expr.isBool().

◆ 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  }

Referenced by Expr.getIndex().

◆ toString()

String toString ( )
inline

A string representation of the AST.

Reimplemented in Sort, RatNum, Pattern, IntNum, FuncDecl, FPNum, FiniteDomainNum, Expr, and BitVecNum.

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, Quantifier, Lambda, FuncDecl, and Expr.

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  }
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_FUNC_DECL_AST
Z3_FUNC_DECL_AST
Definition: Z3_ast_kind.java:19
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_VAR_AST
Z3_VAR_AST
Definition: Z3_ast_kind.java:16
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_QUANTIFIER_AST
Z3_QUANTIFIER_AST
Definition: Z3_ast_kind.java:17
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:180
com.microsoft.z3.AST.getASTKind
Z3_ast_kind getASTKind()
Definition: AST.java:101
com.microsoft.z3.AST.getId
int getId()
Definition: AST.java:76
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_APP_AST
Z3_APP_AST
Definition: Z3_ast_kind.java:15
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_SORT_AST
Z3_SORT_AST
Definition: Z3_ast_kind.java:18
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:181
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:179
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:178
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:182