Z3
RatNum.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 IntNum.cs
7
8Abstract:
9
10 Z3 Managed API: Int Numerals
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-20
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21
22#if !FRAMEWORK_LT_4
23using System.Numerics;
24#endif
25
26namespace Microsoft.Z3
27{
31 public class RatNum : RealExpr
32 {
37 {
38 get
39 {
40
41 return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject));
42 }
43 }
44
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 {
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}
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Integer Numerals
Definition: IntNum.cs:32
override string ToString()
Returns a string representation of the numeral.
Definition: IntNum.cs:115
Rational Numerals
Definition: RatNum.cs:32
BigInteger BigIntNumerator
Converts the numerator of the rational to a BigInteger
Definition: RatNum.cs:62
double Double
Returns a double representing the value.
Definition: RatNum.cs:96
BigInteger BigIntDenominator
Converts the denominator of the rational to a BigInteger
Definition: RatNum.cs:74
IntNum Numerator
The numerator of a rational numeral.
Definition: RatNum.cs:37
override string ToString()
Returns a string representation of the numeral.
Definition: RatNum.cs:103
string ToDecimalString(uint precision)
Returns a string representation in decimal notation.
Definition: RatNum.cs:87
IntNum Denominator
The denominator of a rational numeral.
Definition: RatNum.cs:49
Real expressions
Definition: RealExpr.cs:32