Z3 |

AlgebraicNum.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 AlgebraicNum.cs
7
8 Abstract:
9
10 Z3 Managed API: Algebraic 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 AlgebraicNum : ArithExpr
32 {
40 public RatNum ToUpper(uint precision)
41 {
42
43 return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
44 }
45
53 public RatNum ToLower(uint precision)
54 {
55
56 return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
57 }
58
63 public string ToDecimal(uint precision)
64 {
65
66 return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
67 }
68
69 #region Internal
70 internal AlgebraicNum(Context ctx, IntPtr obj)
71 : base(ctx, obj)
72 {
73 Debug.Assert(ctx != null);
74 }
75 #endregion
76 }
77}
Microsoft.Z3.AlgebraicNum
Algebraic numbers
Definition: AlgebraicNum.cs:32
Microsoft.Z3.AlgebraicNum.ToUpper
RatNum ToUpper(uint precision)
Return a upper bound for a given real algebraic number. The interval isolating the number is smaller ...
Definition: AlgebraicNum.cs:40
Microsoft.Z3.AlgebraicNum.ToLower
RatNum ToLower(uint precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Definition: AlgebraicNum.cs:53
Microsoft.Z3.AlgebraicNum.ToDecimal
string ToDecimal(uint precision)
Returns a string representation in decimal notation.
Definition: AlgebraicNum.cs:63
Microsoft.Z3.ArithExpr
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:32
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
Definition: AlgebraicNum.cs:27