From 3f7a84cefc8df8cfb1c6442861331273c1d46ff3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 13 Apr 2010 09:31:04 -0400 Subject: When applying multiple policies at once, filter the policy set at the beginning, removing unmatchable policies --- src/iflow.sml | 35 ++++++++++++++++++++--------------- 1 file changed, 20 insertions(+), 15 deletions(-) (limited to 'src/iflow.sml') diff --git a/src/iflow.sml b/src/iflow.sml index 560e0752..797f13d0 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -2503,8 +2503,19 @@ fun check file = 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 @@ fun check file = 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 @@ fun check file = (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 -- cgit v1.2.3