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

Public Member Functions

boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

The abstract syntax tree (AST) class.

Definition at line 25 of file AST.java.

Member Function Documentation

int compareTo ( Object  other) throws Z3Exception
inline

Object Comparison.

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

Definition at line 54 of file AST.java.

55  {
56  if (other == null)
57  return 1;
58 
59  AST oAST = null;
60  try
61  {
62  oAST = AST.class.cast(other);
63  } catch (ClassCastException e)
64  {
65  return 1;
66  }
67 
68  if (getId() < oAST.getId())
69  return -1;
70  else if (getId() > oAST.getId())
71  return +1;
72  else
73  return 0;
74  }
boolean equals ( Object  o)
inline

Object comparison.

Parameters
oanother AST

Definition at line 33 of file AST.java.

34  {
35  AST casted = null;
36 
37  try
38  {
39  casted = AST.class.cast(o);
40  } catch (ClassCastException e)
41  {
42  return false;
43  }
44 
45  return this.getNativeObject() == casted.getNativeObject();
46  }
Z3_ast_kind getASTKind ( ) throws Z3Exception
inline

The kind of the AST.

Definition at line 118 of file AST.java.

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

119  {
120  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
121  getNativeObject()));
122  }
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
int getId ( ) throws Z3Exception
inline

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

Definition at line 94 of file AST.java.

Referenced by AST.compareTo().

95  {
96  return Native.getAstId(getContext().nCtx(), getNativeObject());
97  }
String getSExpr ( ) throws Z3Exception
inline

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

Definition at line 198 of file AST.java.

199  {
200  return Native.astToString(getContext().nCtx(), getNativeObject());
201  }
int hashCode ( )
inline

The AST's hash code.

Returns
A hash code

Definition at line 81 of file AST.java.

82  {
83  int r = 0;
84  try {
85  Native.getAstHash(getContext().nCtx(), getNativeObject());
86  }
87  catch (Z3Exception ex) {}
88  return r;
89  }
boolean isApp ( ) throws Z3Exception
inline

Indicates whether the AST is an application

Definition at line 144 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(), 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().

145  {
146  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
147  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isExpr ( ) throws Z3Exception
inline

Indicates whether the AST is an Expr

Definition at line 127 of file AST.java.

Referenced by Expr.isBool().

128  {
129  switch (getASTKind())
130  {
131  case Z3_APP_AST:
132  case Z3_NUMERAL_AST:
133  case Z3_QUANTIFIER_AST:
134  case Z3_VAR_AST:
135  return true;
136  default:
137  return false;
138  }
139  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
boolean isFuncDecl ( ) throws Z3Exception
inline

Indicates whether the AST is a FunctionDeclaration

Definition at line 176 of file AST.java.

177  {
178  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
179  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isQuantifier ( ) throws Z3Exception
inline

Indicates whether the AST is a Quantifier

Definition at line 160 of file AST.java.

161  {
162  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
163  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isSort ( ) throws Z3Exception
inline

Indicates whether the AST is a Sort

Definition at line 168 of file AST.java.

169  {
170  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
171  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isVar ( ) throws Z3Exception
inline

Indicates whether the AST is a BoundVariable

Definition at line 152 of file AST.java.

Referenced by Expr.getIndex().

153  {
154  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
155  }
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
String toString ( )
inline

A string representation of the AST.

Definition at line 184 of file AST.java.

185  {
186  try
187  {
188  return Native.astToString(getContext().nCtx(), getNativeObject());
189  } catch (Z3Exception e)
190  {
191  return "Z3Exception: " + e.getMessage();
192  }
193  }
AST translate ( Context  ctx) throws Z3Exception
inline

Translates (copies) the AST to the Context ctx .

Parameters
ctxA context
Returns
A copy of the AST which is associated with ctx

Definition at line 105 of file AST.java.

106  {
107 
108  if (getContext() == ctx)
109  return this;
110  else
111  return new AST(ctx, Native.translate(getContext().nCtx(),
112  getNativeObject(), ctx.nCtx()));
113  }