Z3
src
api
dotnet
FPNum.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2013 Microsoft Corporation
3
4
Module Name:
5
6
FPNum.cs
7
8
Abstract:
9
10
Z3 Managed API: Floating Point Numerals
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2013-06-10
15
16
Notes:
17
18
--*/
19
using
System
;
20
using
System
.Diagnostics.Contracts;
21
22
namespace
Microsoft
.Z3
23
{
27
[ContractVerification(
true
)]
28
public
class
FPNum
:
FPExpr
29
{
36
public
bool
Sign
37
{
38
get
39
{
40
int
res = 0;
41
if
(
Native
.
Z3_fpa_get_numeral_sign
(
Context
.nCtx, NativeObject, ref res) == 0)
42
throw
new
Z3Exception
(
"Sign is not a Boolean value"
);
43
return
res != 0;
44
}
45
}
46
54
public
string
Significand
55
{
56
get
57
{
58
return
Native
.
Z3_fpa_get_numeral_significand_string
(
Context
.nCtx, NativeObject);
59
}
60
}
61
65
public
string
Exponent
66
{
67
get
68
{
69
return
Native
.
Z3_fpa_get_numeral_exponent_string
(
Context
.nCtx, NativeObject);
70
}
71
}
72
76
public
Int64 ExponentInt64
77
{
78
get
79
{
80
Int64 result = 0;
81
if
(
Native
.
Z3_fpa_get_numeral_exponent_int64
(
Context
.nCtx, NativeObject, ref result) == 0)
82
throw
new
Z3Exception
(
"Exponent is not a 64 bit integer"
);
83
return
result;
84
}
85
}
86
87
#region Internal
88
internal
FPNum
(
Context
ctx, IntPtr obj)
89
: base(ctx, obj)
90
{
91
Contract.Requires(ctx != null);
92
}
93
#endregion
94
98
public
override
string
ToString
()
99
{
100
return
Native
.
Z3_get_numeral_string
(
Context
.nCtx, NativeObject);
101
}
102
}
103
}
Microsoft.Z3.FPNum
FloatiungPoint Numerals
Definition:
FPNum.cs:28
Microsoft.Z3.Native.Z3_fpa_get_numeral_exponent_string
static string Z3_fpa_get_numeral_exponent_string(Z3_context a0, Z3_ast a1)
Definition:
Native.cs:6555
Microsoft.Z3.Native
Definition:
Native.cs:39
Microsoft.Z3.Native.Z3_get_numeral_string
static string Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
Definition:
Native.cs:3541
System
Microsoft
Microsoft.Z3.FPNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition:
FPNum.cs:98
Microsoft.Z3.FPExpr
FloatingPoint Expressions
Definition:
FPExpr.cs:31
Microsoft.Z3.Native.Z3_fpa_get_numeral_significand_string
static string Z3_fpa_get_numeral_significand_string(Z3_context a0, Z3_ast a1)
Definition:
Native.cs:6547
Microsoft.Z3.Native.Z3_fpa_get_numeral_exponent_int64
static int Z3_fpa_get_numeral_exponent_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
Definition:
Native.cs:6563
Microsoft.Z3.Native.Z3_fpa_get_numeral_sign
static int Z3_fpa_get_numeral_sign(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
Definition:
Native.cs:6539
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:31
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition:
Z3Exception.cs:27
Generated on Tue Jun 2 2015 00:02:06 for Z3 by
1.8.9.1