Data Structures | |
class | Parameter |
Public Member Functions | |
boolean | equals (Object o) |
String | toString () |
int | getId () |
int | getArity () |
int | getDomainSize () |
Sort [] | getDomain () |
Sort | getRange () |
Z3_decl_kind | getDeclKind () |
Symbol | getName () |
int | getNumParameters () |
Parameter [] | getParameters () |
Expr | apply (Expr ... args) |
![]() | |
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 () |
Function declarations.
Definition at line 27 of file FuncDecl.java.
Create expression that applies function to arguments.
Definition at line 356 of file FuncDecl.java.
Referenced by Tactic.__call__().
|
inline |
Object comparison.
Definition at line 33 of file FuncDecl.java.
|
inline |
The arity of the function declaration
Definition at line 65 of file FuncDecl.java.
Referenced by Model.getConstInterp(), and Model.getFuncInterp().
|
inline |
The kind of the function declaration.
Definition at line 107 of file FuncDecl.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.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(), and Expr.isXor().
|
inline |
|
inline |
The size of the domain of the function declaration
Definition at line 74 of file FuncDecl.java.
Referenced by DatatypeSort.getAccessors(), FuncDecl.getDomain(), and Expr.isConst().
|
inline |
Returns a unique identifier for the function declaration.
Definition at line 57 of file FuncDecl.java.
|
inline |
The name of the function declaration
Definition at line 116 of file FuncDecl.java.
|
inline |
The number of parameters of the function declaration
Definition at line 126 of file FuncDecl.java.
Referenced by FuncDecl.getParameters().
|
inline |
The parameters of the function declaration
Definition at line 134 of file FuncDecl.java.
|
inline |
The range of the function declaration
Definition at line 97 of file FuncDecl.java.
|
inline |
Definition at line 48 of file FuncDecl.java.