equal
deleted
inserted
replaced
795 fun zchaff_with_proofs fm = |
795 fun zchaff_with_proofs fm = |
796 case SatSolver.invoke_solver "zchaff" fm of |
796 case SatSolver.invoke_solver "zchaff" fm of |
797 SatSolver.UNSATISFIABLE NONE => |
797 SatSolver.UNSATISFIABLE NONE => |
798 (let |
798 (let |
799 (* string list *) |
799 (* string list *) |
|
800 (* FIXME File.tmp_path (!?) *) |
800 val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) |
801 val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) |
801 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" |
802 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" |
802 fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = |
803 fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = |
803 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
804 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
804 | cnf_number_of_clauses _ = 1 |
805 | cnf_number_of_clauses _ = 1 |