Z3
EnumSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public 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};
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
FuncDecl[] getConstDecls()
Definition: EnumSort.java:29
Expr getConst(int inx)
Definition: EnumSort.java:66
FuncDecl getConstDecl(int inx)
Definition: EnumSort.java:42
FuncDecl getTesterDecl(int inx)
Definition: EnumSort.java:88
FuncDecl[] getTesterDecls()
Definition: EnumSort.java:75
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
Definition: Native.java:1024
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2765
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2774
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2783