Data Structures | |
class | Parameter |
Public Member Functions | |
boolean | equals (Object o) |
int | hashCode () |
String | toString () |
int | getId () throws Z3Exception |
int | getArity () throws Z3Exception |
int | getDomainSize () throws Z3Exception |
Sort[] | getDomain () throws Z3Exception |
Sort | getRange () throws Z3Exception |
Z3_decl_kind | getDeclKind () throws Z3Exception |
Symbol | getName () throws Z3Exception |
int | getNumParameters () throws Z3Exception |
Parameter[] | getParameters () throws Z3Exception |
Expr | apply (Expr...args) throws Z3Exception |
Package Functions | |
FuncDecl (Context ctx, long obj) throws Z3Exception | |
FuncDecl (Context ctx, Symbol name, Sort[] domain, Sort range) throws Z3Exception | |
FuncDecl (Context ctx, String prefix, Sort[] domain, Sort range) throws Z3Exception | |
void | checkNativeObject (long obj) throws Z3Exception |
Function declarations.
Definition at line 27 of file FuncDecl.java.
FuncDecl | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 344 of file FuncDecl.java.
Referenced by FuncDecl.equals(), and FuncDecl.getParameters().
{ super(ctx, obj); }
FuncDecl | ( | Context | ctx, |
Symbol | name, | ||
Sort[] | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline, package] |
Definition at line 350 of file FuncDecl.java.
FuncDecl | ( | Context | ctx, |
String | prefix, | ||
Sort[] | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline, package] |
Definition at line 359 of file FuncDecl.java.
Expr apply | ( | Expr... | args | ) | throws Z3Exception [inline] |
Create expression that applies function to arguments.
args |
Definition at line 383 of file FuncDecl.java.
Referenced by Tactic.__call__().
{ getContext().checkContextMatch(args); return Expr.create(getContext(), this, args); }
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 368 of file FuncDecl.java.
{ if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST .toInt()) throw new Z3Exception( "Underlying object is not a function declaration"); super.checkNativeObject(obj); }
boolean equals | ( | Object | o | ) | [inline] |
Comparison operator.
Reimplemented from AST.
Definition at line 48 of file FuncDecl.java.
int getArity | ( | ) | throws Z3Exception [inline] |
The arity of the function declaration
Definition at line 89 of file FuncDecl.java.
{ return Native.getArity(getContext().nCtx(), getNativeObject()); }
Z3_decl_kind getDeclKind | ( | ) | throws Z3Exception [inline] |
The kind of the function declaration.
Definition at line 131 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.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.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(), and Expr.isXor().
{ return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(), getNativeObject())); }
Sort [] getDomain | ( | ) | throws Z3Exception [inline] |
The domain of the function declaration
Definition at line 106 of file FuncDecl.java.
{ int n = getDomainSize(); Sort[] res = new Sort[n]; for (int i = 0; i < n; i++) res[i] = Sort.create(getContext(), Native.getDomain(getContext().nCtx(), getNativeObject(), i)); return res; }
int getDomainSize | ( | ) | throws Z3Exception [inline] |
The size of the domain of the function declaration
Definition at line 98 of file FuncDecl.java.
Referenced by DatatypeSort.getAccessors(), FuncDecl.getDomain(), and Expr.isConst().
{ return Native.getDomainSize(getContext().nCtx(), getNativeObject()); }
int getId | ( | ) | throws Z3Exception [inline] |
Returns a unique identifier for the function declaration.
Reimplemented from AST.
Definition at line 81 of file FuncDecl.java.
{ return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); }
Symbol getName | ( | ) | throws Z3Exception [inline] |
The name of the function declaration
Definition at line 140 of file FuncDecl.java.
{ return Symbol.create(getContext(), Native.getDeclName(getContext().nCtx(), getNativeObject())); }
int getNumParameters | ( | ) | throws Z3Exception [inline] |
The number of parameters of the function declaration
Definition at line 150 of file FuncDecl.java.
Referenced by FuncDecl.getParameters().
{ return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject()); }
Parameter [] getParameters | ( | ) | throws Z3Exception [inline] |
The parameters of the function declaration
Definition at line 158 of file FuncDecl.java.
{ int num = getNumParameters(); Parameter[] res = new Parameter[num]; for (int i = 0; i < num; i++) { Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i)); switch (k) { case Z3_PARAMETER_INT: res[i] = new Parameter(k, Native.getDeclIntParameter(getContext() .nCtx(), getNativeObject(), i)); break; case Z3_PARAMETER_DOUBLE: res[i] = new Parameter(k, Native.getDeclDoubleParameter( getContext().nCtx(), getNativeObject(), i)); break; case Z3_PARAMETER_SYMBOL: res[i] = new Parameter(k, Symbol.create(getContext(), Native .getDeclSymbolParameter(getContext().nCtx(), getNativeObject(), i))); break; case Z3_PARAMETER_SORT: res[i] = new Parameter(k, Sort.create(getContext(), Native .getDeclSortParameter(getContext().nCtx(), getNativeObject(), i))); break; case Z3_PARAMETER_AST: res[i] = new Parameter(k, new AST(getContext(), Native.getDeclAstParameter(getContext().nCtx(), getNativeObject(), i))); break; case Z3_PARAMETER_FUNC_DECL: res[i] = new Parameter(k, new FuncDecl(getContext(), Native.getDeclFuncDeclParameter(getContext().nCtx(), getNativeObject(), i))); break; case Z3_PARAMETER_RATIONAL: res[i] = new Parameter(k, Native.getDeclRationalParameter( getContext().nCtx(), getNativeObject(), i)); break; default: throw new Z3Exception( "Unknown function declaration parameter kind encountered"); } } return res; }
Sort getRange | ( | ) | throws Z3Exception [inline] |
The range of the function declaration
Definition at line 121 of file FuncDecl.java.
{ return Sort.create(getContext(), Native.getRange(getContext().nCtx(), getNativeObject())); }
int hashCode | ( | ) | [inline] |
A hash code.
Reimplemented from AST.
Definition at line 59 of file FuncDecl.java.
{
return super.hashCode();
}
String toString | ( | ) | [inline] |
A string representations of the function declaration.
Reimplemented from AST.
Definition at line 67 of file FuncDecl.java.
{ try { return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }