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

Update the binary for better output when checking proofs

Browse source
This commit is contained in:
Guillaume Bury 2016-02-04 23:51:53 +01:00
parent 74be6cdc9f
commit a2809215ae
2 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
main.ml
View file

@ -228,19 +228,21 @@ let main () =
Gc.delete_alarm al;
begin match res with
| Smt.Sat ->
print "Sat (%f)" (Sys.time ());
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists Smt.eval) cnf) then
raise Incorrect_model
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Smt.Unsat ->
print "Unsat (%f)" (Sys.time ());
let t = Sys.time () in
if !p_check then begin
let p = Smt.get_proof () in
Smt.Proof.check p;
print_proof p;
if !p_unsat_core then
print_unsat_core (Smt.unsat_core p)
end
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
| Mcsat ->
Mcsat.assume cnf;
@ -248,19 +250,21 @@ let main () =
Gc.delete_alarm al;
begin match res with
| Mcsat.Sat ->
print "Sat (%f)" (Sys.time ());
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists Mcsat.eval) cnf) then
raise Incorrect_model
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Mcsat.Unsat ->
print "Unsat (%f)" (Sys.time ());
let t = Sys.time () in
if !p_check then begin
let p = Mcsat.get_proof () in
Mcsat.Proof.check p;
print_mcproof p;
if !p_unsat_core then
print_mc_unsat_core (Mcsat.unsat_core p)
end
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
let () =

1
util/parsedimacs.ml
View file

@ -21,6 +21,7 @@ let rec _read_word s acc i len =
let acc = String.sub s i len :: acc in
_skip_space s acc (i+len+1)
| _ -> _read_word s acc i (len+1)
and _skip_space s acc i =
if i=String.length s
then acc