From 575d226a8e15efc111bfaf57f188261e12f7ef95 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 7 Dec 2014 15:58:48 +0100
Subject: Optimized the VC generation for assumption variables.

---
 Source/VCGeneration/ConditionGeneration.cs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'Source/VCGeneration/ConditionGeneration.cs')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 178f8ddb..aca9d3f8 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1684,6 +1684,15 @@ namespace VC {
             dropCmd = true;
           }
         }
+        else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization"))
+        {
+          var identExpr = pc.Expr as IdentifierExpr;
+          if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl))
+          {
+            incarnationMap[identExpr.Decl] = LiteralExpr.True;
+            dropCmd = true;
+          }
+        }
         pc.Expr = copy;
         if (!dropCmd)
         {
@@ -1739,6 +1748,24 @@ namespace VC {
               newIncarnationMappings[lhs] = x_prime_exp;
             }
             #endregion
+
+            var nAryExpr = copies[i] as NAryExpr;
+            if (nAryExpr != null)
+            {
+              var binOp = nAryExpr.Fun as BinaryOperator;
+              if (binOp != null
+                  && binOp.Op == BinaryOperator.Opcode.And)
+              {
+                var arg0 = nAryExpr.Args[0] as LiteralExpr;
+                var arg1 = nAryExpr.Args[1] as LiteralExpr;
+                if ((arg0 != null && arg0.IsTrue) || (arg1 != null && arg1.IsFalse))
+                {
+                  // Replace the expressions "true && arg1" or "arg0 && false" by "arg1".
+                  copies[i] = nAryExpr.Args[1];
+                }
+              }
+            }
+          
             #region Create an assume command with the new variable
             assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
             #endregion
-- 
cgit v1.2.3