Z3 |

FPSort.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 FPSort.cs
7
8 Abstract:
9
10 Z3 Managed API: Floating Point Sorts
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2013-06-10
15
16 Notes:
17
18--*/
19 using System.Diagnostics;
20 using System;
21
22 namespace 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}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.FPSort
FloatingPoint sort
Definition: FPSort.cs:28
Microsoft.Z3.FPSort.SBits
uint SBits
The number of significand bits.
Definition: FPSort.cs:37
Microsoft.Z3.FPSort.EBits
uint EBits
The number of exponent bits.
Definition: FPSort.cs:32
Microsoft.Z3.Sort
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Microsoft.Z3
Definition: AlgebraicNum.cs:27
Z3_mk_fpa_sort
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.