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 ()
 
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 356 of file FuncDecl.java.

Referenced by Tactic.__call__().

357  {
358  getContext().checkContextMatch(args);
359  return Expr.create(getContext(), this, args);
360  }

§ equals()

boolean equals ( Object  o)
inline

Object comparison.

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

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

66  {
67  return Native.getArity(getContext().nCtx(), getNativeObject());
68  }

§ getDeclKind()

Z3_decl_kind getDeclKind ( )
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().

108  {
109  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
110  getNativeObject()));
111  }
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

§ getDomain()

Sort [] getDomain ( )
inline

The domain of the function declaration

Definition at line 82 of file FuncDecl.java.

83  {
84 
85  int n = getDomainSize();
86 
87  Sort[] res = new Sort[n];
88  for (int i = 0; i < n; i++)
89  res[i] = Sort.create(getContext(),
90  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
91  return res;
92  }

§ getDomainSize()

int getDomainSize ( )
inline

The size of the domain of the function declaration

See also
getArity

Definition at line 74 of file FuncDecl.java.

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

75  {
76  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
77  }

§ getId()

int getId ( )
inline

Returns a unique identifier for the function declaration.

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

117  {
118 
119  return Symbol.create(getContext(),
120  Native.getDeclName(getContext().nCtx(), getNativeObject()));
121  }

§ getNumParameters()

int getNumParameters ( )
inline

The number of parameters of the function declaration

Definition at line 126 of file FuncDecl.java.

Referenced by FuncDecl.getParameters().

127  {
128  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
129  }

§ getParameters()

Parameter [] getParameters ( )
inline

The parameters of the function declaration

Definition at line 134 of file FuncDecl.java.

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

§ getRange()

Sort getRange ( )
inline

The range of the function declaration

Definition at line 97 of file FuncDecl.java.

98  {
99 
100  return Sort.create(getContext(),
101  Native.getRange(getContext().nCtx(), getNativeObject()));
102  }

§ toString()

String toString ( )
inline

Definition at line 48 of file FuncDecl.java.

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