Z3
ListSort.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 ListSort.cs
7
8Abstract:
9
10 Z3 Managed API: List Sorts
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class ListSort : Sort
29 {
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
56 {
57 get
58 {
59 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
60 }
61 }
62
67 {
68 get
69 {
70 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
71 }
72 }
73
79 {
80 get
81 {
82 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
83 }
84 }
85
90 {
91 get
92 {
93 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
94 }
95 }
96
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}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Expressions are terms.
Definition: Expr.cs:31
Function declarations.
Definition: FuncDecl.cs:31
FuncDecl HeadDecl
The declaration of the head function of this list sort.
Definition: ListSort.cs:90
FuncDecl IsConsDecl
The declaration of the isCons function of this list sort.
Definition: ListSort.cs:79
FuncDecl NilDecl
The declaration of the nil function of this list sort.
Definition: ListSort.cs:34
FuncDecl TailDecl
The declaration of the tail function of this list sort.
Definition: ListSort.cs:101
FuncDecl IsNilDecl
The declaration of the isNil function of this list sort.
Definition: ListSort.cs:56
Expr Nil
The empty list.
Definition: ListSort.cs:45
FuncDecl ConsDecl
The declaration of the cons function of this list sort.
Definition: ListSort.cs:67
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