Z3
ListSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class ListSort extends Sort
24 {
30  {
31  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
32  }
33 
38  public Expr getNil()
39  {
40  return getContext().mkApp(getNilDecl());
41  }
42 
48  {
49  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
50  }
51 
57  {
58  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
59  }
60 
67  {
68  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
69  }
70 
76  {
77  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
78  }
79 
85  {
86  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
87  }
88 
89  ListSort(Context ctx, Symbol name, Sort elemSort)
90  {
91  super(ctx, 0);
92 
93  Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr();
94  Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr();
95  Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr();
96 
97  setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
98  elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead,
99  itail));
100  }
101 };
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2180
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2171
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
Definition: Native.java:960
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2189