Z3
ListSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class ListSort extends Sort
26 {
32  {
33  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
34  }
35 
40  public Expr getNil()
41  {
42  return getContext().mkApp(getNilDecl());
43  }
44 
50  {
51  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
52  }
53 
59  {
60  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
61  }
62 
69  {
70  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
71  }
72 
78  {
79  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
80  }
81 
87  {
88  return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
89  }
90 
91  ListSort(Context ctx, Symbol name, Sort elemSort)
92  {
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()));
97  }
98 };
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2438
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2429
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:644
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
Definition: Native.java:966
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2447