Z3 |

Data Structures | Public Member Functions
FuncDecl< R extends Sort > Class Template Reference
Inheritance diagram for FuncDecl< R extends Sort >:

## Data Structures
class | Parameter

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

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.

## Member Function Documentation

## ◆ apply()

Expr< R > apply | ( | Expr<?> ... | args | ) |
| inline

Create expression that applies function to arguments.

Definition at line 374 of file FuncDecl.java.

375 {
376 getContext().checkContextMatch(args);
377 return Expr.create(getContext(), this, args);
378 }

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 }
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.FuncDecl<?>

## ◆ getArity()

int getArity | ( |  | ) |
| inline

The arity of the function declaration

Definition at line 78 of file FuncDecl.java.

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

## ◆ getDeclKind()

Z3_decl_kind getDeclKind | ( |  | ) |
| inline

The kind of the function declaration.

Definition at line 120 of file FuncDecl.java.

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

## ◆ getDomain()

Sort[] getDomain | ( |  | ) |
| inline

The domain of the function declaration

Definition at line 95 of file FuncDecl.java.

96 {
97
98 int n = getDomainSize();
99
100 Sort[] res = new Sort[n];
101 for (int i = 0; i < n; i++)
102 res[i] = Sort.create(getContext(),
103 Native.getDomain(getContext().nCtx(), getNativeObject(), i));
104 return res;
105 }
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:87

## ◆ getDomainSize()

int getDomainSize | ( |  | ) |
| inline

The size of the domain of the function declaration

See also
  getArity

Definition at line 87 of file FuncDecl.java.

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

Referenced by DatatypeSort< R >.getAccessors(), and FuncDecl< R extends Sort >.getDomain().

## ◆ 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 129 of file FuncDecl.java.

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

## ◆ getNumParameters()

int getNumParameters | ( |  | ) |
| inline

The number of parameters of the function declaration

Definition at line 139 of file FuncDecl.java.

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

Referenced by FuncDecl< R extends Sort >.getParameters().

## ◆ getParameters()

Parameter[] getParameters | ( |  | ) |
| inline

The parameters of the function declaration

Definition at line 147 of file FuncDecl.java.

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

## ◆ getRange()

R getRange | ( |  | ) |
| inline

The range of the function declaration

Definition at line 111 of file FuncDecl.java.

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

## ◆ 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< R > translate | ( | Context | ctx | ) |
| inline

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

Parameters

  ctx | A context

Returns
  A copy of the function declaration which is associated with `ctx`

Exceptions

  Z3Exception | on error

Reimplemented from AST.

Definition at line 70 of file FuncDecl.java.

71 {
72 return (FuncDecl<R>) super.translate(ctx);
73 }

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