Public Member Functions | |
int | getNumFields () throws Z3Exception |
FuncDecl | ConstructorDecl () throws Z3Exception |
FuncDecl | getTesterDecl () throws Z3Exception |
FuncDecl[] | getAccessorDecls () throws Z3Exception |
Protected Member Functions | |
void | finalize () throws Z3Exception |
Package Functions | |
Constructor (Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
Constructors are used for datatype sorts.
Definition at line 23 of file Constructor.java.
Constructor | ( | Context | ctx, |
Symbol | name, | ||
Symbol | recognizer, | ||
Symbol[] | fieldNames, | ||
Sort[] | sorts, | ||
int[] | sortRefs | ||
) | throws Z3Exception [inline, package] |
Definition at line 86 of file Constructor.java.
{ super(ctx); n = AST.arrayLength(fieldNames); if (n != AST.arrayLength(sorts)) throw new Z3Exception( "Number of field names does not match number of sorts"); if (sortRefs != null && sortRefs.length != n) throw new Z3Exception( "Number of field names does not match number of sort refs"); if (sortRefs == null) sortRefs = new int[n]; setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames), Sort.arrayToNative(sorts), sortRefs)); }
FuncDecl ConstructorDecl | ( | ) | throws Z3Exception [inline] |
The function declaration of the constructor.
Z3Exception |
Definition at line 38 of file Constructor.java.
{ Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); return new FuncDecl(getContext(), constructor.value); }
void finalize | ( | ) | throws Z3Exception [inline, protected] |
Destructor.
Reimplemented from Z3Object.
Definition at line 79 of file Constructor.java.
{ Native.delConstructor(getContext().nCtx(), getNativeObject()); }
FuncDecl [] getAccessorDecls | ( | ) | throws Z3Exception [inline] |
The function declarations of the accessors
Z3Exception |
Definition at line 64 of file Constructor.java.
{ Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) t[i] = new FuncDecl(getContext(), accessors[i]); return t; }
int getNumFields | ( | ) | throws Z3Exception [inline] |
The number of fields of the constructor.
Z3Exception |
Definition at line 29 of file Constructor.java.
{
return n;
}
FuncDecl getTesterDecl | ( | ) | throws Z3Exception [inline] |
The function declaration of the tester.
Z3Exception |
Definition at line 51 of file Constructor.java.
{ Native.LongPtr constructor = new Native.LongPtr(); Native.LongPtr tester = new Native.LongPtr(); long[] accessors = new long[n]; Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); return new FuncDecl(getContext(), tester.value); }