From 9af64efeb4a057f853bb08cfc0fa8cbdc4a166b2 Mon Sep 17 00:00:00 2001
From: Akash Lal <akashl@microsoft.com>
Date: Thu, 23 Apr 2015 14:59:36 +0530
Subject: Minor fixes for AbsHoudini

---
 Source/Houdini/AbstractHoudini.cs | 86 +++++++++++++++++++++++++++++++++++++--
 1 file changed, 82 insertions(+), 4 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 210d9f6c..3415ae78 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -601,19 +601,24 @@ namespace Microsoft.Boogie.Houdini {
             // Inline functions
             (new InlineFunctionCalls()).VisitBlockList(impl.Blocks);
 
-            ExtractQuantifiedExprs(impl);
+            
             StripOutermostForall(impl);
+            //ExtractQuantifiedExprs(impl);
+            ExtractBoolExprs(impl);
 
             //CommandLineOptions.Clo.PrintInstrumented = true;
-            //var tt = new TokenTextWriter(Console.Out);
-            //impl.Emit(tt, 0);
-            //tt.Close();
+            //using (var tt = new TokenTextWriter(Console.Out))
+            //    impl.Emit(tt, 0);
 
             // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants
             var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);
             var fv = new ReplaceFunctionCalls(existentialFunctionNames);
             fv.VisitBlockList(impl.Blocks);
 
+            //using (var tt = new TokenTextWriter(Console.Out))
+            //    impl.Emit(tt, 0);
+
+
             impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);
             impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);
 
@@ -684,6 +689,24 @@ namespace Microsoft.Boogie.Houdini {
             }
         }
 
+        // convert "foo(... e ...) to:
+        //    (p iff e) ==> foo(... p ...) 
+        // where p is a fresh boolean variable, foo is an existential constant
+        // and e is a Boolean-typed argument of foo
+        private void ExtractBoolExprs(Implementation impl)
+        {
+            var funcs = new HashSet<string>(existentialFunctions.Keys);
+            foreach (var blk in impl.Blocks)
+            {
+                foreach (var acmd in blk.Cmds.OfType<AssertCmd>())
+                {
+                    var ret = ExtractBoolArgs.Extract(acmd.Expr, funcs);
+                    acmd.Expr = ret.Item1;
+                    impl.LocVars.AddRange(ret.Item2);
+                }
+            }
+        }
+
         // convert "assert e1 && forall x: e2" to
         //    assert e1 && e2[x <- x@bound]
         private void StripOutermostForall(Implementation impl)
@@ -967,6 +990,61 @@ namespace Microsoft.Boogie.Houdini {
 
     }
 
+    // convert "foo(... e ...) to:
+    //    (p iff e) ==> foo(... p ...) 
+    // where p is a fresh boolean variable, foo is an existential constant
+    // and e is a Boolean-typed argument of foo
+    class ExtractBoolArgs : StandardVisitor
+    {
+        static int freshConstCounter = 0;
+        HashSet<string> existentialFunctions;
+        HashSet<Constant> newConstants;
+
+        private ExtractBoolArgs(HashSet<string> existentialFunctions)
+        {
+            this.existentialFunctions = existentialFunctions;
+            this.newConstants = new HashSet<Constant>();
+        }
+
+        public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> existentialFunctions)
+        {
+            var eq = new ExtractBoolArgs(existentialFunctions);
+            expr = eq.VisitExpr(expr);
+            return Tuple.Create(expr, eq.newConstants.AsEnumerable());
+        }
+
+        public override Expr VisitNAryExpr(NAryExpr node)
+        {
+            if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName))
+            {
+                var constants = new Dictionary<Constant, Expr>();
+                for (int i = 0; i < node.Args.Count; i++)
+                {
+                    if (node.Args[i].Type == Type.Bool)
+                    {
+                        var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
+                            "boolArg@const" + freshConstCounter, Microsoft.Boogie.Type.Bool), false);
+                        freshConstCounter++;
+                        constants.Add(constant, node.Args[i]);
+                        node.Args[i] = Expr.Ident(constant);
+                    }
+                }
+
+                newConstants.UnionWith(constants.Keys);
+
+                Expr ret = Expr.True;
+                foreach (var tup in constants)
+                {
+                    ret = Expr.And(ret, Expr.Eq(Expr.Ident(tup.Key), tup.Value));
+                }
+                return Expr.Imp(ret, node);
+            } 
+
+            return base.VisitNAryExpr(node);
+        }
+    }
+
+
     // convert "foo(... forall e ...) to:
     //    (p iff forall e) ==> foo(... p ...) 
     // where p is a fresh boolean variable and foo is an existential constant
-- 
cgit v1.2.3