equal
deleted
inserted
replaced
532 val prop_fm = SAT_Solver.read_dimacs_cnf_file (Path.explode dimacsfile) |
532 val prop_fm = SAT_Solver.read_dimacs_cnf_file (Path.explode dimacsfile) |
533 fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) |
533 fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) |
534 | and_to_list fm acc = rev (fm :: acc) |
534 | and_to_list fm acc = rev (fm :: acc) |
535 val clauses = and_to_list prop_fm [] |
535 val clauses = and_to_list prop_fm [] |
536 val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses |
536 val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses |
537 val cterms = map (Thm.cterm_of @{context}) terms |
537 val cterms = map (Thm.cterm_of \<^context>) terms |
538 val start = Timing.start () |
538 val start = Timing.start () |
539 val _ = SAT.rawsat_thm @{context} cterms |
539 val _ = SAT.rawsat_thm \<^context> cterms |
540 in |
540 in |
541 (Timing.result start, ! SAT.counter) |
541 (Timing.result start, ! SAT.counter) |
542 end; |
542 end; |
543 \<close> |
543 \<close> |
544 |
544 |