/// <summary>
 /// Conversion of a floating-point term into a real-numbered term.
 /// </summary>
 /// <remarks>
 /// Produces a term that represents the conversion of the floating-poiunt term t into a
 /// real number. Note that this type of conversion will often result in non-linear 
 /// constraints over real terms.
 /// </remarks>        
 /// <param name="t">FloatingPoint term</param>
 public RealExpr MkFPToReal(FPExpr t)
 {
     Contract.Ensures(Contract.Result<RealExpr>() != null);
     return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
 }

 /// <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>
 /// Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
 /// </summary>
 /// <remarks>
 /// The size of the resulting bit-vector is automatically determined. Note that 
 /// IEEE 754-2008 allows multiple different representations of NaN. This conversion 
 /// knows only one NaN and it will always produce the same bit-vector represenatation of 
 /// that NaN. 
 /// </remarks>
 /// <param name="t">FloatingPoint term.</param>
 public BitVecExpr MkFPToIEEEBV(FPExpr t)
 {
     Contract.Ensures(Contract.Result<BitVecExpr>() != null);
     return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
 }

 /// <summary>
 /// Floating-point subtraction
 /// </summary>
 /// <param name="rm">rounding mode term</param>
 /// <param name="t1">floating-point term</param>
 /// <param name="t2">floating-point term</param>
 public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
 {
     Contract.Ensures(Contract.Result<FPNum>() != null);
     return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
 }

 /// <summary>
 /// Conversion of a floating-point term into a bit-vector.
 /// </summary>
 /// <remarks>
 /// Produces a term that represents the conversion of the floating-poiunt term t into a
 /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
 /// the result will be rounded according to rounding mode rm.
 /// </remarks>        
 /// <param name="rm">RoundingMode term.</param>
 /// <param name="t">FloatingPoint term</param>
 /// <param name="sz">Size of the resulting bit-vector.</param>
 /// <param name="signed">Indicates whether the result is a signed or unsigned bit-vector.</param>
 public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
 {
     Contract.Ensures(Contract.Result<BitVecExpr>() != null);
     if (signed)
         return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
     else
         return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
 }

 /// <summary>
 /// Floating-point roundToIntegral. Rounds a floating-point number to 
 /// the closest integer, again represented as a floating-point number.
 /// </summary>        
 /// <param name="rm">term of RoundingMode sort</param>
 /// <param name="t">floating-point term</param>
 public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
 {
     Contract.Ensures(Contract.Result<FPNum>() != null);
     return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
 }

 /// <summary>
 /// Floating-point negation
 /// </summary>
 /// <param name="t">floating-point term</param>
 public FPExpr MkFPNeg(FPExpr t)
 {
     Contract.Ensures(Contract.Result<FPNum>() != null);
     return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
 }

 /// <summary>
 /// Floating-point less than.
 /// </summary>        
 /// <param name="t1">floating-point term</param>
 /// <param name="t2">floating-point term</param>
 public BoolExpr MkFPLt(FPExpr t1, FPExpr t2)
 {
     Contract.Ensures(Contract.Result<BoolExpr>() != null);
     return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
 }

 /// <summary>
 /// Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
 /// </summary>        
 /// <param name="t">floating-point term</param>        
 public BoolExpr MkFPIsZero(FPExpr t)
 {
     Contract.Ensures(Contract.Result<BoolExpr>() != null);
     return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
 }

 /// <summary>
 /// Translates an ASTVector into a FPExpr[]
 /// </summary>    
 public FPExpr[] ToFPExprArray()
 {
     uint n = Size;
     FPExpr[] res = new FPExpr[n];
     for (uint i = 0; i < n; i++)
         res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
     return res;
 }