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 };
com.microsoft.z3.ListSort.getIsConsDecl
FuncDecl getIsConsDecl()
Definition: ListSort.java:68
com.microsoft.z3.ListSort.getConsDecl
FuncDecl getConsDecl()
Definition: ListSort.java:58
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:27
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft.z3.Context.mkApp
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
com.microsoft.z3.ListSort.getNilDecl
FuncDecl getNilDecl()
Definition: ListSort.java:31
com.microsoft
com.microsoft.z3.Native.getDatatypeSortRecognizer
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2785
com.microsoft.z3.Native.LongPtr
Definition: Native.java:6
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.ListSort.getNil
Expr getNil()
Definition: ListSort.java:40
com.microsoft.z3.Native.getDatatypeSortConstructorAccessor
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2794
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.mkListSort
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
Definition: Native.java:1035
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.ListSort
Definition: ListSort.java:25
com.microsoft.z3.ListSort.getIsNilDecl
FuncDecl getIsNilDecl()
Definition: ListSort.java:49
com.microsoft.z3.ListSort.getTailDecl
FuncDecl getTailDecl()
Definition: ListSort.java:86
com
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.getDatatypeSortConstructor
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2776
com.microsoft.z3.ListSort.getHeadDecl
FuncDecl getHeadDecl()
Definition: ListSort.java:77