Z3
Data Structures | Public Member Functions
FuncDecl Class Reference
+ Inheritance diagram for FuncDecl:

Data Structures

class  Parameter
 

Public Member Functions

boolean equals (Object o)
 
String toString ()
 
int getId ()
 
FuncDecl translate (Context ctx)
 
int getArity ()
 
int getDomainSize ()
 
Sort[] getDomain ()
 
Sort getRange ()
 
Z3_decl_kind getDeclKind ()
 
Symbol getName ()
 
int getNumParameters ()
 
Parameter[] getParameters ()
 
Expr apply (Expr ... args)
 
- Public Member Functions inherited from AST
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 ()
 

Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.

Member Function Documentation

◆ apply()

Expr apply ( Expr ...  args)
inline

Create expression that applies function to arguments.

Definition at line 368 of file FuncDecl.java.

369 {
370 getContext().checkContextMatch(args);
371 return Expr.create(getContext(), this, args);
372 }

Referenced by Tactic.__call__().

◆ equals()

boolean equals ( Object  o)
inline

Object comparison.

Reimplemented from AST.

Definition at line 33 of file FuncDecl.java.

34 {
35 if (o == this) return true;
36 if (!(o instanceof FuncDecl)) return false;
37 FuncDecl other = (FuncDecl) o;
38
39 return
40 (getContext().nCtx() == other.getContext().nCtx()) &&
41 (Native.isEqFuncDecl(
42 getContext().nCtx(),
43 getNativeObject(),
44 other.getNativeObject()));
45 }

◆ getArity()

int getArity ( )
inline

The arity of the function declaration

Definition at line 77 of file FuncDecl.java.

78 {
79 return Native.getArity(getContext().nCtx(), getNativeObject());
80 }

Referenced by Model.getConstInterp(), and Model.getFuncInterp().

◆ getDeclKind()

Z3_decl_kind getDeclKind ( )
inline

The kind of the function declaration.

Definition at line 119 of file FuncDecl.java.

120 {
121 return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
122 getNativeObject()));
123 }
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007

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.isConcat(), 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.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.isProofOrElimination(), Expr.isProofPullQuant(), 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().

◆ getDomain()

Sort[] getDomain ( )
inline

The domain of the function declaration

Definition at line 94 of file FuncDecl.java.

95 {
96
97 int n = getDomainSize();
98
99 Sort[] res = new Sort[n];
100 for (int i = 0; i < n; i++)
101 res[i] = Sort.create(getContext(),
102 Native.getDomain(getContext().nCtx(), getNativeObject(), i));
103 return res;
104 }

◆ getDomainSize()

int getDomainSize ( )
inline

The size of the domain of the function declaration

See also
getArity

Definition at line 86 of file FuncDecl.java.

87 {
88 return Native.getDomainSize(getContext().nCtx(), getNativeObject());
89 }

Referenced by DatatypeSort.getAccessors(), FuncDecl.getDomain(), and Expr.isConst().

◆ getId()

int getId ( )
inline

Returns a unique identifier for the function declaration.

Reimplemented from AST.

Definition at line 57 of file FuncDecl.java.

58 {
59 return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
60 }

◆ getName()

Symbol getName ( )
inline

The name of the function declaration

Definition at line 128 of file FuncDecl.java.

129 {
130
131 return Symbol.create(getContext(),
132 Native.getDeclName(getContext().nCtx(), getNativeObject()));
133 }

◆ getNumParameters()

int getNumParameters ( )
inline

The number of parameters of the function declaration

Definition at line 138 of file FuncDecl.java.

139 {
140 return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
141 }

Referenced by FuncDecl.getParameters().

◆ getParameters()

Parameter[] getParameters ( )
inline

The parameters of the function declaration

Definition at line 146 of file FuncDecl.java.

147 {
148
149 int num = getNumParameters();
150 Parameter[] res = new Parameter[num];
151 for (int i = 0; i < num; i++)
152 {
153 Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
154 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
155 switch (k)
156 {
157 case Z3_PARAMETER_INT:
158 res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
159 .nCtx(), getNativeObject(), i));
160 break;
162 res[i] = new Parameter(k, Native.getDeclDoubleParameter(
163 getContext().nCtx(), getNativeObject(), i));
164 break;
166 res[i] = new Parameter(k, Symbol.create(getContext(), Native
167 .getDeclSymbolParameter(getContext().nCtx(),
168 getNativeObject(), i)));
169 break;
171 res[i] = new Parameter(k, Sort.create(getContext(), Native
172 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
173 i)));
174 break;
175 case Z3_PARAMETER_AST:
176 res[i] = new Parameter(k, new AST(getContext(),
177 Native.getDeclAstParameter(getContext().nCtx(),
178 getNativeObject(), i)));
179 break;
181 res[i] = new Parameter(k, new FuncDecl(getContext(),
182 Native.getDeclFuncDeclParameter(getContext().nCtx(),
183 getNativeObject(), i)));
184 break;
186 res[i] = new Parameter(k, Native.getDeclRationalParameter(
187 getContext().nCtx(), getNativeObject(), i));
188 break;
189 default:
190 throw new Z3Exception(
191 "Unknown function declaration parameter kind encountered");
192 }
193 }
194 return res;
195 }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:134
@ Z3_PARAMETER_INT
Definition: z3_api.h:135
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:141
@ Z3_PARAMETER_SORT
Definition: z3_api.h:139
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:137
@ Z3_PARAMETER_AST
Definition: z3_api.h:140
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:136
@ Z3_PARAMETER_SYMBOL
Definition: z3_api.h:138

◆ getRange()

Sort getRange ( )
inline

The range of the function declaration

Definition at line 109 of file FuncDecl.java.

110 {
111
112 return Sort.create(getContext(),
113 Native.getRange(getContext().nCtx(), getNativeObject()));
114 }

◆ toString()

String toString ( )
inline

A string representation of the AST.

Reimplemented from AST.

Definition at line 48 of file FuncDecl.java.

49 {
50 return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
51 }

◆ translate()

FuncDecl translate ( Context  ctx)
inline

Translates (copies) the function declaration to the Context ctx.

Parameters
ctxA context
Returns
A copy of the function declaration which is associated with ctx
Exceptions
Z3Exceptionon error

Reimplemented from AST.

Definition at line 69 of file FuncDecl.java.

70 {
71 return (FuncDecl) super.translate(ctx);
72 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and FuncDecl.translate().