let rec make_formula_set sa = F.make F.And (SAtom.fold (fun a l -> make_literal a::l) sa []) and make_literal = function | Atom.True -> F.f_true | Atom.False -> F.f_false | Atom.Comp (x, op, y) -> let tx = make_term x in let ty = make_term y in F.make_lit (make_op_comp op) [tx; ty] | Atom.Ite (la, a1, a2) -> let f = make_formula_set la in let a1 = make_literal a1 in let a2 = make_literal a2 in let ff1 = F.make F.Imp [f; a1] in let ff2 = F.make F.Imp [F.make F.Not [f]; a2] in F.make F.And [ff1; ff2]