Z3
ListSort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  ListSort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: List 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 ListSort : Sort
30  {
34  public FuncDecl NilDecl
35  {
36  get
37  {
38  Contract.Ensures(Contract.Result<FuncDecl>() != null);
39  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));
40  }
41  }
42 
46  public Expr Nil
47  {
48  get
49  {
50  Contract.Ensures(Contract.Result<Expr>() != null);
51  return Context.MkApp(NilDecl);
52  }
53  }
54 
58  public FuncDecl IsNilDecl
59  {
60  get
61  {
62  Contract.Ensures(Contract.Result<FuncDecl>() != null);
63  return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
64  }
65  }
66 
70  public FuncDecl ConsDecl
71  {
72  get
73  {
74  Contract.Ensures(Contract.Result<FuncDecl>() != null);
75  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
76  }
77  }
78 
83  public FuncDecl IsConsDecl
84  {
85  get
86  {
87  Contract.Ensures(Contract.Result<FuncDecl>() != null);
88  return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
89  }
90  }
91 
95  public FuncDecl HeadDecl
96  {
97  get
98  {
99  Contract.Ensures(Contract.Result<FuncDecl>() != null);
100  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
101  }
102  }
103 
107  public FuncDecl TailDecl
108  {
109  get
110  {
111  Contract.Ensures(Contract.Result<FuncDecl>() != null);
112  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
113  }
114  }
115 
116  #region Internal
117  internal ListSort(Context ctx, Symbol name, Sort elemSort)
118  : base(ctx, IntPtr.Zero)
119  {
120  Contract.Requires(ctx != null);
121  Contract.Requires(name != null);
122  Contract.Requires(elemSort != null);
123 
124  IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero,
125  icons = IntPtr.Zero, iiscons = IntPtr.Zero,
126  ihead = IntPtr.Zero, itail = IntPtr.Zero;
127 
128  NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
129  ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
130  }
131  #endregion
132  };
133 }
List sorts.
Definition: ListSort.cs:29
Expressions are terms.
Definition: Expr.cs:29
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:807
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