fix(main): properly handle option no-restarts

src/sat/Internal.ml

@@ -1434,7 +1434,7 @@ module Make (Th : Theory_intf.S) = struct
 
   (* do some amount of search, until the number of conflicts or clause learnt
      reaches the given parameters *)
-  let search (st:t) n_of_conflicts n_of_learnts : unit =
+  let search ~restarts (st:t) n_of_conflicts n_of_learnts : unit =
     let conflictC = ref 0 in
     while true do
       check_invariants st;
@@ -1447,8 +1447,8 @@ module Make (Th : Theory_intf.S) = struct
         assert (st.elt_head = Vec.size st.trail);
         assert (st.elt_head = st.th_head);
         if Vec.size st.trail = n_vars st then raise Sat;
-        if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
-          Log.debug 3 "(sat.restarting)";
+        if restarts && n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
+          Log.debug 2 "(sat.restarting)";
           cancel_until st (base_level st);
           raise Restart
         );
@@ -1508,7 +1508,7 @@ module Make (Th : Theory_intf.S) = struct
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
-  let solve ?(assumptions=[]) (st:t) : unit =
+  let solve ?(restarts=true) ?(assumptions=[]) (st:t) : unit =
     Log.debug 5 "(sat.solve)";
     if is_unsat st then raise Unsat;
     let n_of_conflicts = ref (float_of_int restart_first) in
@@ -1523,11 +1523,12 @@ module Make (Th : Theory_intf.S) = struct
         add_boolean_conflict st c;
         call_solve()
     and call_solve() =
-      match search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) with
+      match search ~restarts st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) with
       | () -> ()
       | exception Restart ->
         n_of_conflicts := !n_of_conflicts *. restart_inc;
-        n_of_learnts   := !n_of_learnts *. learntsize_inc
+        n_of_learnts   := !n_of_learnts *. learntsize_inc;
+        check_invariants st
       | exception Conflict c ->
         add_boolean_conflict st c;
         call_solve()

src/sat/Solver.ml

@@ -75,9 +75,9 @@ module Make (Th : Theory_intf.S) = struct
   let[@inline] add_clause ~permanent st c : unit =
     S.add_clause_user ~permanent st c
 
-  let solve (st:t) ?(assumptions=[]) () =
+  let solve ?(restarts=true) (st:t) ?(assumptions=[]) () =
     try
-      S.solve ~assumptions st;
+      S.solve ~restarts ~assumptions st;
       Sat (mk_sat st)
     with S.Unsat ->
       Unsat (mk_unsat st)

src/sat/Solver_intf.ml

@@ -105,7 +105,7 @@ module type S = sig
   (** Lower level addition of clauses. See {!Clause} to create clauses.
       @param permanent if true, kept after backtracking *)
 
-  val solve : t -> ?assumptions:formula list -> unit -> res
+  val solve : ?restarts:bool -> t -> ?assumptions:formula list -> unit -> res
   (** Try and solves the current set of clauses.
       @param assumptions additional atomic assumptions to be temporarily added.
         The assumptions are just used for this call to [solve], they are

src/smt/Solver.ml

@@ -208,8 +208,8 @@ let check_model (s:t) : unit =
 
 (* TODO: main loop with iterative deepening of the unrolling  limit
    (not the value depth limit) *)
-let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res =
-  let r = Sat_solver.solve ~assumptions (solver self) () in
+let solve ?restarts ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res =
+  let r = Sat_solver.solve ?restarts ~assumptions (solver self) () in
   match r with
   | Sat_solver.Sat (Sidekick_sat.Sat_state st) ->
     Log.debugf 0 (fun k->k "SAT");

src/smt/Solver.mli

@@ -55,6 +55,7 @@ val assume_eq : t -> Term.t -> Term.t -> Lit.t -> unit
 val assume_distinct : t -> Term.t list -> neq:Term.t -> Lit.t -> unit
 
 val solve :
+  ?restarts:bool ->
   ?on_exit:(unit -> unit) list ->
   ?check:bool ->
   assumptions:Lit.t list ->

src/smtlib/Process.ml

@@ -262,7 +262,7 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
 (* call the solver to check-sat *)
 let solve
     ?gc:_
-    ?restarts:_
+    ?restarts
     ?dot_proof
     ?(pp_model=false)
     ?(check=false)
@@ -272,7 +272,7 @@ let solve
     s : unit =
   let t1 = Sys.time() in
   let res =
-    Solver.solve ~assumptions s
+    Solver.solve ?restarts ~assumptions s
     (* ?gc ?restarts ?time ?memory ?progress *)
   in
   let t2 = Sys.time () in