Z3
FPSort.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2013 Microsoft Corporation
3
4Module Name:
5
6 FPSort.cs
7
8Abstract:
9
10 Z3 Managed API: Floating Point Sorts
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2013-06-10
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21
22namespace Microsoft.Z3
23{
27 public class FPSort : Sort
28 {
32 public uint EBits { get { return Native.Z3_fpa_get_ebits(Context.nCtx, NativeObject); } }
33
37 public uint SBits { get { return Native.Z3_fpa_get_sbits(Context.nCtx, NativeObject); } }
38
39 #region Internal
40 internal FPSort(Context ctx, IntPtr obj)
41 : base(ctx, obj)
42 {
43 Debug.Assert(ctx != null);
44 }
45 internal FPSort(Context ctx, uint ebits, uint sbits)
46 : base(ctx, Native.Z3_mk_fpa_sort(ctx.nCtx, ebits, sbits))
47 {
48 Debug.Assert(ctx != null);
49 }
50 #endregion
51 }
52}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
FloatingPoint sort
Definition: FPSort.cs:28
uint SBits
The number of significand bits.
Definition: FPSort.cs:37
uint EBits
The number of exponent bits.
Definition: FPSort.cs:32
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.