Z3
AlgebraicNum.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 AlgebraicNum : ArithExpr
33  {
41  public RatNum ToUpper(uint precision)
42  {
43  Contract.Ensures(Contract.Result<RatNum>() != null);
44 
45  return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
46  }
47 
55  public RatNum ToLower(uint precision)
56  {
57  Contract.Ensures(Contract.Result<RatNum>() != null);
58 
59  return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
60  }
61 
66  public string ToDecimal(uint precision)
67  {
68  Contract.Ensures(Contract.Result<string>() != null);
69 
70  return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
71  }
72 
73  #region Internal
74  internal AlgebraicNum(Context ctx, IntPtr obj)
75  : base(ctx, obj)
76  {
77  Contract.Requires(ctx != null);
78  }
79  #endregion
80  }
81 }
RatNum ToUpper(uint precision)
Return a upper bound for a given real algebraic number. The interval isolating the number is smaller ...
Definition: AlgebraicNum.cs:41
string ToDecimal(uint precision)
Returns a string representation in decimal notation.
Definition: AlgebraicNum.cs:66
RatNum ToLower(uint precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Definition: AlgebraicNum.cs:55
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
Rational Numerals
Definition: RatNum.cs:32
Algebraic numbers
Definition: AlgebraicNum.cs:32