diff options
author | Dietrich <dgeisler50@gmail.com> | 2015-05-04 03:46:22 -0600 |
---|---|---|
committer | Dietrich <dgeisler50@gmail.com> | 2015-05-04 03:46:22 -0600 |
commit | d213a71b16a344dab7ac5d08507668abebffd21e (patch) | |
tree | ece00fc97fcc83309a51b95b2b6972a75e6af73d /Source/Provers/SMTLib/SMTLibLineariser.cs | |
parent | 1058d935425fa9c9544fbf18dad184cd8333e0d9 (diff) |
integrated the named float type to act as a real in boogie
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 6accf79f..b834aa6b 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -116,7 +116,7 @@ namespace Microsoft.Boogie.SMTLib }
sb.Append(']');
TypeToStringHelper(m.Result, sb);
- } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {
+ } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) {
sb.Append(TypeToString(t));
} else {
System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -140,6 +140,8 @@ namespace Microsoft.Boogie.SMTLib return "Int";
else if (t.IsReal)
return "Real";
+ else if (t.IsFloat)
+ return "Real"; //TODO: Make to be a float
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -199,6 +201,15 @@ namespace Microsoft.Boogie.SMTLib else
wr.Write(lit.ToDecimalString());
}
+ else if (node is VCExprFloatLit)
+ {
+ BigFloat lit = ((VCExprFloatLit)node).Val;
+ if (lit.IsNegative)
+ // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
+ wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
+ else
+ wr.Write(lit.ToDecimalString());
+ }
else {
Contract.Assert(false);
throw new cce.UnreachableException();
|