equal
deleted
inserted
replaced
534 let |
534 let |
535 val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile) |
535 val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile) |
536 fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) |
536 fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) |
537 | and_to_list fm acc = rev (fm :: acc) |
537 | and_to_list fm acc = rev (fm :: acc) |
538 val clauses = and_to_list prop_fm [] |
538 val clauses = and_to_list prop_fm [] |
539 val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) |
539 val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses |
540 clauses |
540 val cterms = map (Thm.cterm_of @{theory}) terms |
541 val cterms = map (Thm.cterm_of @{theory}) terms |
541 val start = Timing.start () |
542 val timer = start_timing () |
542 val thm = sat.rawsat_thm @{context} cterms |
543 val thm = sat.rawsat_thm @{context} cterms |
|
544 in |
543 in |
545 (end_timing timer, !sat.counter) |
544 (Timing.result start, ! sat.counter) |
546 end; |
545 end; |
547 *} |
546 *} |
548 |
547 |
549 end |
548 end |