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()));
50 return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
59 return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
69 @SuppressWarnings(
"unchecked")
80 return Native.getArity(getContext().nCtx(), getNativeObject());
89 return Native.getDomainSize(getContext().nCtx(), getNativeObject());
101 for (
int i = 0; i < n; i++)
102 res[i] =
Sort.create(getContext(),
103 Native.getDomain(getContext().nCtx(), getNativeObject(), i));
110 @SuppressWarnings(
"unchecked")
113 return (R)
Sort.create(getContext(),
114 Native.getRange(getContext().nCtx(), getNativeObject()));
122 return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
132 return Symbol.create(getContext(),
133 Native.getDeclName(getContext().nCtx(), getNativeObject()));
141 return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
151 Parameter[] res =
new Parameter[num];
152 for (
int i = 0; i < num; i++)
155 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
159 res[i] =
new Parameter(k, Native.getDeclIntParameter(getContext()
160 .nCtx(), getNativeObject(), i));
163 res[i] =
new Parameter(k, Native.getDeclDoubleParameter(
164 getContext().nCtx(), getNativeObject(), i));
167 res[i] =
new Parameter(k,
Symbol.create(getContext(), Native
168 .getDeclSymbolParameter(getContext().nCtx(),
169 getNativeObject(), i)));
172 res[i] =
new Parameter(k,
Sort.create(getContext(), Native
173 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
177 res[i] =
new Parameter(k,
new AST(getContext(),
178 Native.getDeclAstParameter(getContext().nCtx(),
179 getNativeObject(), i)));
182 res[i] =
new Parameter(k,
new FuncDecl<>(getContext(),
183 Native.getDeclFuncDeclParameter(getContext().nCtx(),
184 getNativeObject(), i)));
187 res[i] =
new Parameter(k, Native.getDeclRationalParameter(
188 getContext().nCtx(), getNativeObject(), i));
192 "Unknown function declaration parameter kind encountered");
201 public static class Parameter
225 public double getDouble()
228 throw new Z3Exception(
"parameter is not a double ");
235 public Symbol getSymbol()
238 throw new Z3Exception(
"parameter is not a Symbol");
245 public Sort getSort()
248 throw new Z3Exception(
"parameter is not a Sort");
258 throw new Z3Exception(
"parameter is not an AST");
268 throw new Z3Exception(
"parameter is not a function declaration");
275 public String getRational()
278 throw new Z3Exception(
"parameter is not a rational String");
333 FuncDecl(Context ctx,
long obj)
339 FuncDecl(Context ctx, Symbol name, Sort[] domain, R
range)
341 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
342 AST.arrayLength(domain), AST.arrayToNative(domain),
343 range.getNativeObject()));
346 FuncDecl(Context ctx, Symbol name, Sort[] domain, R
range,
boolean is_rec)
348 super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(),
349 AST.arrayLength(domain), AST.arrayToNative(domain),
350 range.getNativeObject()));
354 FuncDecl(Context ctx,
String prefix, Sort[] domain, R
range)
356 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
357 AST.arrayLength(domain), AST.arrayToNative(domain),
358 range.getNativeObject()));
362 void checkNativeObject(
long obj)
364 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_FUNC_DECL_AST
366 throw new Z3Exception(
367 "Underlying object is not a function declaration");
368 super.checkNativeObject(obj);
376 getContext().checkContextMatch(args);
377 return Expr.create(getContext(),
this, args);
Expr< R > apply(Expr<?> ... args)
Parameter[] getParameters()
Z3_decl_kind getDeclKind()
FuncDecl< R > translate(Context ctx)
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_decl_kind
The different kinds of interpreted function kinds.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.