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

feat: enforce time/memory limits in main runner

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 13:09:48 -05:00
parent e177534a46
commit 20791a551f
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 17 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/main/main.ml
View file

@ -23,7 +23,7 @@ let p_proof = ref false
let p_model = ref false
let check = ref false
let time_limit = ref 300.
let size_limit = ref 1000_000_000.
let size_limit = ref 1_000_000_000.
let restarts = ref true
let gc = ref true
let p_stat = ref false

20
src/smtlib/Process.ml
View file

@ -145,15 +145,27 @@ let solve
?proof_file
?(pp_model=false)
?(check=false)
?time:_ ?memory:_ ?(progress=false)
?time ?memory ?(progress=false)
~assumptions
s : Solver.res =
let t1 = Sys.time() in
let on_progress =
if progress then Some (mk_progress s) else None in
let on_progress = if progress then Some (mk_progress s) else None in
let should_stop = match time, memory with
| None, None -> None
| _ ->
let time = CCOpt.get_or ~default:3600. time in (* default: 1 hour *)
let memory = CCOpt.get_or ~default:4e9 memory in (* default: 4 GB *)
let stop _ _ =
Sys.time () -. t1 > time ||
(Gc.quick_stat()).Gc.major_words *. 8. > memory
in
Some stop
in
let res =
Profile.with_ "solve" begin fun () ->
Solver.solve ~assumptions ?on_progress s
Solver.solve ~assumptions ?on_progress ?should_stop s
(* ?gc ?restarts ?time ?memory ?progress *)
end
in