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 };
com.microsoft.z3.Native.mkEnumerationSort
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
Definition: Native.java:1026
com.microsoft.z3.EnumSort.getTesterDecls
FuncDecl[] getTesterDecls()
Definition: EnumSort.java:75
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.Native.getDatatypeSortRecognizer
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2785
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.EnumSort.getConstDecls
FuncDecl[] getConstDecls()
Definition: EnumSort.java:29
com.microsoft.z3.EnumSort.getConst
Expr getConst(int inx)
Definition: EnumSort.java:66
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.getDatatypeSortNumConstructors
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2767
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.EnumSort
Definition: EnumSort.java:23
com.microsoft.z3.EnumSort.getTesterDecl
FuncDecl getTesterDecl(int inx)
Definition: EnumSort.java:88
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.EnumSort.getConstDecl
FuncDecl getConstDecl(int inx)
Definition: EnumSort.java:42
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Native.getDatatypeSortConstructor
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2776
com.microsoft.z3.EnumSort.getConsts
Expr[] getConsts()
Definition: EnumSort.java:52