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 | |
| parent | 1058d935425fa9c9544fbf18dad184cd8333e0d9 (diff) | |
integrated the named float type to act as a real in boogie
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 13 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 2 |
2 files changed, 13 insertions, 2 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();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 30363102..2b053410 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -296,7 +296,7 @@ void ObjectInvariant() return;
}
- if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
+ if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv)
return;
CtorType ctorType = type as CtorType;
|