Public Member Functions | |
FuncDecl | getNilDecl () throws Z3Exception |
Expr | getNil () throws Z3Exception |
FuncDecl | getIsNilDecl () throws Z3Exception |
FuncDecl | getConsDecl () throws Z3Exception |
FuncDecl | getIsConsDecl () throws Z3Exception |
FuncDecl | getHeadDecl () throws Z3Exception |
FuncDecl | getTailDecl () throws Z3Exception |
Package Functions | |
ListSort (Context ctx, Symbol name, Sort elemSort) throws Z3Exception |
List sorts.
Definition at line 23 of file ListSort.java.
ListSort | ( | Context | ctx, |
Symbol | name, | ||
Sort | elemSort | ||
) | throws Z3Exception [inline, package] |
Definition at line 89 of file ListSort.java.
{ super(ctx); Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr(); Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr(); Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr(); setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(), elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead, itail)); }
FuncDecl getConsDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the cons function of this list sort.
Z3Exception |
Definition at line 56 of file ListSort.java.
{ return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1)); }
FuncDecl getHeadDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the head function of this list sort.
Z3Exception |
Definition at line 75 of file ListSort.java.
{ return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0)); }
FuncDecl getIsConsDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the isCons function of this list sort.
Z3Exception |
Definition at line 66 of file ListSort.java.
{ return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1)); }
FuncDecl getIsNilDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the isNil function of this list sort.
Z3Exception |
Definition at line 47 of file ListSort.java.
{ return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0)); }
Expr getNil | ( | ) | throws Z3Exception [inline] |
The empty list.
Z3Exception |
Definition at line 38 of file ListSort.java.
{ return getContext().mkApp(getNilDecl()); }
FuncDecl getNilDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the nil function of this list sort.
Z3Exception |
Definition at line 29 of file ListSort.java.
Referenced by ListSort.getNil().
{ return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0)); }
FuncDecl getTailDecl | ( | ) | throws Z3Exception [inline] |
The declaration of the tail function of this list sort.
Z3Exception |
Definition at line 84 of file ListSort.java.
{ return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1)); }