equal
deleted
inserted
replaced
298 in |
298 in |
299 case SatSolver.invoke_solver (!solver) fm of |
299 case SatSolver.invoke_solver (!solver) fm of |
300 SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( |
300 SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( |
301 if !trace_sat then |
301 if !trace_sat then |
302 tracing ("Proof trace from SAT solver:\n" ^ |
302 tracing ("Proof trace from SAT solver:\n" ^ |
303 "clauses: [" ^ commas (map (fn (c, cs) => |
303 "clauses: " ^ string_of_list (string_of_pair string_of_int (string_of_list string_of_int)) (Inttab.dest clause_table) ^ "\n" ^ |
304 "(" ^ string_of_int c ^ ", [" ^ commas (map string_of_int cs) ^ "])") (Inttab.dest clause_table)) ^ "]\n" ^ |
|
305 "empty clause: " ^ string_of_int empty_id) |
304 "empty clause: " ^ string_of_int empty_id) |
306 else (); |
305 else (); |
307 if !quick_and_dirty then |
306 if !quick_and_dirty then |
308 make_quick_and_dirty_thm () |
307 make_quick_and_dirty_thm () |
309 else |
308 else |