| Ast.NotEq (a,b) -> false, Ast.Function ("==",[Ast.Constant "_"; a; b])
;;
-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)
| Ast.NegAtom _ -> assert false
;;
+let trans_formulae = trans_formulae ([],[]);;
+
(* HELPERS *)
let resolve ~tptppath s =
| Ast.Comment _ :: tl -> aux p n tl
| Ast.AnnotatedFormula (name,
(Ast.Axiom | Ast.Hypothesis|Ast.Negated_conjecture), f,_,_) :: tl->
- let is_positive, f = trans_formulae f in
- if is_positive then aux (p@[Ast.Constant name,f]) n tl
- else aux p (n@[Ast.Constant name,f]) tl
+ let (nlit,plit) = trans_formulae f in
+ if plit = [] then aux p (n@[Ast.Constant name,(nlit,plit)]) tl
+ else aux (p@[Ast.Constant name,(nlit,plit)]) n tl
| _ -> prerr_endline "bad syntax"; assert false
in
aux [] [] statements