Z3 |

EnumSort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23@SuppressWarnings("unchecked")
24public class EnumSort<R> extends Sort
25{
30 public FuncDecl<EnumSort<R>>[] getConstDecls()
31 {
32 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
33 FuncDecl<?>[] t = new FuncDecl[n];
34 for (int i = 0; i < n; i++)
35 t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
36 return (FuncDecl<EnumSort<R>>[]) t;
37 }
38
43 public FuncDecl<EnumSort<R>> getConstDecl(int inx)
44 {
45 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
46 }
47
53 public Expr<EnumSort<R>>[] getConsts()
54 {
55 FuncDecl<?>[] cds = getConstDecls();
56 Expr<?>[] t = new Expr[cds.length];
57 for (int i = 0; i < t.length; i++)
58 t[i] = getContext().mkApp(cds[i]);
59 return (Expr<EnumSort<R>>[]) t;
60 }
61
67 public Expr<EnumSort<R>> getConst(int inx)
68 {
69 return getContext().mkApp(getConstDecl(inx));
70 }
71
76 @SuppressWarnings("unchecked")
77 public FuncDecl<BoolSort>[] getTesterDecls()
78 {
79 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
80 FuncDecl<BoolSort>[] t = new FuncDecl[n];
81 for (int i = 0; i < n; i++)
82 t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
83 return t;
84 }
85
90 public FuncDecl<BoolSort> getTesterDecl(int inx)
91 {
92 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
93 }
94
95 EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
96 {
97 super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
98 name.getNativeObject(), enumNames.length,
99 Symbol.arrayToNative(enumNames),
100 new long[enumNames.length], new long[enumNames.length]));
101 }
102};
com.microsoft.z3.BoolSort
Definition: BoolSort.java:24
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.EnumSort
Definition: EnumSort.java:25
com.microsoft.z3.EnumSort.getConst
Expr< EnumSort< R > > getConst(int inx)
Definition: EnumSort.java:67
com.microsoft.z3.EnumSort.getConstDecl
FuncDecl< EnumSort< R > > getConstDecl(int inx)
Definition: EnumSort.java:43
com.microsoft.z3.EnumSort.getTesterDecl
FuncDecl< BoolSort > getTesterDecl(int inx)
Definition: EnumSort.java:90
com.microsoft.z3.EnumSort.getConsts
Expr< EnumSort< R > >[] getConsts()
Definition: EnumSort.java:53
com.microsoft.z3.EnumSort.getConstDecls
FuncDecl< EnumSort< R > >[] getConstDecls()
Definition: EnumSort.java:30
com.microsoft.z3.Expr
Definition: Expr.java:35
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
z3py.EnumSort
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5317