Z3 |

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.Diagnostics;
20 using System;
21
22#if !FRAMEWORK_LT_4
23 using System.Numerics;
24#endif
25
26 namespace Microsoft.Z3
27{
31 public class RatNum : RealExpr
32 {
36 public IntNum Numerator
37 {
38 get
39 {
40
41 return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject));
42 }
43 }
44
48 public IntNum Denominator
49 {
50 get
51 {
52
53 return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject));
54 }
55 }
56
57#if !FRAMEWORK_LT_4
61 public BigInteger BigIntNumerator
62 {
63 get
64 {
65 IntNum n = Numerator;
66 return BigInteger.Parse(n.ToString());
67 }
68 }
69
73 public BigInteger BigIntDenominator
74 {
75 get
76 {
77 IntNum n = Denominator;
78 return BigInteger.Parse(n.ToString());
79 }
80 }
81#endif
82
87 public string ToDecimalString(uint precision)
88 {
89 return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
90 }
91
95 public double Double
96 {
97 get { return Native.Z3_get_numeral_double(Context.nCtx, NativeObject); }
98 }
99
103 public override string ToString()
104 {
105 return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
106 }
107
108 #region Internal
109 internal RatNum(Context ctx, IntPtr obj)
110 : base(ctx, obj)
111 {
112 Debug.Assert(ctx != null);
113 }
114 #endregion
115 }
116}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.IntNum
Integer Numerals
Definition: IntNum.cs:32
Microsoft.Z3.IntNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition: IntNum.cs:115
Microsoft.Z3.RatNum
Rational Numerals
Definition: RatNum.cs:32
Microsoft.Z3.RatNum.BigIntNumerator
BigInteger BigIntNumerator
Converts the numerator of the rational to a BigInteger
Definition: RatNum.cs:62
Microsoft.Z3.RatNum.Double
double Double
Returns a double representing the value.
Definition: RatNum.cs:96
Microsoft.Z3.RatNum.BigIntDenominator
BigInteger BigIntDenominator
Converts the denominator of the rational to a BigInteger
Definition: RatNum.cs:74
Microsoft.Z3.RatNum.Numerator
IntNum Numerator
The numerator of a rational numeral.
Definition: RatNum.cs:37
Microsoft.Z3.RatNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition: RatNum.cs:103
Microsoft.Z3.RatNum.ToDecimalString
string ToDecimalString(uint precision)
Returns a string representation in decimal notation.
Definition: RatNum.cs:87
Microsoft.Z3.RatNum.Denominator
IntNum Denominator
The denominator of a rational numeral.
Definition: RatNum.cs:49
Microsoft.Z3.RealExpr
Real expressions
Definition: RealExpr.cs:32
Microsoft.Z3
Definition: AlgebraicNum.cs:27