Z3
src/api/java/ListSort.java
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 };
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines