Z3
src
api
dotnet
TupleSort.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2012 Microsoft Corporation
3
4
Module Name:
5
6
TupleSort.cs
7
8
Abstract:
9
10
Z3 Managed API: Tuple Sorts
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2012-11-23
15
16
Notes:
17
18
--*/
19
20
using
System;
21
using
System.Diagnostics;
22
23
namespace
Microsoft.Z3
24
{
28
public
class
TupleSort
:
Sort
29
{
33
public
FuncDecl
MkDecl
34
{
35
get
36
{
37
38
return
new
FuncDecl
(
Context
, Native.Z3_get_tuple_sort_mk_decl(
Context
.nCtx, NativeObject));
39
}
40
}
41
45
public
uint
NumFields
46
{
47
get
{
return
Native.Z3_get_tuple_sort_num_fields(
Context
.nCtx, NativeObject); }
48
}
49
53
public
FuncDecl
[]
FieldDecls
54
{
55
get
56
{
57
58
uint n =
NumFields
;
59
FuncDecl
[] res =
new
FuncDecl
[n];
60
for
(uint i = 0; i < n; i++)
61
res[i] =
new
FuncDecl
(
Context
, Native.Z3_get_tuple_sort_field_decl(
Context
.nCtx, NativeObject, i));
62
return
res;
63
}
64
}
65
66
#region Internal
67
internal
TupleSort
(
Context
ctx,
Symbol
name, uint numFields,
Symbol
[] fieldNames,
Sort
[] fieldSorts)
68
: base(ctx, IntPtr.Zero)
69
{
70
Debug.Assert(ctx !=
null
);
71
Debug.Assert(name !=
null
);
72
73
IntPtr t = IntPtr.Zero;
74
IntPtr[] f =
new
IntPtr[numFields];
75
NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
76
Symbol
.ArrayToNative(fieldNames),
AST
.ArrayToNative(fieldSorts),
77
ref t, f);
78
}
79
#endregion
80
};
81
}
Microsoft.Z3.AST
The abstract syntax tree (AST) class.
Definition:
AST.cs:31
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:32
Microsoft.Z3.FuncDecl
Function declarations.
Definition:
FuncDecl.cs:31
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.TupleSort
Tuple sorts.
Definition:
TupleSort.cs:29
Microsoft.Z3.TupleSort.NumFields
uint NumFields
The number of fields in the tuple.
Definition:
TupleSort.cs:46
Microsoft.Z3.TupleSort.MkDecl
FuncDecl MkDecl
The constructor function of the tuple.
Definition:
TupleSort.cs:34
Microsoft.Z3.TupleSort.FieldDecls
FuncDecl[] FieldDecls
The field declarations.
Definition:
TupleSort.cs:54
Microsoft.Z3
Definition:
AlgebraicNum.cs:27
Generated on Sat Jun 4 2022 15:24:57 for Z3 by
1.9.3