Z3
EnumSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class EnumSort extends Sort
24 {
30  {
31  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
32  FuncDecl[] t = new FuncDecl[n];
33  for (int i = 0; i < n; i++)
34  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
35  return t;
36  }
37 
42  public FuncDecl getConstDecl(int inx)
43  {
44  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
45  }
46 
52  public Expr[] getConsts()
53  {
54  FuncDecl[] cds = getConstDecls();
55  Expr[] t = new Expr[cds.length];
56  for (int i = 0; i < t.length; i++)
57  t[i] = getContext().mkApp(cds[i]);
58  return t;
59  }
60 
66  public Expr getConst(int inx)
67  {
68  return getContext().mkApp(getConstDecl(inx));
69  }
70 
76  {
77  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
78  FuncDecl[] t = new FuncDecl[n];
79  for (int i = 0; i < n; i++)
80  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
81  return t;
82  }
83 
88  public FuncDecl getTesterDecl(int inx)
89  {
90  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
91  }
92 
93  EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
94  {
95  super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
96  name.getNativeObject(), enumNames.length,
97  Symbol.arrayToNative(enumNames),
98  new long[enumNames.length], new long[enumNames.length]));
99  }
100 };
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 getConst(int inx)
Definition: EnumSort.java:66
FuncDecl [] getConstDecls()
Definition: EnumSort.java:29
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:644
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2420
FuncDecl getTesterDecl(int inx)
Definition: EnumSort.java:88
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
Definition: Native.java:957
FuncDecl getConstDecl(int inx)
Definition: EnumSort.java:42
FuncDecl [] getTesterDecls()
Definition: EnumSort.java:75