equal
deleted
inserted
replaced
231 |
231 |
232 fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = |
232 fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = |
233 let |
233 let |
234 (* string -> int list *) |
234 (* string -> int list *) |
235 fun int_list_from_string s = |
235 fun int_list_from_string s = |
236 List.mapPartial Int.fromString (space_explode " " s) |
236 map_filter Int.fromString (space_explode " " s) |
237 (* int list -> assignment *) |
237 (* int list -> assignment *) |
238 fun assignment_from_list [] i = |
238 fun assignment_from_list [] i = |
239 NONE (* the SAT solver didn't provide a value for this variable *) |
239 NONE (* the SAT solver didn't provide a value for this variable *) |
240 | assignment_from_list (x::xs) i = |
240 | assignment_from_list (x::xs) i = |
241 if x=i then (SOME true) |
241 if x=i then (SOME true) |
348 (conjunction |
348 (conjunction |
349 o (map disjunction) |
349 o (map disjunction) |
350 o (map (map literal_from_int)) |
350 o (map (map literal_from_int)) |
351 o clauses |
351 o clauses |
352 o (map int_from_string) |
352 o (map int_from_string) |
353 o List.concat |
353 o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) |
354 o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) |
|
355 o filter_preamble |
354 o filter_preamble |
356 o (List.filter (fn l => l <> "")) |
355 o (List.filter (fn l => l <> "")) |
357 o split_lines |
356 o split_lines |
358 o File.read) |
357 o File.read) |
359 path |
358 path |