ctl/double_negate_ml

   1 (* optimizes triples that have complementary environments and the same
   2 witnesses *)
   3
   4 let double_negate trips =
   5   let y =
   6     List.sort
   7       (function (s,_,wit) -> function (s',_,wit') -> compare (s,wit) (s',wit'))
   8       trips in
   9   let rec classify = function
  10       [] -> []
  11     | ((s,th,wit) as x)::rest ->
  12         (match classify rest with
  13           [] -> [[x]]
  14         | (((s',th',wit')::_) as x1)::rest ->
  15             if (s,wit) = (s',wit')
  16             then (x::x1)::rest
  17             else [x]::(x1::rest)
  18         | _ -> failwith "not possible") in
  19   let y =
  20     List.map
  21       (function
  22           (((s,_,wit)::_) as all) ->
  23             ((s,wit),List.map (function (_,th,_) -> th) all)
  24         | _ -> failwith "not possible")
  25     (classify y) in
  26   let cnf rest_th th =
  27     List.fold_left
  28       (function rest ->
  29         function sub1 ->
  30           List.fold_left
  31             (function rest ->
  32               function subs ->
  33                 if memBy eq_sub (negate_sub sub1) subs
  34                 then rest
  35                 else if memBy eq_sub sub1 subs
  36                 then subs::rest
  37                 else (sub1::subs)::rest)
  38             rest rest_th)
  39       [] th in
  40   let dnf rest_th th =
  41     List.fold_left
  42       (function rest ->
  43         function sub1 ->
  44           List.fold_left
  45             (function rest ->
  46               function subs ->
  47                 match conj_subst [sub1] subs with
  48                   None -> rest
  49                 | Some th -> th::rest)
  50             rest rest_th)
  51       [] th in
  52   let res =
  53     List.sort compare
  54       (List.fold_left
  55          (function rest ->
  56            function
  57                ((s,wit),[th]) -> (s,th,wit)::rest
  58              | ((s,wit),ths) ->
  59                  match ths with
  60                    [] -> failwith "not possible"
  61                  | (th::ths) ->
  62                      let (cnf : substitution list) =
  63                        List.fold_left cnf
  64                          (List.map (function x -> [x]) th) ths in
  65                      match cnf with
  66                        [] -> (s,[],wit)::rest
  67                      | th::ths ->
  68                          let res =
  69                            setify
  70                              (List.fold_left dnf
  71                                 (List.map (function x -> [x]) th)
  72                                 ths) in
  73                          (List.map (function th -> (s,th,wit)) res) @ rest)
  74          [] y) in
  75   res