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.Diagnostics;
21 using System;
22
23 namespace Microsoft.Z3
24{
28 public class ListSort : Sort
29 {
33 public FuncDecl NilDecl
34 {
35 get
36 {
37 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));
38 }
39 }
40
44 public Expr Nil
45 {
46 get
47 {
48 return Context.MkApp(NilDecl);
49 }
50 }
51
55 public FuncDecl IsNilDecl
56 {
57 get
58 {
59 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
60 }
61 }
62
66 public FuncDecl ConsDecl
67 {
68 get
69 {
70 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
71 }
72 }
73
78 public FuncDecl IsConsDecl
79 {
80 get
81 {
82 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
83 }
84 }
85
89 public FuncDecl HeadDecl
90 {
91 get
92 {
93 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
94 }
95 }
96
100 public FuncDecl TailDecl
101 {
102 get
103 {
104 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
105 }
106 }
107
108 #region Internal
109 internal ListSort(Context ctx, Symbol name, Sort elemSort)
110 : base(ctx, IntPtr.Zero)
111 {
112 Debug.Assert(ctx != null);
113 Debug.Assert(name != null);
114 Debug.Assert(elemSort != null);
115
116 IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero,
117 icons = IntPtr.Zero, iiscons = IntPtr.Zero,
118 ihead = IntPtr.Zero, itail = IntPtr.Zero;
119
120 NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
121 ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
122 }
123 #endregion
124 };
125}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Microsoft.Z3.Expr
Expressions are terms.
Definition: Expr.cs:31
Microsoft.Z3.FuncDecl
Function declarations.
Definition: FuncDecl.cs:31
Microsoft.Z3.ListSort
List sorts.
Definition: ListSort.cs:29
Microsoft.Z3.ListSort.HeadDecl
FuncDecl HeadDecl
The declaration of the head function of this list sort.
Definition: ListSort.cs:90
Microsoft.Z3.ListSort.IsConsDecl
FuncDecl IsConsDecl
The declaration of the isCons function of this list sort.
Definition: ListSort.cs:79
Microsoft.Z3.ListSort.NilDecl
FuncDecl NilDecl
The declaration of the nil function of this list sort.
Definition: ListSort.cs:34
Microsoft.Z3.ListSort.TailDecl
FuncDecl TailDecl
The declaration of the tail function of this list sort.
Definition: ListSort.cs:101
Microsoft.Z3.ListSort.IsNilDecl
FuncDecl IsNilDecl
The declaration of the isNil function of this list sort.
Definition: ListSort.cs:56
Microsoft.Z3.ListSort.Nil
Expr Nil
The empty list.
Definition: ListSort.cs:45
Microsoft.Z3.ListSort.ConsDecl
FuncDecl ConsDecl
The declaration of the cons function of this list sort.
Definition: ListSort.cs:67
Microsoft.Z3.Sort
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Microsoft.Z3.Symbol
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Microsoft.Z3
Definition: AlgebraicNum.cs:27