18 package com.microsoft.z3;
35 if (o ==
this)
return true;
36 if (!(o instanceof
FuncDecl))
return false;
40 (getContext().
nCtx() == other.getContext().
nCtx()) &&
44 other.getNativeObject()));
100 for (
int i = 0; i < n; i++)
101 res[i] =
Sort.create(getContext(),
112 return Sort.create(getContext(),
131 return Symbol.create(getContext(),
151 for (
int i = 0; i < num; i++)
154 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
159 .nCtx(), getNativeObject(), i));
163 getContext().nCtx(), getNativeObject(), i));
167 .getDeclSymbolParameter(getContext().nCtx(),
168 getNativeObject(), i)));
172 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
178 getNativeObject(), i)));
183 getNativeObject(), i)));
187 getContext().nCtx(), getNativeObject(), i));
191 "Unknown function declaration parameter kind encountered");
227 throw new Z3Exception(
"parameter is not a double ");
237 throw new Z3Exception(
"parameter is not a Symbol");
267 throw new Z3Exception(
"parameter is not a function declaration");
277 throw new Z3Exception(
"parameter is not a rational String");
332 FuncDecl(Context ctx,
long obj)
338 FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort
range)
341 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
342 AST.arrayLength(domain), AST.arrayToNative(domain),
343 range.getNativeObject()));
347 FuncDecl(Context ctx,
String prefix, Sort[] domain, Sort
range)
350 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
351 AST.arrayLength(domain), AST.arrayToNative(domain),
352 range.getNativeObject()));
356 void checkNativeObject(
long obj)
358 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_FUNC_DECL_AST
360 throw new Z3Exception(
361 "Underlying object is not a function declaration");
362 super.checkNativeObject(obj);
370 getContext().checkContextMatch(args);
371 return Expr.create(getContext(),
this, args);