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 |
Package Functions | |
AST (Context ctx) | |
AST (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
Static Package Functions | |
static AST | create (Context ctx, long obj) throws Z3Exception |
Definition at line 203 of file AST.java.
Referenced by FuncDecl.getParameters(), and AST.translate().
{ super(ctx); }
AST | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
int compareTo | ( | Object | other | ) | throws Z3Exception [inline] |
Object Comparison.
other | Another AST |
static AST create | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, static, package] |
Reimplemented in Expr, and Sort.
Definition at line 235 of file AST.java.
Referenced by Context.wrapAST().
{ switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj))) { case Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj); case Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); case Z3_SORT_AST: return Sort.create(ctx, obj); case Z3_APP_AST: case Z3_NUMERAL_AST: case Z3_VAR_AST: return Expr.create(ctx, obj); default: throw new Z3Exception("Unknown AST kind"); } }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 224 of file AST.java.
{ // Console.WriteLine("AST DecRef()"); if (getContext() == null) throw new Z3Exception("dec() called on null context"); if (o == 0) throw new Z3Exception("dec() called on null AST"); getContext().ast_DRQ().add(o); super.decRef(o); }
boolean equals | ( | Object | o | ) | [inline] |
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().
{ return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(), getNativeObject())); }
int getId | ( | ) | throws Z3Exception [inline] |
A unique identifier for the AST (unique among all ASTs).
Reimplemented in FuncDecl, and Sort.
Definition at line 94 of file AST.java.
Referenced by AST.compareTo().
{ return Native.getAstId(getContext().nCtx(), getNativeObject()); }
String getSExpr | ( | ) | throws Z3Exception [inline] |
A string representation of the AST in s-expression notation.
Definition at line 198 of file AST.java.
{ return Native.astToString(getContext().nCtx(), getNativeObject()); }
int hashCode | ( | ) | [inline] |
The AST's hash code.
Reimplemented in FuncDecl, and Sort.
Definition at line 81 of file AST.java.
{ int r = 0; try { Native.getAstHash(getContext().nCtx(), getNativeObject()); } catch (Z3Exception ex) {} return r; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 213 of file AST.java.
{ // Console.WriteLine("AST IncRef()"); if (getContext() == null) throw new Z3Exception("inc() called on null context"); if (o == 0) throw new Z3Exception("inc() called on null AST"); getContext().ast_DRQ().incAndClear(getContext(), o); super.incRef(o); }
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.IsBVSDiv0(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.IsBVSMod0(), Expr.isBVSRem(), Expr.IsBVSRem0(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.IsBVUDiv0(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.IsBVURem0(), 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().
{ return this.getASTKind() == Z3_ast_kind.Z3_APP_AST; }
boolean isExpr | ( | ) | throws Z3Exception [inline] |
Indicates whether the AST is an Expr
Definition at line 127 of file AST.java.
Referenced by Expr.isBool().
{ switch (getASTKind()) { case Z3_APP_AST: case Z3_NUMERAL_AST: case Z3_QUANTIFIER_AST: case Z3_VAR_AST: return true; default: return false; } }
boolean isFuncDecl | ( | ) | throws Z3Exception [inline] |
Indicates whether the AST is a FunctionDeclaration
Definition at line 176 of file AST.java.
{ return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST; }
boolean isQuantifier | ( | ) | throws Z3Exception [inline] |
Indicates whether the AST is a Quantifier
Definition at line 160 of file AST.java.
{ return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST; }
boolean isSort | ( | ) | throws Z3Exception [inline] |
Indicates whether the AST is a Sort
Definition at line 168 of file AST.java.
{ return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST; }
boolean isVar | ( | ) | throws Z3Exception [inline] |
Indicates whether the AST is a BoundVariable
Definition at line 152 of file AST.java.
Referenced by Expr.getIndex().
{ return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST; }
String toString | ( | ) | [inline] |
A string representation of the AST.
Reimplemented in Expr, Sort, RatNum, FuncDecl, IntNum, BitVecNum, and Pattern.
Definition at line 184 of file AST.java.
{ try { return Native.astToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }
AST translate | ( | Context | ctx | ) | throws Z3Exception [inline] |
Translates (copies) the AST to the Context ctx .
ctx | A context |
Reimplemented in Expr.
Definition at line 105 of file AST.java.
{ if (getContext() == ctx) return this; else return new AST(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx())); }