From 20791a551fecbb5fd863f509ff7f040bd0933a03 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 17 Feb 2022 13:09:48 -0500
Subject: [PATCH] feat: enforce time/memory limits in main runner

---
 src/main/main.ml      |  2 +-
 src/smtlib/Process.ml | 20 ++++++++++++++++----
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 75e31693..b4fdf611 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -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
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 5f04bc45..e532a03f 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -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