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()));
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));
190 throw new Z3Exception(
191 "Unknown function declaration parameter kind encountered");
217 throw new Z3Exception(
"parameter is not an int");
227 throw new Z3Exception(
"parameter is not a double ");
237 throw new Z3Exception(
"parameter is not a Symbol");
247 throw new Z3Exception(
"parameter is not a Sort");
257 throw new Z3Exception(
"parameter is not an AST");
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);
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
expr range(expr const &lo, expr const &hi)
Z3_parameter_kind getParameterKind()
static String getDeclRationalParameter(long a0, long a1, int a2)
static long getDomain(long a0, long a1, int a2)
static int getDeclNumParameters(long a0, long a1)
static int getDomainSize(long a0, long a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
static String funcDeclToString(long a0, long a1)
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()
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
static int getFuncDeclId(long a0, long a1)
static boolean isEqFuncDecl(long a0, long a1, long a2)
static double getDeclDoubleParameter(long a0, long a1, int a2)
FuncDecl translate(Context ctx)
Parameter[] getParameters()
static long getRange(long a0, long a1)
static long getDeclName(long a0, long a1)