/// <summary>
 /// Create a floating-point zero of sort s.
 /// </summary>        
 /// <param name="s">FloatingPoint sort.</param>   
 /// <param name="negative">indicates whether the result should be negative.</param>
 public FPNum MkFPZero(FPSort s, bool negative)
 {
     Contract.Ensures(Contract.Result<FPRMExpr>() != null);
     return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
 }

 /// <summary>
 /// Conversion of a floating-point number to another FloatingPoint sort s.
 /// </summary>
 /// <remarks>
 /// Produces a term that represents the conversion of a floating-point term t to a different
 /// FloatingPoint sort s. If necessary, rounding according to rm is applied. 
 /// </remarks>
 /// <param name="s">FloatingPoint sort</param>
 /// <param name="rm">floating-point rounding mode term</param>
 /// <param name="t">floating-point term</param>
 public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
 {
     Contract.Ensures(Contract.Result<FPExpr>() != null);
     return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
 }

 /// <summary>
 /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
 /// </summary>        
 /// <param name="sgn">the sign.</param>
 /// <param name="sig">the significand.</param>
 /// <param name="exp">the exponent.</param>
 /// <param name="s">FloatingPoint sort.</param>        
 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
 {
     Contract.Ensures(Contract.Result<FPRMExpr>() != null);
     return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
 }

 /// <summary>
 /// Create a NaN of sort s.
 /// </summary>        
 /// <param name="s">FloatingPoint sort.</param>        
 public FPNum MkFPNaN(FPSort s)
 {
     Contract.Ensures(Contract.Result<FPRMExpr>() != null);
     return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
 }

 /// <summary>
 /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
 /// </summary>        
 /// <param name="sgn">the sign.</param>        
 /// <param name="exp">the exponent.</param>
 /// <param name="sig">the significand.</param>
 /// <param name="s">FloatingPoint sort.</param>        
 public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
 {
     Contract.Ensures(Contract.Result<FPRMExpr>() != null);
     return MkFPNumeral(sgn, exp, sig, s);
 }