Commit 6ae0e342 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2005-05-10 07:50:11 by afrisch] Empty log message

Original author: afrisch
Date: 2005-05-10 07:50:11+00:00
parent 8607db52
......@@ -142,12 +142,11 @@ OBJECTS = \
driver/config.cmo \
misc/stats.cmo \
misc/serialize.cmo misc/custom.cmo \
misc/state.cmo misc/pool.cmo misc/encodings.cmo \
misc/bool.cmo \
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo \
misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/myweak.cmo \
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo \
misc/html.cmo \
\
types/sortedList.cmo types/boolean.cmo types/ident.cmo \
types/sortedList.cmo misc/bool.cmo types/boolean.cmo types/ident.cmo \
types/intervals.cmo \
types/chars.cmo types/atoms.cmo \
types/normal.cmo \
......
let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=)
module type S =
sig
type elem
......@@ -169,8 +173,8 @@ struct
*)
let split x pos ign neg =
if ign = True then True
else if (pos = False) && (neg = False) then ign
if ign == True then True
else if (pos == False) && (neg == False) then ign
else split x pos ign neg
......@@ -207,10 +211,10 @@ struct
let rec simplify a l =
if (a = False) then False else simpl_aux1 a [] l
if (a == False) then False else simpl_aux1 a [] l
and simpl_aux1 a accu = function
| [] ->
if accu = [] then a else
if accu == [] then a else
(match a with
| True -> True
| False -> assert false
......@@ -295,9 +299,9 @@ struct
split x2 (p2 ** a) (i2 ** a) (n2 ** a)
let rec trivially_disjoint a b =
if a == b then a = False
if a == b then a == False
else match (a,b) with
| True, a | a, True -> a = False
| True, a | a, True -> a == False
| False, _ | _, False -> true
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
......@@ -349,7 +353,7 @@ struct
let rec serialize t = function
| (True | False) as b ->
Serialize.Put.bool t true; Serialize.Put.bool t (b = True)
Serialize.Put.bool t true; Serialize.Put.bool t (b == True)
| Split (_,x,p,i,n) ->
Serialize.Put.bool t false;
X.serialize t x;
......@@ -561,7 +565,7 @@ struct
let rec serialize t = function
| (Zero | One) as b ->
Serialize.Put.bool t true; Serialize.Put.bool t (b = One)
Serialize.Put.bool t true; Serialize.Put.bool t (b == One)
| Branch (x,p,n,_,_) ->
Serialize.Put.bool t false;
X.serialize t x;
......@@ -594,506 +598,708 @@ struct
end
(*
module Simplify(M : MAKE)(X : Custom.T) = struct
module B = M(X)
module Simplify(X : Custom.T) = struct
type elem = X.t
type f = { vars: (X.t * bool) list; (* toplevel vars and their polarity *)
subs: f list; (* subformulas *)
mutable allvars: (X.t * int * int) list; (* # of pos,neg occurences *)
mutable form: B.t option;
mutable id: int (* unique id for hash consing *)
}
type t = f
let tmpl = { vars = []; subs = []; allvars = []; form = None; id = 0 }
module V = SortedList.Make(X)
type f = {
pos: V.t;
neg: V.t;
subs: fset;
mutable id: int (* unique id for hash consing *)
}
and fset =
| Empty
| Leaf of f
| Branch of int * int * fset * fset
type t = PosF of f | NegF of f | PosV of X.t | NegV of X.t | Zero | One
let id k = k.id
module F = struct
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let singleton k = Leaf k
let zero_bit k m = (k land m) == 0
let rec mem k = function
| Empty -> false
| Leaf j -> k == j
| Branch (_, m, l, r) -> mem k (if zero_bit (id k) m then l else r)
let lowest_bit x = x land (-x)
let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
let mask p m = p land (m-1)
let join (p0,t0,p1,t1) =
let m = branching_bit p0 p1 in
if zero_bit p0 m then Branch (mask p0 m, m, t0, t1)
else Branch (mask p0 m, m, t1, t0)
let match_prefix k p m = (mask k m) == p
let add k t =
let rec ins = function
| Empty -> Leaf k
| Leaf j as t -> if j== k then t else join (id k, Leaf k, id j, t)
| Branch (p,m,t0,t1) as t ->
if match_prefix (id k) p m then
if zero_bit (id k) m then Branch (p, m, ins t0, t1)
else Branch (p, m, t0, ins t1)
else join (id k, Leaf k, p, t)
in
ins t
let print px =
let allvars ppf f =
List.iter (fun (x,p,n) -> Format.fprintf ppf "[%a:%i,%i]" px x p n)
f.allvars
in
let rec union s t = match s,t with
| Empty, t -> t
| t, Empty -> t
| Leaf k, t -> add k t
| t, Leaf k -> add k t
| (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
if m == n && match_prefix q p m then
Branch (p, m, union s0 t0, union s1 t1)
else if m < n && match_prefix q p m then
if zero_bit q m then Branch (p, m, union s0 t, s1)
else Branch (p, m, s0, union s1 t)
else if m > n && match_prefix p q n then
if zero_bit p n then Branch (q, n, union s t0, t1)
else Branch (q, n, t0, union s t1)
else join (p, s, q, t)
let rec subset s1 s2 = match s1,s2 with
| Empty, _ -> true
| _, Empty -> false
| Leaf k1, _ -> mem k1 s2
| Branch _, Leaf _ -> false
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then subset l1 l2 && subset r1 r2
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then subset l1 l2 && subset r1 l2
else subset l1 r2 && subset r1 r2
else
false
let branch = function
| (_,_,Empty,t) -> t
| (_,_,t,Empty) -> t
| (p,m,t0,t1) -> Branch (p,m,t0,t1)
let rec remove k = function
| Empty -> Empty
| Leaf j as t -> if k == j then Empty else t
| Branch (p,m,t0,t1) as t ->
if match_prefix (id k) p m then
if zero_bit (id k) m then branch (p, m, remove k t0, t1)
else branch (p, m, t0, remove k t1)
else t
let rec inter s1 s2 = match s1,s2 with
| Empty, _ -> Empty
| _, Empty -> Empty
| Leaf k1, _ -> if mem k1 s2 then s1 else Empty
| _, Leaf k2 -> if mem k2 s1 then s2 else Empty
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then union (inter l1 l2) (inter r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
inter (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
inter s1 (if zero_bit p1 m2 then l2 else r2)
else Empty
let rec split s1 s2 = match s1,s2 with
| Empty, _ -> Empty,Empty,s2
| _, Empty -> s1,Empty,Empty
| Leaf k1, _ -> if mem k1 s2 then Empty,s1,(remove k1 s2) else s1,Empty,s2
| _, Leaf k2 -> if mem k2 s1 then (remove k2 s1),s2,Empty else s1,Empty,s2
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
let x1,x12,x2 = split l1 l2
and y1,y12,y2 = split r1 r2 in
union x1 y1, union x12 y12, union x2 y2
else if m1 < m2 && match_prefix p2 p1 m1 then
if zero_bit p2 m1
then let x1,x12,x2 = split l1 s2 in union x1 r1, x12, x2
else let x1,x12,x2 = split r1 s2 in union l1 x1, x12, x2
else if m2 < m1 && match_prefix p1 p2 m1 then
if zero_bit p1 m2
then let x1,x12,x2 = split l2 s1 in x1, x12, union x2 r2
else let x1,x12,x2 = split r1 s2 in x1, x12, union l2 x2
else (s1,Empty,s2)
let rec diff s1 s2 = match s1,s2 with
| Empty, _ -> Empty
| _, Empty -> s1
| Leaf k1, _ -> if mem k1 s2 then Empty else s1
| _, Leaf k2 -> remove k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then union (diff l1 l2) (diff r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
if zero_bit p2 m1 then union (diff l1 s2) r1
else union l1 (diff r1 s2)
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
else s1
let rec intersect s1 s2 = match s1,s2 with
| Empty, _ -> false
| _, Empty -> false
| Leaf k1, _ -> mem k1 s2
| _, Leaf k2 -> mem k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then intersect l1 l2 || intersect r1 r2
else if m1 < m2 && match_prefix p2 p1 m1 then
intersect (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
intersect s1 (if zero_bit p1 m2 then l2 else r2)
else false
let disjoint s1 s2 = not (intersect s1 s2)
let rec equal x y = x == y || match x,y with
| Leaf k1, Leaf k2 -> k1 == k2
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
p1 == p2 && m1 == m2 && (equal l1 l2) && (equal r1 r2)
| _ -> false
let rec hash = function
| Empty -> 0
| Leaf k -> 1 + 3 * (id k)
| Branch (p,m,l,r) ->
2 + 3 * p + 257 * m + 16387 * (hash l) + 1048577 * (hash r)
let rec iter f = function
| Empty -> ()
| Leaf k -> f k
| Branch (_,_,t0,t1) -> iter f t0; iter f t1
let rec fold f s accu = match s with
| Empty -> accu
| Leaf k -> f k accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
let rec card f s accu = match s with
| Empty -> accu
| Leaf k -> f k accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
let rec cardinal = function
| Empty -> 0
| Leaf _ -> 1
| Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
let rec allvars = function
| Empty -> V.empty
| Leaf f -> f.allvars
| Branch (_,_,t0,t1) -> V.cup (allvars t0) (allvars t1)
end
let print_f px =
let rec aux ppf f =
(* Format.fprintf ppf "{%i}" f.id; *)
(* (match f.form with Some _ -> Format.fprintf ppf "*" | _ -> ()); *)
(* allvars ppf f; *)
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "|" in
List.iter (function
| (x,true) -> sep (); Format.fprintf ppf "%a" px x
| (x,false) -> sep (); Format.fprintf ppf "~%a" px x) f.vars;
List.iter (fun f -> sep (); Format.fprintf ppf "~(@[%a@])" aux f) f.subs;
V.iter (fun x -> sep (); Format.fprintf ppf "%a" px x) f.pos;
V.iter (fun x -> sep (); Format.fprintf ppf "~%a" px x) f.neg;
F.iter (fun f -> sep (); Format.fprintf ppf "~(@[%a@])" aux f) f.subs;
if !first then Format.fprintf ppf "."
in
fun ppf f -> (*allvars ppf f; *) aux ppf f
let dump = print (*X.dump*)
let print_t px ppf = function
| PosV f -> Format.fprintf ppf "%a" px f
| NegV f -> Format.fprintf ppf "~%a" px f
| PosF f -> Format.fprintf ppf "%a" (print_f px) f
| NegF f -> Format.fprintf ppf "~(%a)" (print_f px) f
| Zero -> Format.fprintf ppf "0"
| One -> Format.fprintf ppf "1"
let dump = print_f
(fun ppf i -> Format.fprintf ppf "%i" (X.hash i))
let rec cup_vars vars1 vars2 = match (vars1,vars2) with
| ((x1,p1,n1) as z1)::vars1', ((x2,p2,n2) as z2)::vars2' ->
let c = X.compare x1 x2 in
if c = 0 then (x1,p1+p2,n1+n2)::(cup_vars vars1' vars2')
else if c < 0 then z1::(cup_vars vars1' vars2)
else z2::(cup_vars vars1 vars2')
| vars, [] | [], vars -> vars
let occ (x1,x1v) = if x1v then (x1,1,0) else (x1,0,1)
let rec cup_vars' vars1 vars2 = match (vars1,vars2) with
| (x1,x1v)::vars1', (x2,p2,n2)::vars2' ->
let c = X.compare x1 x2 in
if c = 0 then assert false (* x1::(cup_vars' vars1' vars2') *)
else if c < 0 then
(if x1v then (x1,1,0) else (x1,0,1))::(cup_vars' vars1' vars2)
else (x2,n2,p2)::(cup_vars' vars1 vars2')
| vars, [] -> List.map occ vars
| [], vars -> List.map (fun (x,p,n) -> (x,n,p)) vars
let compute_allvars subs vars =
cup_vars' vars
(List.fold_left (fun accu f -> cup_vars accu f.allvars) [] subs)
let rec cap_vars vars1 vars2 = match (vars1,vars2) with
| ((x1,xv1) as z1)::vars1', (x2,_,_)::vars2' ->
let c = X.compare x1 x2 in
if c = 0 then z1::(cap_vars vars1' vars2')
else if c < 0 then cap_vars vars1' vars2
else cap_vars vars1 vars2'
| _ -> []
let rec csubs s1 s2 = match s1,s2 with
| f1::s1', f2::s2' ->
if f1 == f2 then f1::(csubs s1' s2')
else if f1.id < f2.id then f1::(csubs s1' s2)
else f2::(csubs s1 s2')
| [], [] -> []
| s, [] | [], s -> s
let print_vars v =
List.iter (fun (x,b) -> Printf.printf "[%i:%b]" (X.hash x) b) v;
print_newline ()
module H = struct
type t = f
let rec hash_vars accu = function
| (x,v)::r ->
hash_vars (65537 * accu + 257 * X.hash x + (if v then 1 else 0)) r
| [] -> accu
let rec hash_subs accu = function
| f::r -> hash_subs (257 * accu + f.id) r
| [] -> accu
let hash f = hash_vars (hash_subs 1 f.subs) f.vars
let dump_vars ppf v =
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "|" in
V.iter (fun x -> sep (); Format.fprintf ppf "%i" (X.hash x)) v
let dump_subs ppf v =
let first = ref true in
let sep () = if !first then first := false else Format.fprintf ppf "|" in
F.iter (fun f -> sep (); Format.fprintf ppf "#%i:%a" f.id dump f) v
(*
let rec equal_vars vars1 vars2 = vars1 == vars2 || match vars1,vars2 with
| (x1,xv1)::(x1',xv1')::vars1,(x2,xv2)::(x2',xv2')::vars2 ->
xv1 == xv2 && xv1' == xv2' && X.equal x1 x2 &&
X.equal x1' x2' && equal_vars vars1 vars2
| [(x1,xv1)],[(x2,xv2)] ->
xv1 == xv2 && X.equal x1 x2
| _ -> false *)
let rec equal_vars vars1 vars2 = vars1 == vars2 || match vars1,vars2 with
| (x1,xv1)::vars1,(x2,xv2)::vars2 ->
xv1 == xv2 && X.equal x1 x2 && equal_vars vars1 vars2
| _ -> false
let rec equal_subs s1 s2 = s1 == s2 || match s1,s2 with
| f1::s1, f2::s2 -> f1 == f2 && equal_subs s1 s2
| _ -> false
let equal f1 f2 =
(f1 == f2) || ((f1.id = 0 || f2.id = 0) &&
equal_vars f1.vars f2.vars &&
equal_subs f1.subs f2.subs)
end
module W = Myweak.Make(H)
let mk =
let tbl = W.create 16387 in
let id = ref 0 in
fun vars subs ->
let f = W.merge tbl { tmpl with vars = vars; subs = subs } in
if (f.id = 0) then (
f.id <- (incr id; !id);
f.allvars <- compute_allvars subs vars;
);
f
let rec form f =
let rec aux1 accu = function
| x::l -> aux1 (B.cup accu (B.atom x)) l
| [] -> accu in
let rec aux2 accu = function
| x::l -> aux2 (B.cup accu (B.diff B.full (B.atom x))) l
| [] -> accu in
let accu = aux2 (aux1 B.empty f.pos) f.neg in
F.fold (fun f accu -> B.cup accu (B.diff B.full (form f))) f.subs accu
let empty = mk [] []
let full = mk [] [empty]
let check f = ()
let get f = match f.get with Some x -> x | None ->
let r = B.get (form f) in
f.get <- Some r;
r
*)
let posvar x = mk [x,true] []
let negvar x = mk [x,false] []
(* Hash-consing *)
module W = Weak.Make(
struct
type t = f
let hash f =
(V.hash f.pos)
+ 257 * (V.hash f.neg)
+ 65537 * (F.hash f.subs)
let equal f1 f2 =
V.equal f1.pos f2.pos
&& V.equal f1.neg f2.neg
&& F.equal f1.subs f2.subs
end
)
let tmpl = { pos = V.empty; neg = V.empty; subs = F.empty; id = 0 }
let mk_f = let id = ref 0 and tbl = W.create 16387 in
fun pos neg subs ->
assert (V.length pos + V.length neg + F.cardinal >= 2);
let f = W.merge tbl { pos = pos; neg = neg; subs = subs; id = 0 } in
if f.id = 0 then f.id <- (incr id; !id);
f
let neg = function
| { vars = [x,v]; subs = [] } -> mk [x, not v] []
| { vars = []; subs = [f] } -> f
| f -> mk [] [f]
let has_complement f1 f2 = List.memq f2 f1.subs
let is_complement f1 f2 =
match f1 with
| { vars = []; subs = [f] } -> f == f2
| _ -> match f2 with
| { vars = []; subs = [f] } -> f == f1
| _ -> false
exception One
| PosF x -> NegF x
| NegF x -> PosF x
| PosV x -> NegV x
| NegV x -> PosV x
| Zero -> One
| One -> Zero
let only_vars pos neg = match pos,neg with
| [x],[] -> PosV x
| [],[x] -> NegV x
| [], [] -> Zero
| _ -> PosF (mk_f pos neg Empty)
let mk pos neg subs = match pos,neg,subs with
| [],[],Empty -> Zero
| [x],[],Empty -> PosV x
| [],[x],Empty -> NegV x
| [],[],Leaf f -> NegF f
| _ -> PosF (mk_f pos neg subs)
let cap t1 t2 = match t1,t2 with
| Zero, t | t, Zero -> Zero
| One, t | t, One -> t
| PosV x, PosV y ->
let c = X.compare x y in
if c = 0 then t1
else PosF (mk_f (if c <0 then [x;y] else [y;x]) [] Empty)
| NegV x, NegV y ->
let c = X.compare x y in
if c = 0 then t1
else PosF (mk_f [] (if c <0 then [x;y] else [y;x]) Empty)
| PosV x, NegV y
| NegV y, PosV x -> if X.equal x y then Zero else PosF (mk_f [x] [y] Empty)
| PosF f, PosF g -> cap_f f g
| PosF f, NegF g
| NegF g, PosF f -> diff_f f g
| NegF f, NegF g -> nor_f f g
| (PosF f as t), PosV x
| PosV x, (PosF f as t) ->
if V.mem x f.pos then t
else if V.mem x f.neg then Zero
else PosF (mk_f
PosF { tmpl with pos = [x]; neg = [y];
allvars = if c <0 then [x;y] else [y;x] }
| PosV x, (PosF f as t)| (PosF f as t), PosV x ->
if V.mem f.pos x then t
else if V.mem f.neg x then One
else if V.mem f.allvars x
then zero_var_mk x (V.add x f.pos) f.neg f.subs
else
PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
allvars = V.add x f.allvars; subs = f.subs }
| PosV x, NegF f | NegF f, PosV x ->
if V.mem f.neg x then One
else if V.mem f.allvars x
then match zero_var_mk x f.pos f.neg f.subs with
| NegF f -> PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
allvars = V.add x f.allvars; subs = f.subs }
| PosF f -> PosF { tmpl with pos = [x];
allvars = V.add x f.allvars; subs = Leaf f }
| One -> PosV x
| Zero -> One
| PosV y ->
PosF { tmpl with pos = [x]; neg = [y];
allvars = if X.compare x y <0 then [x;y] else [y;x] }
| NegV y ->
let vs = if X.compare x y < 0 then [x;y] else [y;x] in
PosF { tmpl with pos = vs; allvars = vs }
else PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
allvars = V.add x f.allvars; subs = f.subs }
| NegF x, _ -> assert false
| PosF x, _ -> assert false
(*
type memo = { key1 : int array;
key2 : int array;
res : t array }
(* Memoization *)
type memo = { key1 : int array; key2 : int array; res : f array }
let new_memo n = { key1 = Array.create n (-1);
key2 = Array.create n (-1);
res = Array.create n empty }
let new_memo n = { key1 = Array.create n (-1); key2 = Array.create n (-1);
res = Array.create n tmpl }
let memo_cup = new_memo 16383
let memo_cap = new_memo 16383
let filrat tbl =
let o = ref 0 in
Array.iter (fun i -> if i >= 0 then incr o) tbl.key1;
!o
let memo_bin tbl g f1 f2 =
let h = ((f1.id + 1027 * f2.id) land max_int) mod (Array.length tbl.res) in
if (tbl.key1.(h) == f1.id) && (tbl.key2.(h) == f2.id) then
tbl.res.(h)
else
let r = g (f1,f2) in
let r = g f1 f2 in
tbl.key1.(h) <- f1.id;
tbl.key2.(h) <- f2.id;
tbl.res.(h) <- r;
r
let rec cvars vars1 vars2 = match (vars1,vars2) with
| ((x1,xv1) as z1)::vars1', ((x2,xv2) as z2)::vars2' ->
let c = X.compare x1 x2 in
if c = 0 then
if xv1 == xv2 then z1::(cvars vars1' vars2') else raise One
else if c < 0 then z1::(cvars vars1' vars2)
else z2::(cvars vars1 vars2')
| vars,[] | [],vars -> vars
let rec split_vars vars1 vars2 = match vars1,vars2 with
| ((x1,xv1) as z1)::vars1', ((x2,xv2) as z2)::vars2' ->
let c = X.compare x1 x2 in
if c = 0 then
let (vars1,common,vars2) = split_vars vars1' vars2' in
if xv1 == xv2 then (vars1,z1::common,vars2)
else (z1::vars1,common,z2::vars2)
else if c < 0 then
let (vars1,common,vars2) = split_vars vars1' vars2 in
z1::vars1,common,vars2
else
let (vars1,common,vars2) = split_vars vars1 vars2' in
vars1,common,z2::vars2
| vars1,vars2 -> vars1,[],vars2
let rec split_subs s1 s2 = match s1,s2 with
| f1::s1',f2::s2' ->
if f1 == f2 then
let (s1,common,s2) = split_subs s1' s2' in (s1,f1::common,s2)
else if f1.id < f2.id then
let (s1,common,s2) = split_subs s1' s2 in f1::s1,common,s2
else
let (s1,common,s2) = split_subs s1 s2' in s1,common,f2::s2
| s1,s2 -> s1,[],s2
let empty = mk V.empty V.empty F.empty
let full = mk V.empty V.empty (F.singleton empty)
let order_subs subs =
let rec clean = function
| f1::(f2::_ as z) -> if f1 == f2 then clean z else f1::(clean z)
| z -> z
in
clean (List.sort (fun f1 f2 -> f1.id - f2.id) subs)
let rec check f =
F.iter
(fun g ->
let n1 = V.length g.pos and n2 = V.length g.neg and n3 =
F.fold (fun _ x -> succ x) g.subs 0 in
if (n1 + n2 + n3 < 2) && f != full then
(Format.fprintf Format.std_formatter "BUG f=%a g=%a pos=%i neg=%i subs=%i@." dump f dump g n1 n2 n3;
assert false);
check g;
assert(V.disjoint f.pos g.allvars);
assert(V.disjoint f.neg g.allvars)) f.subs;
assert (V.disjoint f.pos f.neg)
let rec remove_complement f c =
let rec aux = function
| c'::r -> if (c == c') then r else c'::(aux r)
| _ -> assert false