simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(sat): produce DRUP proofs if asked to

Browse source
This commit is contained in:
Simon Cruanes 2021-08-02 23:48:04 -04:00
parent b9800023ec
commit e6fc7e7357
1 changed files with 31 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/main/main.ml
View file

@ -143,15 +143,44 @@ let main_smt ~dot_proof () : _ result =
let main_cnf () : _ result =
let module S = Pure_sat_solver in
let close_proof_, on_learnt, on_gc =
if !proof_file ="" then (
(fun() -> ()), None, None
) else (
let oc = open_out !proof_file in
let pp_c solver c =
let store = S.SAT.store solver in
Array.iteri (fun i a ->
if i>0 then output_char oc ' ';
let v = S.SAT.Atom.formula store a in
output_string oc (string_of_int v))
c
in
let on_learnt solver c =
pp_c solver c; output_string oc " 0\n";
and on_gc solver c =
output_string oc "d "; pp_c solver c; output_string oc " 0\n";
()
and close () =
flush oc;
close_out_noerr oc;
in
close, Some on_learnt, Some on_gc
)
in
let n_atoms = ref 0 in
let solver =
S.SAT.create
~on_new_atom:(fun _ -> incr n_atoms)
~size:`Big ()
~on_new_atom:(fun _ _ -> incr n_atoms) ~size:`Big ()
?on_learnt ?on_gc
in
S.Dimacs.parse_file solver !file >>= fun () ->
let r = S.solve ~check:!check solver in
close_proof_();
if !p_stat then (
Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@.\
; n-restarts: %d n-atoms: %d@."