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