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 ()
 
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 }

◆ 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
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 }

◆ 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;
163 res[i] = new Parameter(k, Native.getDeclDoubleParameter(
164 getContext().nCtx(), getNativeObject(), i));
165 break;
167 res[i] = new Parameter(k, Symbol.create(getContext(), Native
168 .getDeclSymbolParameter(getContext().nCtx(),
169 getNativeObject(), i)));
170 break;
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;
182 res[i] = new Parameter(k, new FuncDecl<>(getContext(),
183 Native.getDeclFuncDeclParameter(getContext().nCtx(),
184 getNativeObject(), i)));
185 break;
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 }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:136
@ Z3_PARAMETER_INT
Definition: z3_api.h:137
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:143
@ Z3_PARAMETER_SORT
Definition: z3_api.h:141
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:139
@ Z3_PARAMETER_AST
Definition: z3_api.h:142
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:138
@ 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
ctxA context
Returns
A copy of the function declaration which is associated with ctx
Exceptions
Z3Exceptionon 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__().