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

Data Structures

class  Parameter
 

Public Member Functions

boolean equals (Object o)
 
int hashCode ()
 
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)
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object 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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.

Member Function Documentation

Expr apply ( Expr...  args)
inline

Create expression that applies function to arguments.

Parameters
args
Returns

Definition at line 383 of file FuncDecl.java.

Referenced by Tactic.__call__().

384  {
385  getContext().checkContextMatch(args);
386  return Expr.create(getContext(), this, args);
387  }
boolean equals ( Object  o)
inline

Comparison operator.

Returns
True if
a"/> and <paramref name="b
share the same context and are equal, false otherwise. Comparison operator.
True if
a"/> and <paramref name="b
do not share the same context or are not equal, false otherwise. Object comparison.

Definition at line 48 of file FuncDecl.java.

49  {
50  FuncDecl casted = (FuncDecl) o;
51  if (casted == null)
52  return false;
53  return this == casted;
54  }
int getArity ( )
inline

The arity of the function declaration

Definition at line 89 of file FuncDecl.java.

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

90  {
91  return Native.getArity(getContext().nCtx(), getNativeObject());
92  }
Z3_decl_kind getDeclKind ( )
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.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().

132  {
133  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
134  getNativeObject()));
135  }
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:966
Sort [] getDomain ( )
inline

The domain of the function declaration

Definition at line 106 of file FuncDecl.java.

107  {
108 
109  int n = getDomainSize();
110 
111  Sort[] res = new Sort[n];
112  for (int i = 0; i < n; i++)
113  res[i] = Sort.create(getContext(),
114  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
115  return res;
116  }
int getDomainSize ( )
inline

The size of the domain of the function declaration

See also
getArity

Definition at line 98 of file FuncDecl.java.

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

99  {
100  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
101  }
int getId ( )
inline

Returns a unique identifier for the function declaration.

Definition at line 81 of file FuncDecl.java.

82  {
83  return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
84  }
Symbol getName ( )
inline

The name of the function declaration

Definition at line 140 of file FuncDecl.java.

141  {
142 
143  return Symbol.create(getContext(),
144  Native.getDeclName(getContext().nCtx(), getNativeObject()));
145  }
int getNumParameters ( )
inline

The number of parameters of the function declaration

Definition at line 150 of file FuncDecl.java.

Referenced by FuncDecl.getParameters().

151  {
152  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
153  }
Parameter [] getParameters ( )
inline

The parameters of the function declaration

Definition at line 158 of file FuncDecl.java.

159  {
160 
161  int num = getNumParameters();
162  Parameter[] res = new Parameter[num];
163  for (int i = 0; i < num; i++)
164  {
165  Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
166  .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
167  switch (k)
168  {
169  case Z3_PARAMETER_INT:
170  res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
171  .nCtx(), getNativeObject(), i));
172  break;
173  case Z3_PARAMETER_DOUBLE:
174  res[i] = new Parameter(k, Native.getDeclDoubleParameter(
175  getContext().nCtx(), getNativeObject(), i));
176  break;
177  case Z3_PARAMETER_SYMBOL:
178  res[i] = new Parameter(k, Symbol.create(getContext(), Native
179  .getDeclSymbolParameter(getContext().nCtx(),
180  getNativeObject(), i)));
181  break;
182  case Z3_PARAMETER_SORT:
183  res[i] = new Parameter(k, Sort.create(getContext(), Native
184  .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
185  i)));
186  break;
187  case Z3_PARAMETER_AST:
188  res[i] = new Parameter(k, new AST(getContext(),
189  Native.getDeclAstParameter(getContext().nCtx(),
190  getNativeObject(), i)));
191  break;
193  res[i] = new Parameter(k, new FuncDecl(getContext(),
194  Native.getDeclFuncDeclParameter(getContext().nCtx(),
195  getNativeObject(), i)));
196  break;
198  res[i] = new Parameter(k, Native.getDeclRationalParameter(
199  getContext().nCtx(), getNativeObject(), i));
200  break;
201  default:
202  throw new Z3Exception(
203  "Unknown function declaration parameter kind encountered");
204  }
205  }
206  return res;
207  }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
Sort getRange ( )
inline

The range of the function declaration

Definition at line 121 of file FuncDecl.java.

122  {
123 
124  return Sort.create(getContext(),
125  Native.getRange(getContext().nCtx(), getNativeObject()));
126  }
int hashCode ( )
inline

A hash code.

Definition at line 59 of file FuncDecl.java.

60  {
61  return super.hashCode();
62  }
String toString ( )
inline

A string representations of the function declaration.

Definition at line 67 of file FuncDecl.java.

68  {
69  try
70  {
71  return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
72  } catch (Z3Exception e)
73  {
74  return "Z3Exception: " + e.getMessage();
75  }
76  }