From d5890371c7ba71af00cced2376009e0fb966a56a Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 7 Sep 2013 00:17:10 -0700
Subject: fixed the problem with codexprs now positive/negative context is
 detected and appropriate translation is done

---
 Source/VCExpr/Boogie2VCExpr.cs | 34 +++++++++++++++++++++++++++++++---
 1 file changed, 31 insertions(+), 3 deletions(-)

(limited to 'Source/VCExpr/Boogie2VCExpr.cs')

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index e4101d49..c5c61546 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
-  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext);
+  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);
 
   public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
     // Stack on which the various Visit-methods put the result of the translation
@@ -375,13 +375,42 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;
     }
 
+    public bool isPositiveContext = true;
     private VCExpr TranslateNAryExpr(NAryExpr node) {
       Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
+     
+      bool flipContextForArg0 = false;
+      if (node.Fun is UnaryOperator)
+      {
+          UnaryOperator oper = (UnaryOperator)node.Fun;
+          if (oper.Op == UnaryOperator.Opcode.Neg)
+              flipContextForArg0 = true;
+      }
+      else if (node.Fun is BinaryOperator)
+      {
+          BinaryOperator oper = (BinaryOperator)node.Fun;
+          if (oper.Op == BinaryOperator.Opcode.Imp)
+              flipContextForArg0 = true;
+          else if (oper.Op == BinaryOperator.Opcode.Iff) {
+              Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[0], node.Args[1] });
+              Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[1], node.Args[0] });
+              NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List<Expr> { one, two });
+              TypecheckingContext tc = new TypecheckingContext(null);
+              cmpd.Typecheck(tc);
+              return TranslateNAryExpr(cmpd);
+          }
+      }
+
       int n = node.Args.Count;
       List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);
+        
       for (int i = 0; i < n; i++) {
+        if (i == 0 && flipContextForArg0)
+            isPositiveContext = !isPositiveContext;
         vcs.Add(Translate(cce.NonNull(node.Args)[i]));
+        if (i == 0 && flipContextForArg0)
+            isPositiveContext = !isPositiveContext;
       }
 
       if (node.Type == null) {
@@ -618,12 +647,11 @@ namespace Microsoft.Boogie.VCExprAST {
     public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {
       //Contract.Requires(codeExpr != null);
       Contract.Ensures(Contract.Result<Expr>() != null);
-
       Contract.Assume(codeExprConverter != null);
 
       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
       List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();
-      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, false);
+      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext);
       Push(e);
       return codeExpr;
     }
-- 
cgit v1.2.3