Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00023 public class ListSort extends Sort
00024 {
00029 public FuncDecl getNilDecl() throws Z3Exception
00030 {
00031 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
00032 }
00033
00038 public Expr getNil() throws Z3Exception
00039 {
00040 return getContext().mkApp(getNilDecl());
00041 }
00042
00047 public FuncDecl getIsNilDecl() throws Z3Exception
00048 {
00049 return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
00050 }
00051
00056 public FuncDecl getConsDecl() throws Z3Exception
00057 {
00058 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
00059 }
00060
00066 public FuncDecl getIsConsDecl() throws Z3Exception
00067 {
00068 return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
00069 }
00070
00075 public FuncDecl getHeadDecl() throws Z3Exception
00076 {
00077 return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
00078 }
00079
00084 public FuncDecl getTailDecl() throws Z3Exception
00085 {
00086 return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
00087 }
00088
00089 ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception
00090 {
00091 super(ctx);
00092
00093 Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr();
00094 Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr();
00095 Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr();
00096
00097 setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
00098 elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead,
00099 itail));
00100 }
00101 };