18 package com.microsoft.z3;
38 }
catch (ClassCastException e) {
46 (getContext().nCtx() == casted.getContext().nCtx()) &&
47 (
Native.
isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
55 return super.hashCode();
68 return "Z3Exception: " + e.getMessage();
106 for (
int i = 0; i < n; i++)
107 res[i] =
Sort.create(getContext(),
118 return Sort.create(getContext(),
137 return Symbol.create(getContext(),
157 for (
int i = 0; i < num; i++)
160 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
165 .nCtx(), getNativeObject(), i));
169 getContext().nCtx(), getNativeObject(), i));
173 .getDeclSymbolParameter(getContext().nCtx(),
174 getNativeObject(), i)));
178 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
184 getNativeObject(), i)));
189 getNativeObject(), i)));
193 getContext().nCtx(), getNativeObject(), i));
197 "Unknown function declaration parameter kind encountered");
233 throw new Z3Exception(
"parameter is not a double ");
243 throw new Z3Exception(
"parameter is not a Symbol");
273 throw new Z3Exception(
"parameter is not a function declaration");
283 throw new Z3Exception(
"parameter is not a rational String");
348 AST.arrayLength(domain),
AST.arrayToNative(domain),
349 range.getNativeObject()));
357 AST.arrayLength(domain),
AST.arrayToNative(domain),
358 range.getNativeObject()));
362 void checkNativeObject(
long obj)
367 "Underlying object is not a function declaration");
368 super.checkNativeObject(obj);
379 getContext().checkContextMatch(args);
380 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)
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)
static long getDeclName(long a0, long a1)