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
int compareTo (AST other)
 
int hashCode ()
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
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:961

◆ 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;
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;
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:94
@ Z3_PARAMETER_INT
Definition: z3_api.h:95
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:101
@ Z3_PARAMETER_SORT
Definition: z3_api.h:99
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:97
@ Z3_PARAMETER_AST
Definition: z3_api.h:100
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:96
@ Z3_PARAMETER_SYMBOL
Definition: z3_api.h:98

◆ 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__().