mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

FPA API bugfix

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-10 20:04:24 +00:00
parent c2b5b6a36b
commit 72dbb2a513
2 changed files with 1 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/api/dotnet/Context.cs
View file

@ -3788,19 +3788,6 @@ namespace Microsoft.Z3
return new FPExpr(this, Native.Z3_mk_fpa_convert(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject)); return new FPExpr(this, Native.Z3_mk_fpa_convert(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
} }
/// <summary>
/// Conversion of a floating point term to a bit-vector term in IEEE754 format.
/// </summary>
/// <remarks>
/// The size of the resulting bit-vector is automatically determined.
/// </remarks>
/// <param name="t">floating point term</param>
public FPExpr MkFPToIEEEBV(FPExpr t)
{
Contract.Ensures(Contract.Result<FPNum>() != null);
return new FPExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
}
#endregion #endregion
#region Miscellaneous #region Miscellaneous

2
src/ast/fpa/fpa2bv_converter.h
View file

@ -73,7 +73,7 @@ public:
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
SASSERT(m_bv_util.is_bv(significand)); SASSERT(m_bv_util.is_bv(significand));
SASSERT(m_bv_util.is_bv(exponent)); SASSERT(m_bv_util.is_bv(exponent));
result = m.mk_app(m_util.get_family_id(), OP_FLOAT_FP, sign, significand, exponent); result = m.mk_app(m_util.get_family_id(), OP_FLOAT_TO_FP, sign, significand, exponent);
} }
void mk_eq(expr * a, expr * b, expr_ref & result); void mk_eq(expr * a, expr * b, expr_ref & result);