equal
deleted
inserted
replaced
275 (* int list -> int list list *) |
275 (* int list -> int list list *) |
276 fun clauses xs = |
276 fun clauses xs = |
277 let |
277 let |
278 val (xs1, xs2) = take_prefix (fn i => i <> 0) xs |
278 val (xs1, xs2) = take_prefix (fn i => i <> 0) xs |
279 in |
279 in |
280 xs1 :: clauses (tl xs2) |
280 case xs2 of |
|
281 [] => [xs1] |
|
282 | (0::[]) => [xs1] |
|
283 | (0::tl) => xs1 :: clauses tl |
281 end |
284 end |
282 (* int -> PropLogic.prop_formula *) |
285 (* int -> PropLogic.prop_formula *) |
283 fun literal_from_int i = |
286 fun literal_from_int i = |
284 (assert (i<>0) "variable index in DIMACS CNF file is 0"; |
287 (assert (i<>0) "variable index in DIMACS CNF file is 0"; |
285 if i>0 then |
288 if i>0 then |