Z3
src
api
dotnet
RatNum.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2012 Microsoft Corporation
3
4
Module Name:
5
6
IntNum.cs
7
8
Abstract:
9
10
Z3 Managed API: Int Numerals
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2012-03-20
15
16
Notes:
17
18
--*/
19
using
System
;
20
using
System
.
Diagnostics
.
Contracts
;
21
22
#if !FRAMEWORK_LT_4
23
using
System
.Numerics;
24
#endif
25
26
namespace
Microsoft
.Z3
27
{
31
[
ContractVerification
(
true
)]
32
public
class
RatNum
:
RealExpr
33
{
37
public
IntNum
Numerator
38
{
39
get
40
{
41
Contract.Ensures(Contract.Result<
IntNum
>() != null);
42
43
return
new
IntNum
(
Context
, Native.Z3_get_numerator(
Context
.nCtx, NativeObject));
44
}
45
}
46
50
public
IntNum
Denominator
51
{
52
get
53
{
54
Contract.Ensures(Contract.Result<
IntNum
>() != null);
55
56
return
new
IntNum
(
Context
, Native.Z3_get_denominator(
Context
.nCtx, NativeObject));
57
}
58
}
59
60
#if !FRAMEWORK_LT_4
61
public
BigInteger BigIntNumerator
65
{
66
get
67
{
68
IntNum
n = Numerator;
69
return
BigInteger.Parse(n.
ToString
());
70
}
71
}
72
76
public
BigInteger BigIntDenominator
77
{
78
get
79
{
80
IntNum
n = Denominator;
81
return
BigInteger.Parse(n.
ToString
());
82
}
83
}
84
#endif
85
90
public
string
ToDecimalString
(uint precision)
91
{
92
return
Native.Z3_get_numeral_decimal_string(
Context
.nCtx, NativeObject, precision);
93
}
94
98
public
override
string
ToString
()
99
{
100
return
Native.Z3_get_numeral_string(
Context
.nCtx, NativeObject);
101
}
102
103
#region Internal
104
internal
RatNum
(
Context
ctx, IntPtr obj)
105
: base(ctx, obj)
106
{
107
Contract.Requires(ctx != null);
108
}
109
#endregion
110
}
111
}
Microsoft.Z3.IntNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition:
IntNum.cs:116
Microsoft.Z3.RatNum.ToDecimalString
string ToDecimalString(uint precision)
Returns a string representation in decimal notation.
Definition:
RatNum.cs:90
System
System.Diagnostics
Microsoft
System.Diagnostics.Contracts.ContractVerification
Definition:
DummyContracts.cs:38
Microsoft.Z3.RatNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition:
RatNum.cs:98
Microsoft.Z3.IntNum
Integer Numerals
Definition:
IntNum.cs:32
System.Diagnostics.Contracts
Definition:
DummyContracts.cs:21
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:32
Microsoft.Z3.RatNum
Rational Numerals
Definition:
RatNum.cs:32
Microsoft.Z3.RealExpr
Real expressions
Definition:
RealExpr.cs:31
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12