24 (unit -> result) -> solver |
24 (unit -> result) -> solver |
25 |
25 |
26 val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula |
26 val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula |
27 |
27 |
28 (* generic solver interface *) |
28 (* generic solver interface *) |
29 val solvers : (string * solver) list ref |
29 val solvers : (string * solver) list Unsynchronized.ref |
30 val add_solver : string * solver -> unit |
30 val add_solver : string * solver -> unit |
31 val invoke_solver : string -> solver (* exception Option *) |
31 val invoke_solver : string -> solver (* exception Option *) |
32 end; |
32 end; |
33 |
33 |
34 structure SatSolver : SAT_SOLVER = |
34 structure SatSolver : SAT_SOLVER = |
361 |
361 |
362 (* ------------------------------------------------------------------------- *) |
362 (* ------------------------------------------------------------------------- *) |
363 (* solvers: a (reference to a) table of all registered SAT solvers *) |
363 (* solvers: a (reference to a) table of all registered SAT solvers *) |
364 (* ------------------------------------------------------------------------- *) |
364 (* ------------------------------------------------------------------------- *) |
365 |
365 |
366 val solvers = ref ([] : (string * solver) list); |
366 val solvers = Unsynchronized.ref ([] : (string * solver) list); |
367 |
367 |
368 (* ------------------------------------------------------------------------- *) |
368 (* ------------------------------------------------------------------------- *) |
369 (* add_solver: updates 'solvers' by adding a new solver *) |
369 (* add_solver: updates 'solvers' by adding a new solver *) |
370 (* ------------------------------------------------------------------------- *) |
370 (* ------------------------------------------------------------------------- *) |
371 |
371 |
627 | init_array (fm, n) = |
627 | init_array (fm, n) = |
628 (Array.update (clauses, n, clause_to_lit_list fm); n+1) |
628 (Array.update (clauses, n, clause_to_lit_list fm); n+1) |
629 val _ = init_array (cnf, 0) |
629 val _ = init_array (cnf, 0) |
630 (* optimization for the common case where MiniSat "R"s clauses in their *) |
630 (* optimization for the common case where MiniSat "R"s clauses in their *) |
631 (* original order: *) |
631 (* original order: *) |
632 val last_ref_clause = ref (number_of_clauses - 1) |
632 val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) |
633 (* search the 'clauses' array for the given list of literals 'lits', *) |
633 (* search the 'clauses' array for the given list of literals 'lits', *) |
634 (* starting at index '!last_ref_clause + 1' *) |
634 (* starting at index '!last_ref_clause + 1' *) |
635 (* int list -> int option *) |
635 (* int list -> int option *) |
636 fun original_clause_id lits = |
636 fun original_clause_id lits = |
637 let |
637 let |
659 case Int.fromString s of |
659 case Int.fromString s of |
660 SOME i => i |
660 SOME i => i |
661 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
661 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
662 ) |
662 ) |
663 (* parse the proof file *) |
663 (* parse the proof file *) |
664 val clause_table = ref (Inttab.empty : int list Inttab.table) |
664 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) |
665 val empty_id = ref ~1 |
665 val empty_id = Unsynchronized.ref ~1 |
666 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) |
666 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) |
667 (* our proof format, where original clauses are numbered starting from 0 *) |
667 (* our proof format, where original clauses are numbered starting from 0 *) |
668 val clause_id_map = ref (Inttab.empty : int Inttab.table) |
668 val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table) |
669 fun sat_to_proof id = ( |
669 fun sat_to_proof id = ( |
670 case Inttab.lookup (!clause_id_map) id of |
670 case Inttab.lookup (!clause_id_map) id of |
671 SOME id' => id' |
671 SOME id' => id' |
672 | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") |
672 | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") |
673 ) |
673 ) |
674 val next_id = ref (number_of_clauses - 1) |
674 val next_id = Unsynchronized.ref (number_of_clauses - 1) |
675 (* string list -> unit *) |
675 (* string list -> unit *) |
676 fun process_tokens [] = |
676 fun process_tokens [] = |
677 () |
677 () |
678 | process_tokens (tok::toks) = |
678 | process_tokens (tok::toks) = |
679 if tok="R" then ( |
679 if tok="R" then ( |
706 fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." |
706 fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." |
707 | unevens (x :: []) = x :: [] |
707 | unevens (x :: []) = x :: [] |
708 | unevens (x :: _ :: xs) = x :: unevens xs |
708 | unevens (x :: _ :: xs) = x :: unevens xs |
709 val rs = (map sat_to_proof o unevens o map int_from_string) ids |
709 val rs = (map sat_to_proof o unevens o map int_from_string) ids |
710 (* extend the mapping of clause IDs with this newly defined ID *) |
710 (* extend the mapping of clause IDs with this newly defined ID *) |
711 val proof_id = inc next_id |
711 val proof_id = Unsynchronized.inc next_id |
712 val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
712 val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
713 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") |
713 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") |
714 in |
714 in |
715 (* update clause table *) |
715 (* update clause table *) |
716 clause_table := Inttab.update_new (proof_id, rs) (!clause_table) |
716 clause_table := Inttab.update_new (proof_id, rs) (!clause_table) |
819 case Int.fromString s of |
819 case Int.fromString s of |
820 SOME i => i |
820 SOME i => i |
821 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
821 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
822 ) |
822 ) |
823 (* parse the "resolve_trace" file *) |
823 (* parse the "resolve_trace" file *) |
824 val clause_offset = ref ~1 |
824 val clause_offset = Unsynchronized.ref ~1 |
825 val clause_table = ref (Inttab.empty : int list Inttab.table) |
825 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) |
826 val empty_id = ref ~1 |
826 val empty_id = Unsynchronized.ref ~1 |
827 (* string list -> unit *) |
827 (* string list -> unit *) |
828 fun process_tokens [] = |
828 fun process_tokens [] = |
829 () |
829 () |
830 | process_tokens (tok::toks) = |
830 | process_tokens (tok::toks) = |
831 if tok="CL:" then ( |
831 if tok="CL:" then ( |