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

test: check unsat cores in icnf-solve

Browse source
This commit is contained in:
Simon Cruanes 2019-01-19 18:13:29 -06:00 • committed by Guillaume Bury
parent 52ae127a5d
commit f8281bfcc2
2 changed files with 27 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/Makefile
View file

@ -2,7 +2,7 @@
test-icnf: test-icnf:
@for i in regression/*.icnf ; do \ @for i in regression/*.icnf ; do \
echo "test problem $$i"; \ echo "test problem $$i"; \
./icnf-solve/icnf_solve.exe $$i > regression/.`basename $$i`.out 2>/dev/null ; \ ./icnf-solve/icnf_solve.exe --check $$i > regression/.`basename $$i`.out 2>/dev/null ; \
diff regression/.`basename $$i`.out regression/.`basename $$i`.ref \ diff regression/.`basename $$i`.out regression/.`basename $$i`.ref \
|| ( echo "mismatch for $$i" ; exit 1) ; \ || ( echo "mismatch for $$i" ; exit 1) ; \
done done

34
tests/icnf-solve/icnf_solve.ml
View file

@ -69,11 +69,13 @@ module Solver = struct
let solve s ass = let solve s ass =
let ass = Array.to_list ass in let ass = Array.to_list ass in
match S.solve ~assumptions:ass s () with match S.solve ~assumptions:ass s () with
| S.Sat _ -> true | S.Sat _ -> Ok ()
| S.Unsat _ -> false | S.Unsat { unsat_assumptions; _ } ->
let core = unsat_assumptions() in
Error core
end end
let solve_with_solver ~debug file : unit = let solve_with_solver ~check ~debug file : unit =
Printf.eprintf "c process %S\n%!" file; Printf.eprintf "c process %S\n%!" file;
let s = Solver.make () in let s = Solver.make () in
let pp_arr out a = let pp_arr out a =
@ -97,8 +99,22 @@ let solve_with_solver ~debug file : unit =
if debug then ( if debug then (
Printf.printf "c solve %a\n%!" pp_arr assumptions; Printf.printf "c solve %a\n%!" pp_arr assumptions;
); );
let r = Solver.solve s assumptions in begin match Solver.solve s assumptions with
Printf.printf "%s\n%!" (if r then "SAT" else "UNSAT"); | Ok () -> Printf.printf "SAT\n%!"
| Error (_::_ as core) when check ->
Printf.printf "UNSAT\n%!";
let core = Array.of_list core in
if debug then Printf.printf "check unsat core %a\n" pp_arr core;
(* check unsat core *)
begin match Solver.solve s core with
| Ok () ->
Printf.printf "error: unsat core %a is SAT\n%!" pp_arr core;
exit 1
| Error _ -> ()
end;
| Error _ ->
Printf.printf "UNSAT\n%!";
end;
(* next problem! *) (* next problem! *)
process_problem() process_problem()
| exception End_of_file -> | exception End_of_file ->
@ -114,8 +130,8 @@ let solve_with_solver ~debug file : unit =
in in
process_problem () process_problem ()
let solve_with_file ~debug file : unit = let solve_with_file ~check ~debug file : unit =
try solve_with_solver ~debug file try solve_with_solver ~check ~debug file
with e -> with e ->
Printf.printf "error while solving %S:\n%s" Printf.printf "error while solving %S:\n%s"
file (Printexc.to_string e); file (Printexc.to_string e);
@ -124,9 +140,11 @@ let solve_with_file ~debug file : unit =
let () = let () =
let files = ref [] in let files = ref [] in
let debug = ref false in let debug = ref false in
let check = ref false in
let opts = [ let opts = [
"-d", Arg.Set debug, " debug"; "-d", Arg.Set debug, " debug";
"--check", Arg.Set check, " check unsat cores";
] |> Arg.align in ] |> Arg.align in
Arg.parse opts (fun f -> files := f :: !files) "icnf_solve [options] <file>"; Arg.parse opts (fun f -> files := f :: !files) "icnf_solve [options] <file>";
List.iter (fun f -> solve_with_file ~debug:!debug f) !files; List.iter (fun f -> solve_with_file ~check:!check ~debug:!debug f) !files;
() ()