20 using System.Diagnostics.Contracts;
27 [ContractVerification(
true)]
42 throw new Z3Exception(
"Sign is not a Boolean value");
54 public string Significand
70 public UInt64 SignificandUInt64
76 throw new Z3Exception(
"Significand is not a 64 bit unsigned integer");
84 public string Exponent
95 public Int64 ExponentInt64
101 throw new Z3Exception(
"Exponent is not a 64 bit integer");
110 Contract.Requires(ctx != null);
static string Z3_fpa_get_numeral_exponent_string(Z3_context a0, Z3_ast a1)
static string Z3_get_numeral_string(Z3_context a0, Z3_ast a1)
override string ToString()
Returns a string representation of the numeral.
static int Z3_fpa_get_numeral_significand_uint64(Z3_context a0, Z3_ast a1, [In, Out] ref UInt64 a2)
FloatingPoint Expressions
static string Z3_fpa_get_numeral_significand_string(Z3_context a0, Z3_ast a1)
static int Z3_fpa_get_numeral_exponent_int64(Z3_context a0, Z3_ast a1, [In, Out] ref Int64 a2)
static int Z3_fpa_get_numeral_sign(Z3_context a0, Z3_ast a1, [In, Out] ref int a2)
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3