-let rec atom_of_formula = function
- | A.Disjunction (a,b) ->
- atom_of_formula a @ atom_of_formula b
- | A.NegAtom a -> [a] (* removes the negation *)
- | A.Atom a -> [a]
+let rec atom_of_formula neg pos = function
+ | A.Disjunction (a,b) ->
+ let neg, pos = atom_of_formula neg pos a in
+ atom_of_formula neg pos b
+ | A.NegAtom a -> a::neg, pos
+ | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
+ | A.Atom a -> neg, a::pos
+;;
+
+let atom_of_formula f =
+ let neg, pos = atom_of_formula [] [] f in
+ neg @ pos