Z3
Public Member Functions
AST Class Reference
+ Inheritance diagram for AST:

Public Member Functions

boolean equals (Object o)
 
int compareTo (Object 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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

The abstract syntax tree (AST) class.

Definition at line 25 of file AST.java.

Member Function Documentation

int compareTo ( Object  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 60 of file AST.java.

61  {
62  if (other == null)
63  return 1;
64 
65  AST oAST = null;
66  try
67  {
68  oAST = AST.class.cast(other);
69  } catch (ClassCastException e)
70  {
71  return 1;
72  }
73 
74  if (getId() < oAST.getId())
75  return -1;
76  else if (getId() > oAST.getId())
77  return +1;
78  else
79  return 0;
80  }
boolean equals ( Object  o)
inline

Object comparison.

Parameters
oanother AST

Definition at line 32 of file AST.java.

33  {
34  AST casted = null;
35 
36  try
37  {
38  casted = AST.class.cast(o);
39  } catch (ClassCastException e)
40  {
41  return false;
42  }
43 
44  return
45  (this == casted) ||
46  (this != null) &&
47  (casted != null) &&
48  (getContext().nCtx() == casted.getContext().nCtx()) &&
49  (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
50 }
Z3_ast_kind getASTKind ( )
inline

The kind of the AST.

Exceptions
Z3Exceptionon error

Definition at line 127 of file AST.java.

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

128  {
129  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
130  getNativeObject()));
131  }
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
int getId ( )
inline

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

Exceptions
Z3Exceptionon error

Definition at line 101 of file AST.java.

Referenced by AST.compareTo().

102  {
103  return Native.getAstId(getContext().nCtx(), getNativeObject());
104  }
String getSExpr ( )
inline

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

Definition at line 215 of file AST.java.

216  {
217  return Native.astToString(getContext().nCtx(), getNativeObject());
218  }
int hashCode ( )
inline

The AST's hash code.

Returns
A hash code

Definition at line 87 of file AST.java.

88  {
89  int r = 0;
90  try {
91  Native.getAstHash(getContext().nCtx(), getNativeObject());
92  }
93  catch (Z3Exception ex) {}
94  return r;
95  }
boolean isApp ( )
inline

Indicates whether the AST is an application

Returns
a boolean
Exceptions
Z3Exceptionon error

Definition at line 157 of file AST.java.

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.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.isProofCNFStar(), 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.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), 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.isSub(), Expr.isTrue(), Expr.isUMinus(), Expr.isXor(), and Expr.update().

158  {
159  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
160  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
boolean isExpr ( )
inline

Indicates whether the AST is an Expr

Exceptions
Z3Exceptionon error
Z3Exceptionon error

Definition at line 138 of file AST.java.

Referenced by Expr.isBool().

139  {
140  switch (getASTKind())
141  {
142  case Z3_APP_AST:
143  case Z3_NUMERAL_AST:
144  case Z3_QUANTIFIER_AST:
145  case Z3_VAR_AST:
146  return true;
147  default:
148  return false;
149  }
150  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
boolean isFuncDecl ( )
inline

Indicates whether the AST is a FunctionDeclaration

Definition at line 193 of file AST.java.

194  {
195  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
196  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
boolean isQuantifier ( )
inline

Indicates whether the AST is a Quantifier

Returns
a boolean
Exceptions
Z3Exceptionon error

Definition at line 177 of file AST.java.

178  {
179  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
180  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
boolean isSort ( )
inline

Indicates whether the AST is a Sort

Definition at line 185 of file AST.java.

186  {
187  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
188  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
boolean isVar ( )
inline

Indicates whether the AST is a BoundVariable.

Returns
a boolean
Exceptions
Z3Exceptionon error

Definition at line 167 of file AST.java.

Referenced by Expr.getIndex().

168  {
169  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
170  }
Z3_ast_kind getASTKind()
Definition: AST.java:127
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
String toString ( )
inline

A string representation of the AST.

Definition at line 201 of file AST.java.

202  {
203  try
204  {
205  return Native.astToString(getContext().nCtx(), getNativeObject());
206  } catch (Z3Exception e)
207  {
208  return "Z3Exception: " + e.getMessage();
209  }
210  }
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

Definition at line 113 of file AST.java.

114  {
115 
116  if (getContext() == ctx)
117  return this;
118  else
119  return new AST(ctx, Native.translate(getContext().nCtx(),
120  getNativeObject(), ctx.nCtx()));
121  }