18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_decl_kind;
22import com.microsoft.z3.enumerations.Z3_parameter_kind;
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);
Z3_parameter_kind getParameterKind()
FuncDecl translate(Context ctx)
Parameter[] getParameters()
Z3_decl_kind getDeclKind()
Expr apply(Expr ... args)
static int getDomainSize(long a0, long a1)
static int getDeclIntParameter(long a0, long a1, int a2)
static double getDeclDoubleParameter(long a0, long a1, int a2)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
static int getFuncDeclId(long a0, long a1)
static boolean isEqFuncDecl(long a0, long a1, long a2)
static long getRange(long a0, long a1)
static int getArity(long a0, long a1)
static long getDeclAstParameter(long a0, long a1, int a2)
static long getDomain(long a0, long a1, int a2)
static String funcDeclToString(long a0, long a1)
static int getDeclKind(long a0, long a1)
static int getDeclNumParameters(long a0, long a1)
static long getDeclName(long a0, long a1)
static String getDeclRationalParameter(long a0, long a1, int a2)
static final Z3_decl_kind fromInt(int v)
static final Z3_parameter_kind fromInt(int v)
expr range(expr const &lo, expr const &hi)
def String(name, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.