diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2015-11-29 14:28:17 -0700 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2015-11-29 14:28:17 -0700 |
| commit | a1c9e11736bda4bf8ea4bf431523b9b975b01670 (patch) | |
| tree | 7cb10a22d54fa41c535f96299c76e06bae6953a8 /Source/Provers | |
| parent | a3b2bfa16f991f4d5f844b6d18e836e57b4195a1 (diff) | |
Special fp types (such as infinity and NaN are now translated by boogie
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 629f7e2d..7c3ae960 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -204,7 +204,11 @@ namespace Microsoft.Boogie.SMTLib else if (node is VCExprFloatLit)
{
BigFloat lit = ((VCExprFloatLit)node).Val;
- wr.Write(("((_ to_fp 8 24) roundTowardZero "));
+ if (lit.IsSpecialType) {
+ wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ")");
+ return true;
+ }
+ wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ") RNE ");
if (lit.IsNegative)
// In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
@@ -620,31 +624,31 @@ namespace Microsoft.Boogie.SMTLib public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("fp.add roundTowardZero", node, options);
+ WriteApplication("fp.add RNE", node, options);
return true;
}
public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("fp.sub roundTowardZero", node, options);
+ WriteApplication("fp.sub RNE", node, options);
return true;
}
public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("fp.mul roundTowardZero", node, options);
+ WriteApplication("fp.mul RNE", node, options);
return true;
}
public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("fp.div roundTowardZero", node, options);
+ WriteApplication("fp.div RNE", node, options);
return true;
}
public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("fp.rem roundTowardZero", node, options);
+ WriteApplication("fp.rem RNE", node, options);
return true;
}
|