diff options
author | RustanLeino <leino@microsoft.com> | 2016-08-17 13:40:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-08-17 13:40:57 -0700 |
commit | 12d1543333babd202d76e259418dd03c0c7c56c3 (patch) | |
tree | 69bd181ccb97621378ab630a1357bd5583cc96a8 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
parent | 529b1bc37b6da3f40dc85aef4cf252e9c98dd566 (diff) | |
parent | 2b64144fb02b68d00188ee81c27afa5fbc026b5b (diff) |
Merge pull request #35 from Checkmate50/master
Floating Point Support
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 81 |
1 files changed, 80 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 06aa5bbe..7b2525f7 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -121,7 +121,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(); @@ -145,6 +145,8 @@ namespace Microsoft.Boogie.SMTLib return "Int"; else if (t.IsReal) return "Real"; + else if (t.IsFloat) + return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -204,6 +206,11 @@ namespace Microsoft.Boogie.SMTLib else wr.Write(lit.ToDecimalString()); } + else if (node is VCExprFloatLit) + { + BigFloat lit = ((VCExprFloatLit)node).Val; + wr.Write("(" + lit.ToBVString() + ")"); + } else { Contract.Assert(false); throw new cce.UnreachableException(); @@ -630,6 +637,78 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.add RNE", node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.sub RNE", node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.mul RNE", node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.div RNE", node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.rem RNE", node, options); + return true; + } + + public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.min", node, options); + return true; + } + + public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.max", node, options); + return true; + } + + public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.leq", node, options); + return true; + } + + public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.lt", node, options); + return true; + } + + public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.geq", node, options); + return true; + } + + public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.gt", node, options); + return true; + } + + public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.eq", node, options); + return true; + } + static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' }; public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { |