Z3
EnumSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class EnumSort extends Sort
24 {
29  {
30  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
31  FuncDecl[] t = new FuncDecl[n];
32  for (int i = 0; i < n; i++)
33  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
34  return t;
35  }
36 
40  public Expr[] getConsts() throws Z3Exception
41  {
42  FuncDecl[] cds = getConstDecls();
43  Expr[] t = new Expr[cds.length];
44  for (int i = 0; i < t.length; i++)
45  t[i] = getContext().mkApp(cds[i]);
46  return t;
47  }
48 
53  {
54  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
55  FuncDecl[] t = new FuncDecl[n];
56  for (int i = 0; i < n; i++)
57  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
58  return t;
59  }
60 
61  EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
62  {
63  super(ctx);
64 
65  int n = enumNames.length;
66  long[] n_constdecls = new long[n];
67  long[] n_testers = new long[n];
68  setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
69  name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
70  n_constdecls, n_testers));
71  }
72 };
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2084
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2075
FuncDecl[] getConstDecls()
Definition: EnumSort.java:28
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:624
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2066
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
Definition: Native.java:855
FuncDecl[] getTesterDecls()
Definition: EnumSort.java:52