-let trans_formulae = function
- | Ast.Disjunction _ -> assert false
- | Ast.Atom a -> trans_atom a
+let rec trans_formulae (nlit,plit) = function
+ | Ast.Disjunction (a,b) ->
+ trans_formulae (trans_formulae (nlit,plit) b) a
+ | Ast.Atom a ->
+ let is_positive,lit = trans_atom a in
+ if is_positive then (nlit,lit::plit) else (lit::nlit,plit)