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

Update for latest version of dolmen

Browse source
This commit is contained in:
Guillaume Bury 2018-09-11 14:19:37 +02:00
parent 5e57bfc827
commit 4bb1f5b793
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/main.ml
View file

@ -88,13 +88,14 @@ module Make
| Dolmen.Statement.Pack [ | Dolmen.Statement.Pack [
{ Dolmen.Statement.descr = Dolmen.Statement.Push 1; }; { Dolmen.Statement.descr = Dolmen.Statement.Push 1; };
{ Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; }; { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; };
{ Dolmen.Statement.descr = Dolmen.Statement.Prove; }; { Dolmen.Statement.descr = Dolmen.Statement.Prove []; };
{ Dolmen.Statement.descr = Dolmen.Statement.Pop 1; }; { Dolmen.Statement.descr = Dolmen.Statement.Pop 1; };
] -> ] ->
let assumptions = T.assumptions f in let assumptions = T.assumptions f in
prove ~assumptions prove ~assumptions
| Dolmen.Statement.Prove -> | Dolmen.Statement.Prove l ->
prove ~assumptions:[] let assumptions = List.map T.assumptions l in
prove ~assumptions
| Dolmen.Statement.Set_info _ | Dolmen.Statement.Set_info _
| Dolmen.Statement.Set_logic _ -> () | Dolmen.Statement.Set_logic _ -> ()
| Dolmen.Statement.Exit -> exit 0 | Dolmen.Statement.Exit -> exit 0
@ -205,7 +206,7 @@ let main () =
List.iter S.do_task input; List.iter S.do_task input;
(* Small hack for dimacs, which do not output a "Prove" statement *) (* Small hack for dimacs, which do not output a "Prove" statement *)
begin match lang with begin match lang with
| P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat () | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat []
| _ -> () | _ -> ()
end; end;
Gc.delete_alarm al; Gc.delete_alarm al;