summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2015-11-29 14:28:17 -0700
committerGravatar Checkmate50 <dgeisler50@gmail.com>2015-11-29 14:28:17 -0700
commita1c9e11736bda4bf8ea4bf431523b9b975b01670 (patch)
tree7cb10a22d54fa41c535f96299c76e06bae6953a8 /Source
parenta3b2bfa16f991f4d5f844b6d18e836e57b4195a1 (diff)
Special fp types (such as infinity and NaN are now translated by boogie
Diffstat (limited to 'Source')
-rw-r--r--Source/Basetypes/BigFloat.cs68
-rw-r--r--Source/Core/Parser.cs4
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs16
3 files changed, 63 insertions, 25 deletions
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index bbc39db4..6cf94feb 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Basetypes
// the internal representation
[Rep]
- internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)
+ internal readonly long mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)
[Rep]
internal readonly int mantissaSize;
[Rep]
@@ -37,7 +37,7 @@ namespace Microsoft.Basetypes
[Rep]
internal readonly bool isDec;
- public BIM Mantissa {
+ public long Mantissa {
get {
return mantissa;
}
@@ -69,17 +69,17 @@ namespace Microsoft.Basetypes
public bool IsDec {
get {
- return IsDec;
+ return isDec;
}
}
public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero
private static readonly BIM two = new BIM(2);
- private static BIM two_n(int n) {
- BIM toReturn = new BIM(1);
+ private static long two_n(int n) {
+ long toReturn = 1;
for (int i = 0; i < n; i++)
- toReturn = toReturn * two;
+ toReturn = toReturn * 2;
return toReturn;
}
@@ -96,10 +96,14 @@ namespace Microsoft.Basetypes
}
[Pure]
- public static BigFloat FromBigInt(BIM v) {
+ public static BigFloat FromLong(long v) {
return new BigFloat(0, v, 8, 24);
}
+ public static BigFloat FromBigInt(BIM v) {
+ return FromLong(Int64.Parse(v.ToString())); //Sketchy. Hope this doesn't cause problems
+ }
+
public static BigFloat FromBigDec(BigDec v)
{
return new BigFloat(v.ToDecimalString(), 8, 24);
@@ -116,11 +120,11 @@ namespace Microsoft.Basetypes
case 1:
return new BigFloat(vals[0], 8, 24);
case 2:
- return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);
+ return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), 8, 24);
case 3:
return new BigFloat(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
case 4:
- return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
+ return new BigFloat(Int32.Parse(vals[0]), Int64.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
default:
throw new FormatException(); //Unreachable
}
@@ -130,7 +134,7 @@ namespace Microsoft.Basetypes
}
}
- internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) {
+ internal BigFloat(int exponent, long mantissa, int exponentSize, int mantissaSize) {
this.exponentSize = exponentSize;
this.exponent = exponent;
this.mantissa = mantissa;
@@ -146,8 +150,30 @@ namespace Microsoft.Basetypes
this.mantissa = 0;
this.isDec = true;
this.dec_value = dec_value;
+ //Special cases:
+ if (this.dec_value.Equals("+oo") || this.dec_value.Equals("-oo") || this.dec_value.Equals("-zero"))
+ return;
+ if (this.dec_value.ToLower().Equals("nan")) {
+ this.dec_value = "NaN";
+ return;
+ }
+ if (this.dec_value.Equals("INF") || this.dec_value.Equals("+INF")) {
+ this.dec_value = "+oo";
+ return;
+ }
+ if (this.dec_value.Equals("-INF")) {
+ this.dec_value = "-oo";
+ return;
+ }
+ if (this.dec_value.Equals("+zero")) {
+ this.dec_value = "0.0";
+ return;
+ }
+ //End special cases
if (this.dec_value.IndexOf(".") == -1)
this.dec_value += ".0"; //Assures that the decimal value is a "real" number
+ if (this.dec_value.IndexOf(".") == 0)
+ this.dec_value = "0" + this.dec_value; //Assures that decimals always have a 0 in front
}
private BIM maxMantissa()
@@ -265,7 +291,7 @@ namespace Microsoft.Basetypes
}
}
- return new BigFloat(exp, value, exponentSize, mantissaSize);
+ return new BigFloat(exp, Int64.Parse(value.ToString()), exponentSize, mantissaSize);
}
// ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
@@ -345,7 +371,7 @@ namespace Microsoft.Basetypes
public BigFloat Abs {
//TODO: fix for fp functionality
get {
- return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
+ return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize);
}
}
@@ -353,7 +379,7 @@ namespace Microsoft.Basetypes
public BigFloat Negate {
//TODO: Modify for correct fp functionality
get {
- return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
+ return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize);
}
}
@@ -367,9 +393,9 @@ namespace Microsoft.Basetypes
//TODO: Modify for correct fp functionality
Contract.Requires(x.ExponentSize == y.ExponentSize);
Contract.Requires(x.MantissaSize == y.MantissaSize);
- BIM m1 = x.Mantissa;
+ long m1 = x.Mantissa;
int e1 = x.Exponent;
- BIM m2 = y.Mantissa;
+ long m2 = y.Mantissa;
int e2 = y.Exponent;
m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit
m2 = m2 + two_n(y.mantissaSize + 1);
@@ -381,7 +407,7 @@ namespace Microsoft.Basetypes
}
while (e2 < e1) {
- m2 = m2 / two;
+ m2 = m2 / 2;
e2++;
}
@@ -404,6 +430,14 @@ namespace Microsoft.Basetypes
////////////////////////////////////////////////////////////////////////////
// Some basic comparison operations
+ public bool IsSpecialType {
+ get {
+ if (!IsDec)
+ return false;
+ return (dec_value.Equals("NaN") || dec_value.Equals("+oo") || dec_value.Equals("-oo") || dec_value.Equals("-zero"));
+ }
+ }
+
public bool IsPositive {
get {
return !IsNegative;
@@ -418,7 +452,7 @@ namespace Microsoft.Basetypes
public bool IsZero {
get {
- return Mantissa.IsZero && Exponent == 0;
+ return Mantissa == 0 && Exponent == 0;
}
}
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 889d7be8..5fcb1cdc 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1897,9 +1897,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get(); //Skip the fp token
Get();
if (t.val != "(") { throw new FormatException(); }
- while (la.kind == 1 || la.kind == 3 || la.kind == 6 || la.kind == 75) { //Get values between the parens
+ while (la.kind == 1 || la.kind == 3 || la.kind == 6 || la.kind == 4 || la.kind == 74 || la.kind == 75) { //Get values between the parens
Get();
- if (t.val == "-") //special negative case (la.kind == 75)
+ if (t.val == "-" || t.val == "+") //special sign case (la.kind == 74 or 75)
s += t.val;
else
s += t.val + " ";
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;
}