18 package com.microsoft.z3;
53 return this == casted;
61 return super.hashCode();
74 return "Z3Exception: " + e.getMessage();
112 for (
int i = 0; i < n; i++)
113 res[i] =
Sort.create(getContext(),
124 return Sort.create(getContext(),
143 return Symbol.create(getContext(),
163 for (
int i = 0; i < num; i++)
166 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
171 .nCtx(), getNativeObject(), i));
175 getContext().nCtx(), getNativeObject(), i));
179 .getDeclSymbolParameter(getContext().nCtx(),
180 getNativeObject(), i)));
184 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
190 getNativeObject(), i)));
195 getNativeObject(), i)));
199 getContext().nCtx(), getNativeObject(), i));
203 "Unknown function declaration parameter kind encountered");
239 throw new Z3Exception(
"parameter is not a double ");
249 throw new Z3Exception(
"parameter is not a Symbol");
279 throw new Z3Exception(
"parameter is not a function declaration");
289 throw new Z3Exception(
"parameter is not a rational String");
344 FuncDecl(Context ctx,
long obj)
350 FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
353 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
354 AST.arrayLength(domain), AST.arrayToNative(domain),
355 range.getNativeObject()));
359 FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
362 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
363 AST.arrayLength(domain), AST.arrayToNative(domain),
364 range.getNativeObject()));
368 void checkNativeObject(
long obj)
370 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_FUNC_DECL_AST
372 throw new Z3Exception(
373 "Underlying object is not a function declaration");
374 super.checkNativeObject(obj);
385 getContext().checkContextMatch(args);
386 return Expr.create(getContext(),
this, args);
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
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 double getDeclDoubleParameter(long a0, long a1, int a2)
Parameter[] getParameters()
static long getRange(long a0, long a1)
static long getDeclName(long a0, long a1)