18 package com.microsoft.z3;
35 if (o ==
this)
return true;
36 if (!(o instanceof
FuncDecl))
return false;
37 FuncDecl other = (FuncDecl) o;
40 (getContext().nCtx() == other.getContext().nCtx()) &&
44 other.getNativeObject()));
88 for (
int i = 0; i < n; i++)
89 res[i] =
Sort.create(getContext(),
100 return Sort.create(getContext(),
119 return Symbol.create(getContext(),
139 for (
int i = 0; i < num; i++)
142 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
147 .nCtx(), getNativeObject(), i));
151 getContext().nCtx(), getNativeObject(), i));
155 .getDeclSymbolParameter(getContext().nCtx(),
156 getNativeObject(), i)));
160 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
166 getNativeObject(), i)));
171 getNativeObject(), i)));
175 getContext().nCtx(), getNativeObject(), i));
179 "Unknown function declaration parameter kind encountered");
215 throw new Z3Exception(
"parameter is not a double ");
225 throw new Z3Exception(
"parameter is not a Symbol");
255 throw new Z3Exception(
"parameter is not a function declaration");
265 throw new Z3Exception(
"parameter is not a rational String");
330 AST.arrayLength(domain),
AST.arrayToNative(domain),
331 range.getNativeObject()));
339 AST.arrayLength(domain),
AST.arrayToNative(domain),
340 range.getNativeObject()));
344 void checkNativeObject(
long obj)
349 "Underlying object is not a function declaration");
350 super.checkNativeObject(obj);
358 getContext().checkContextMatch(args);
359 return Expr.create(getContext(),
this, args);
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
static long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
Z3_parameter_kind getParameterKind()
static String getDeclRationalParameter(long a0, long a1, int a2)
Expr apply(Expr ... args)
static long getDomain(long a0, long a1, int a2)
static int getDeclNumParameters(long a0, long a1)
static int getDomainSize(long a0, long a1)
static String funcDeclToString(long a0, long a1)
static long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
static final Z3_parameter_kind fromInt(int v)
static int getDeclKind(long a0, long a1)
static int getArity(long a0, long a1)
static long getDeclAstParameter(long a0, long a1, int a2)
static int getDeclIntParameter(long a0, long a1, int a2)
Z3_decl_kind getDeclKind()
static int getFuncDeclId(long a0, long a1)
static int getAstKind(long a0, long a1)
static boolean isEqFuncDecl(long a0, long a1, long a2)
static double getDeclDoubleParameter(long a0, long a1, int a2)
Parameter [] getParameters()
static long getRange(long a0, long a1)
def String(name, ctx=None)
static long getDeclName(long a0, long a1)