Z3
EnumSort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  EnumSort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Enum Sorts
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-11-23
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class EnumSort : Sort
30  {
34  public FuncDecl[] ConstDecls
35  {
36  get
37  {
38  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
39  uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
40  FuncDecl[] t = new FuncDecl[n];
41  for (uint i = 0; i < n; i++)
42  t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
43  return t;
44  }
45  }
46 
52  public FuncDecl ConstDecl(uint inx)
53  {
54  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
55  }
56 
60  public Expr[] Consts
61  {
62  get
63  {
64  Contract.Ensures(Contract.Result<Expr[]>() != null);
65  FuncDecl[] cds = ConstDecls;
66  Expr[] t = new Expr[cds.Length];
67  for (uint i = 0; i < t.Length; i++)
68  t[i] = Context.MkApp(cds[i]);
69  return t;
70  }
71  }
72 
78  public Expr Const(uint inx)
79  {
80  return Context.MkApp(ConstDecl(inx));
81  }
82 
86  public FuncDecl[] TesterDecls
87  {
88  get
89  {
90  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
91  uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
92  FuncDecl[] t = new FuncDecl[n];
93  for (uint i = 0; i < n; i++)
94  t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
95  return t;
96  }
97  }
98 
104  public FuncDecl TesterDecl(uint inx)
105  {
106  return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
107  }
108 
109  #region Internal
110  internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
111  : base(ctx, IntPtr.Zero)
112  {
113  Contract.Requires(ctx != null);
114  Contract.Requires(name != null);
115  Contract.Requires(enumNames != null);
116 
117  int n = enumNames.Length;
118  IntPtr[] n_constdecls = new IntPtr[n];
119  IntPtr[] n_testers = new IntPtr[n];
120  NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
121  Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
122  }
123  #endregion
124  };
125 }
FuncDecl ConstDecl(uint inx)
Retrieves the inx&#39;th constant declaration in the enumeration.
Definition: EnumSort.cs:52
def Consts(names, sort)
Definition: z3py.py:1204
Expressions are terms.
Definition: Expr.cs:29
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:807
Expr Const(uint inx)
Retrieves the inx&#39;th constant in the enumeration.
Definition: EnumSort.cs:78
Enumeration sorts.
Definition: EnumSort.cs:29
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Function declarations.
Definition: FuncDecl.cs:29
FuncDecl TesterDecl(uint inx)
Retrieves the inx&#39;th tester/recognizer declaration in the enumeration.
Definition: EnumSort.cs:104