Z3
FPNum.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6  FPNum.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Floating Point Numerals
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2013-06-10
15 
16 Notes:
17 
18 --*/
19 using System;
20 using System.Diagnostics.Contracts;
21 
22 namespace Microsoft.Z3
23 {
27  [ContractVerification(true)]
28  public class FPNum : FPExpr
29  {
36  public bool Sign
37  {
38  get
39  {
40  int res = 0;
41  if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
42  throw new Z3Exception("Sign is not a Boolean value");
43  return res != 0;
44  }
45  }
46 
54  public string Significand
55  {
56  get
57  {
58  return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
59  }
60  }
61 
65  public string Exponent
66  {
67  get
68  {
69  return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
70  }
71  }
72 
76  public Int64 ExponentInt64
77  {
78  get
79  {
80  Int64 result = 0;
81  if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
82  throw new Z3Exception("Exponent is not a 64 bit integer");
83  return result;
84  }
85  }
86 
87  #region Internal
88  internal FPNum(Context ctx, IntPtr obj)
89  : base(ctx, obj)
90  {
91  Contract.Requires(ctx != null);
92  }
93  #endregion
94 
98  public override string ToString()
99  {
100  return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
101  }
102  }
103 }
FloatiungPoint Numerals
Definition: FPNum.cs:28
static string Z3_fpa_get_numeral_exponent_string(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6555
static string Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3541
override string ToString()
Returns a string representation of the numeral.
Definition: FPNum.cs:98
FloatingPoint Expressions
Definition: FPExpr.cs:31
static string Z3_fpa_get_numeral_significand_string(Z3_context a0, Z3_ast a1)
Definition: Native.cs:6547
static int Z3_fpa_get_numeral_exponent_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
Definition: Native.cs:6563
static int Z3_fpa_get_numeral_sign(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
Definition: Native.cs:6539
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27