18package com.microsoft.z3;
20import com.microsoft.z3.Native.LongPtr;
33 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
51 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
60 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
70 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
79 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
88 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
93 super(ctx, Native.mkListSort(ctx.
nCtx(), name.getNativeObject(),
94 elemSort.getNativeObject(),
95 new LongPtr(),
new Native.LongPtr(),
new LongPtr(),
96 new LongPtr(),
new LongPtr(),
new LongPtr()));
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
FuncDecl< BoolSort > getIsNilDecl()
FuncDecl< ListSort< R > > getTailDecl()
FuncDecl< BoolSort > getIsConsDecl()
FuncDecl< ListSort< R > > getConsDecl()
Expr< ListSort< R > > getNil()
FuncDecl< R > getHeadDecl()
FuncDecl< ListSort< R > > getNilDecl()