264 (* ------------------------------------------------------------------------- *) |
264 (* ------------------------------------------------------------------------- *) |
265 (* string_of_prop_formula: return a human-readable string representation of *) |
265 (* string_of_prop_formula: return a human-readable string representation of *) |
266 (* a 'prop_formula' (just for tracing) *) |
266 (* a 'prop_formula' (just for tracing) *) |
267 (* ------------------------------------------------------------------------- *) |
267 (* ------------------------------------------------------------------------- *) |
268 |
268 |
269 fun string_of_prop_formula PropLogic.True = "True" |
269 fun string_of_prop_formula Prop_Logic.True = "True" |
270 | string_of_prop_formula PropLogic.False = "False" |
270 | string_of_prop_formula Prop_Logic.False = "False" |
271 | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i |
271 | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i |
272 | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm |
272 | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm |
273 | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = |
273 | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) = |
274 "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" |
274 "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" |
275 | string_of_prop_formula (PropLogic.And (fm1, fm2)) = |
275 | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) = |
276 "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; |
276 "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; |
277 |
277 |
278 (* ------------------------------------------------------------------------- *) |
278 (* ------------------------------------------------------------------------- *) |
279 (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) |
279 (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) |
280 (* a proof from the resulting proof trace of the SAT solver. The *) |
280 (* a proof from the resulting proof trace of the SAT solver. The *) |
311 val _ = |
311 val _ = |
312 if !trace_sat then |
312 if !trace_sat then |
313 tracing ("Sorted non-trivial clauses:\n" ^ |
313 tracing ("Sorted non-trivial clauses:\n" ^ |
314 cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) |
314 cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) |
315 else () |
315 else () |
316 (* translate clauses from HOL terms to PropLogic.prop_formula *) |
316 (* translate clauses from HOL terms to Prop_Logic.prop_formula *) |
317 val (fms, atom_table) = |
317 val (fms, atom_table) = |
318 fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) |
318 fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) |
319 sorted_clauses Termtab.empty |
319 sorted_clauses Termtab.empty |
320 val _ = |
320 val _ = |
321 if !trace_sat then |
321 if !trace_sat then |
322 tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) |
322 tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) |
323 else () |
323 else () |
324 val fm = PropLogic.all fms |
324 val fm = Prop_Logic.all fms |
325 (* unit -> Thm.thm *) |
325 (* unit -> Thm.thm *) |
326 fun make_quick_and_dirty_thm () = |
326 fun make_quick_and_dirty_thm () = |
327 let |
327 let |
328 val _ = |
328 val _ = |
329 if !trace_sat then |
329 if !trace_sat then |