# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1271165464 14400
# Node ID efbefd6e3f6cc6ed32a9025eb788dbc5ecd68595
# Parent  5fa8ae2a34e3d45bf26409825801e9ceb4ce3631
When applying multiple policies at once, filter the policy set at the beginning, removing unmatchable policies

diff -r 5fa8ae2a34e3 -r efbefd6e3f6c src/iflow.sml
--- a/src/iflow.sml	Tue Apr 13 09:25:45 2010 -0400
+++ b/src/iflow.sml	Tue Apr 13 09:31:04 2010 -0400
@@ -2503,8 +2503,19 @@
                                            let
                                                val cc = ccOf hyps
 
-                                               val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab)
-                                                                   | (_, avail) => avail) SS.empty hyps
+                                               fun relevant () =
+                                                   let
+                                                       val avail = foldl (fn (AReln (Sql tab, _), avail) =>
+                                                                             SS.add (avail, tab)
+                                                                           | (_, avail) => avail) SS.empty hyps
+                                                   in
+                                                       List.filter
+                                                           (fn (g1, _) =>
+                                                               decompG g1
+                                                                       (List.all (fn AReln (Sql tab, _) =>
+                                                                                     SS.member (avail, tab)
+                                                                                   | _ => true))) client
+                                                   end
 
                                                fun tryCombos (maxLv, pols, g, outs) =
                                                    case pols of
@@ -2517,18 +2528,12 @@
                                                            val outs1 = map (bumpLvars (maxLv + 1)) outs1
                                                            fun skip () = tryCombos (maxLv, pols, g, outs)
                                                        in
-                                                           if decompG g1
-                                                                      (List.all (fn AReln (Sql tab, _) =>
-                                                                                    SS.member (avail, tab)
-                                                                                  | _ => true)) then
-                                                               skip ()
-                                                               orelse tryCombos (Int.max (maxLv,
-                                                                                          maxLvarP g1),
-                                                                                 pols,
-                                                                                 And (g1, g),
-                                                                                 outs1 @ outs)
-                                                           else
-                                                               skip ()
+                                                           skip ()
+                                                           orelse tryCombos (Int.max (maxLv,
+                                                                                      maxLvarP g1),
+                                                                             pols,
+                                                                             And (g1, g),
+                                                                             outs1 @ outs)
                                                        end
                                            in
                                                (fl <> Control Where
@@ -2538,7 +2543,7 @@
                                                                               (fn goals => imply (cc, hyps, goals,
                                                                                                   SOME outs)))
                                                                   client
-                                               orelse tryCombos (0, client, True, [])
+                                               orelse tryCombos (0, relevant (), True, [])
                                                orelse (reset ();
                                                        Print.preface ("Untenable hypotheses"
                                                                       ^ (case fl of