From 5cff8cd77c629ec8e48a2498b1e704173306586a Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 21:09:06 -0600
Subject: finished testing, fixed several minor compiler bugs

---
 Source/Basetypes/BigFloat.cs           |  2 +-
 Source/Core/Parser.cs                  | 82 ++++++++++++++++++++--------------
 Source/Provers/SMTLib/SMTLibProcess.cs |  2 +-
 3 files changed, 51 insertions(+), 35 deletions(-)

(limited to 'Source')

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index a0ce03a5..3c4cc40a 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -313,7 +313,7 @@ namespace Microsoft.Basetypes
         return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
       }
       else if (this.Value == "") {
-        return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + this.significandSize + ")";
+        return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
       }
       else {
         return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 8161544f..7982f594 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -668,35 +668,7 @@ private class BvBounds : Expr {
    ty = new BasicType(t, SimpleType.Real);
   } else if (la.kind == 98) {
    Get();
-   if (t.val.Length > 5) {
-    switch (Int32.Parse(t.val.Substring(5))) {
-    case 16:
-        ty = new FloatType(t, 5, 11);
-        break;
-    case 32:
-        ty = new FloatType(t, 8, 24);
-        break;
-    case 64:
-        ty = new FloatType(t, 11, 53);
-        break;
-    case 128:
-        ty = new FloatType(t, 15, 113);
-        break;
-    default:
-        SynErr(3);
-        break;
-    }
-   }
-   else {
-    Expect(19); //<
-    Expect(3); //int
-    int exp = Int32.Parse(t.val);
-    Expect(12); //,
-    Expect(3); //int
-    int man = Int32.Parse(t.val);
-    ty = new FloatType(t, exp, man);
-    Expect(20); //>
-   }
+   ty = FType();
   } else if (la.kind == 16) {
 			Get();
 			ty = new BasicType(t, SimpleType.Bool); 
@@ -707,6 +679,39 @@ private class BvBounds : Expr {
 		} else SynErr(101);
 	}
 
+ FloatType FType() {
+   if (t.val.Length > 5) {
+    switch (Int32.Parse(t.val.Substring(5))) {
+     case 16:
+      return new FloatType(t, 5, 11);
+     case 32:
+      return new FloatType(t, 8, 24);
+     case 64:
+      return new FloatType(t, 11, 53);
+     case 128:
+      return new FloatType(t, 15, 113);
+     default:
+      SynErr(3);
+      return new FloatType(t, 0, 0);
+     }
+   }
+   else {
+    try {
+     Expect(19); //<
+     Expect(3); //int
+     int exp = Int32.Parse(t.val);
+     Expect(12); //,
+     Expect(3); //int
+     int man = Int32.Parse(t.val);
+     Expect(20); //>
+     return new FloatType(t, exp, man);
+    }
+    catch (Exception) {
+     return new FloatType(t, 0, 0);
+    }
+   }
+ }
+
 	void Ident(out IToken/*!*/ x) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);
 		Expect(1);
@@ -1915,8 +1920,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
        Get(); //Skip the float token
        if (la.val == "(") {
          Get();
-         Expect(16); //bool
-         negative = Boolean.Parse(t.val);
+         if (la.val == "false")
+           negative = false;
+         else if (la.val == "true")
+           negative = true;
+         else
+           throw new FormatException();
+         Get();
          Expect(12); //,
          BvLit(out exp_val, out exp);
          Expect(12);
@@ -1933,10 +1943,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
          sig = Int32.Parse(t.val);
          Expect(20); //>
          Expect(9); //(
-         if (la.kind == 4) {
+         if (la.kind == 1) { //NaN
            Get();
            n = new BigFloat(t.val, exp, sig);
          }
+         else if (la.kind == 74 || la.kind == 75) { //+ or -
+           Get();
+           String s = t.val;
+           Get();
+           n = new BigFloat(s + t.val, exp, sig);
+         }
          else {
            BvLit(out value, out size);
            n = new BigFloat(value.ToString(), exp, sig);
@@ -2194,7 +2210,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		{x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x},
 		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
 		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+		{x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4982d81e..bc94e253 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,7 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");
         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
       }
-      Console.WriteLine(cmd);
+      //Console.WriteLine(cmd);
       toProver.WriteLine(cmd);
     }
 
-- 
cgit v1.2.3