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;
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 }
override string ToString()
Returns a string representation of the numeral.
Definition: IntNum.cs:116
string ToDecimalString(uint precision)
Returns a string representation in decimal notation.
Definition: RatNum.cs:90
override string ToString()
Returns a string representation of the numeral.
Definition: RatNum.cs:98
Integer Numerals
Definition: IntNum.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Rational Numerals
Definition: RatNum.cs:32
Real expressions
Definition: RealExpr.cs:31