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 377 of file FuncDecl.java.

Referenced by Tactic.__call__().

378  {
379  getContext().checkContextMatch(args);
380  return Expr.create(getContext(), this, args);
381  }
boolean equals ( Object  o)
inline

Object comparison.

Definition at line 32 of file FuncDecl.java.

33  {
34  FuncDecl casted = null;
35 
36  try {
37  casted = FuncDecl.class.cast(o);
38  } catch (ClassCastException e) {
39  return false;
40  }
41 
42  return
43  (this == casted) ||
44  (this != null) &&
45  (casted != null) &&
46  (getContext().nCtx() == casted.getContext().nCtx()) &&
47  (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
48  }
int getArity ( )
inline

The arity of the function declaration

Definition at line 83 of file FuncDecl.java.

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

84  {
85  return Native.getArity(getContext().nCtx(), getNativeObject());
86  }
Z3_decl_kind getDeclKind ( )
inline

The kind of the function declaration.

Definition at line 125 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().

126  {
127  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
128  getNativeObject()));
129  }
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
Sort [] getDomain ( )
inline

The domain of the function declaration

Definition at line 100 of file FuncDecl.java.

101  {
102 
103  int n = getDomainSize();
104 
105  Sort[] res = new Sort[n];
106  for (int i = 0; i < n; i++)
107  res[i] = Sort.create(getContext(),
108  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
109  return res;
110  }
int getDomainSize ( )
inline

The size of the domain of the function declaration

See also
getArity

Definition at line 92 of file FuncDecl.java.

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

93  {
94  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
95  }
int getId ( )
inline

Returns a unique identifier for the function declaration.

Definition at line 75 of file FuncDecl.java.

76  {
77  return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
78  }
Symbol getName ( )
inline

The name of the function declaration

Definition at line 134 of file FuncDecl.java.

135  {
136 
137  return Symbol.create(getContext(),
138  Native.getDeclName(getContext().nCtx(), getNativeObject()));
139  }
int getNumParameters ( )
inline

The number of parameters of the function declaration

Definition at line 144 of file FuncDecl.java.

Referenced by FuncDecl.getParameters().

145  {
146  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
147  }
Parameter [] getParameters ( )
inline

The parameters of the function declaration

Definition at line 152 of file FuncDecl.java.

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

The range of the function declaration

Definition at line 115 of file FuncDecl.java.

116  {
117 
118  return Sort.create(getContext(),
119  Native.getRange(getContext().nCtx(), getNativeObject()));
120  }
int hashCode ( )
inline

A hash code.

Definition at line 53 of file FuncDecl.java.

54  {
55  return super.hashCode();
56  }
String toString ( )
inline

A string representations of the function declaration.

Definition at line 61 of file FuncDecl.java.

62  {
63  try
64  {
65  return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
66  } catch (Z3Exception e)
67  {
68  return "Z3Exception: " + e.getMessage();
69  }
70  }