328 Formula (ident, Hypothesis, mk_anot phi, source, info) |
328 Formula (ident, Hypothesis, mk_anot phi, source, info) |
329 | negate_conjecture_line line = line |
329 | negate_conjecture_line line = line |
330 |
330 |
331 exception CLAUSIFY of unit |
331 exception CLAUSIFY of unit |
332 |
332 |
333 fun clausify_formula pos (phi as AAtom _) = phi |> not pos ? mk_anot |
333 (* This "clausification" only expands syntactic sugar, such as "phi => psi" to |
334 | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi |
334 "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't |
335 | clausify_formula false (AConn (AAnd, phis)) = |
335 attempt to distribute conjunctions over disjunctions. *) |
336 AConn (AOr, map (clausify_formula false) phis) |
336 fun clausify_formula1 pos (phi as AAtom _) = phi |> not pos ? mk_anot |
337 | clausify_formula true (AConn (AOr, phis)) = |
337 | clausify_formula1 pos (AConn (ANot, [phi])) = clausify_formula1 (not pos) phi |
338 AConn (AOr, map (clausify_formula true) phis) |
338 | clausify_formula1 false (AConn (AAnd, phis)) = |
339 | clausify_formula true (AConn (AImplies, [phi1, phi2])) = |
339 AConn (AOr, map (clausify_formula1 false) phis) |
340 AConn (AOr, [clausify_formula false phi1, clausify_formula true phi2]) |
340 | clausify_formula1 true (AConn (AOr, phis)) = |
341 | clausify_formula true (AConn (AIf, phis)) = |
341 AConn (AOr, map (clausify_formula1 true) phis) |
342 clausify_formula true (AConn (AImplies, rev phis)) |
342 | clausify_formula1 true (AConn (AImplies, [phi1, phi2])) = |
343 | clausify_formula _ _ = raise CLAUSIFY () |
343 AConn (AOr, [clausify_formula1 false phi1, clausify_formula1 true phi2]) |
|
344 | clausify_formula1 true (AConn (AIf, phis)) = |
|
345 clausify_formula1 true (AConn (AImplies, rev phis)) |
|
346 | clausify_formula1 _ _ = raise CLAUSIFY () |
|
347 fun clausify_formula true (AConn (AIff, phis)) = |
|
348 [clausify_formula1 true (AConn (AIf, phis)), |
|
349 clausify_formula1 true (AConn (AImplies, phis))] |
|
350 | clausify_formula false (AConn (ANotIff, phis)) = |
|
351 clausify_formula true (AConn (AIff, phis)) |
|
352 | clausify_formula pos phi = [clausify_formula1 pos phi] |
344 |
353 |
345 fun clausify_formula_line (Formula (ident, kind, phi, source, info)) = |
354 fun clausify_formula_line (Formula (ident, kind, phi, source, info)) = |
346 (case try (clausify_formula true) phi of |
355 let |
347 SOME phi => SOME (Formula (ident, kind, phi, source, info)) |
356 val (n, phis) = phi |> try (clausify_formula true) |> these |> `length |
348 | NONE => NONE) |
357 in |
349 | clausify_formula_line _ = NONE |
358 map2 (fn phi => fn j => |
|
359 Formula (ident ^ |
|
360 (if n > 1 then "_cls" ^ string_of_int j else ""), |
|
361 kind, phi, source, info)) |
|
362 phis (1 upto n) |
|
363 end |
|
364 | clausify_formula_line _ = [] |
350 |
365 |
351 fun ensure_cnf_problem_line line = |
366 fun ensure_cnf_problem_line line = |
352 line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line |
367 line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line |
353 |
368 |
354 fun ensure_cnf_problem problem = |
369 fun ensure_cnf_problem problem = |
355 problem |> map (apsnd (map_filter ensure_cnf_problem_line)) |
370 problem |> map (apsnd (maps ensure_cnf_problem_line)) |
356 |
371 |
357 fun filter_cnf_ueq_problem problem = |
372 fun filter_cnf_ueq_problem problem = |
358 problem |
373 problem |
359 |> map (apsnd (map open_formula_line |
374 |> map (apsnd (map open_formula_line |
360 #> filter is_problem_line_cnf_ueq |
375 #> filter is_problem_line_cnf_ueq |