From 0324757fb1a12d76861a51be988690bf8de75f64 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Wed, 14 Oct 2015 12:57:50 -0600
Subject: Modified translation so that z3 runs with type checking for simple
 binary operations

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 76 ++++++++++++++++++++++++++++++-
 Source/Provers/SMTLib/Z3.cs               |  4 +-
 2 files changed, 77 insertions(+), 3 deletions(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f030870e..629f7e2d 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsReal)
         return "Real";
       else if (t.IsFloat)
-        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax
+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")";
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
@@ -204,11 +204,13 @@ namespace Microsoft.Boogie.SMTLib
       else if (node is VCExprFloatLit)
       {
         BigFloat lit = ((VCExprFloatLit)node).Val;
+        wr.Write(("((_ to_fp 8 24) roundTowardZero "));
         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());
+        wr.Write(")");
       }
       else {
         Contract.Assert(false);
@@ -616,6 +618,78 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
+      public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.add roundTowardZero", node, options);
+        return true;
+      }
+
+      public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.sub roundTowardZero", node, options);
+        return true;
+      }
+
+      public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.mul roundTowardZero", node, options);
+        return true;
+      }
+
+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.div roundTowardZero", node, options);
+        return true;
+      }
+
+      public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.rem roundTowardZero", 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)
       {
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8e8b2d55..250e04c9 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -253,7 +253,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)
             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
 
-            options.AddWeakSmtOption("TYPE_CHECK", "false");
+            options.AddWeakSmtOption("TYPE_CHECK", "true");
             options.AddWeakSmtOption("smt.BV.REFLECT", "true");
 
             if (options.TimeLimit > 0)
@@ -334,7 +334,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)
             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
 
-            options.AddWeakSmtOption("TYPE_CHECK", "false");
+            options.AddWeakSmtOption("TYPE_CHECK", "true");
             options.AddWeakSmtOption("BV_REFLECT", "true");
 
             if (options.TimeLimit > 0)
-- 
cgit v1.2.3