Adding a generic option manager for the dolmen state

src/bin/common/solving_loop.ml

@@ -31,6 +31,7 @@
 open AltErgoLib
 open D_loop
 
+module DO = D_state_option
 module O = Options
 
 type solver_ctx = {
@@ -142,18 +143,6 @@ type model = Model : 'a sat_module * 'a -> model
 let main () =
   let () = Dolmen_loop.Code.init [] in
 
-  let make_sat () =
-    let module SatCont =
-      (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) in
-
-    let module TH =
-      (val
-        (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S)
-         else (module Theory.Main_Default : Theory.S)) : Theory.S ) in
-    O.get_sat_solver (),
-    (module SatCont.Make(TH) : Sat_solver_sig.S)
-  in
-
   let solve (module SAT : Sat_solver_sig.S) all_context (cnf, goal_name) =
     let module FE = Frontend.Make (SAT) in
     if Options.get_debug_commands () then
@@ -316,11 +305,17 @@ let main () =
         | Exit -> exit 0
       end
     in
-
+    let sat_solver =
+      let module SatCont =
+        (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer)
+      in
+      let module TH = (val Sat_solver.get_theory ~no_th:(O.get_no_theory ())) in
+      (module SatCont.Make(TH) : Sat_solver_sig.S)
+    in
     let state = {
       env = I.empty_env;
       solver_ctx = empty_solver_ctx;
-      sat_solver = snd @@ make_sat ();
+      sat_solver;
     } in
     try
       let parsed_seq = parsed () in
@@ -335,22 +330,10 @@ let main () =
     State.create_key ~pipe:"" "solving_state"
   in
 
-  let sat_solver_key : (Util.sat_solver * (module Sat_solver_sig.S)) State.key =
-    State.create_key ~pipe:"" "sat_solver"
-  in
-
   let partial_model_key: model option State.key =
     State.create_key ~pipe:"" "sat_state"
   in
 
-  let optimize_key: bool State.key =
-    State.create_key ~pipe:"" "optimize"
-  in
-
-  let produce_assignment: bool State.key =
-    State.create_key ~pipe:"" "produce_assignment"
-  in
-
   let named_terms: DStd.Expr.term Util.MS.t State.key =
     State.create_key ~pipe:"" "named_terms"
   in
@@ -486,12 +469,10 @@ let main () =
     let response_file = State.mk_file dir (`Raw ("", "")) in
     logic_file,
     State.empty
-    |> State.set sat_solver_key (make_sat ())
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
-    |> State.set optimize_key (O.get_optimize ())
-    |> State.set produce_assignment false
     |> State.set named_terms Util.MS.empty
+    |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
     |> Parser.init
@@ -506,7 +487,7 @@ let main () =
   in
 
   let set_sat_solver sat st =
-    let optim = State.get optimize_key st in
+    let optim = DO.Optimize.get st in
     match sat with
     | Util.Tableaux | Tableaux_CDCL when optim ->
       warning
@@ -515,17 +496,13 @@ let main () =
         sat;
       st
     | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
-      O.set_sat_solver sat;
       (* `make_sat` returns the sat solver corresponding to the new sat_solver
          option. *)
-      State.set
-        sat_solver_key
-        (make_sat ())
-        st
+      DO.SatSolver.set sat st
   in
 
   let set_optimize optim st =
-    let sat, _ = State.get sat_solver_key st in
+    let sat = DO.SatSolver.get st in
     match sat with
     | Util.Tableaux | Tableaux_CDCL when optim ->
       warning
@@ -535,7 +512,7 @@ let main () =
       st
     | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
       enable_maxsmt optim;
-      State.set optimize_key optim st
+      DO.Optimize.set optim st
   in
 
   let handle_option st_loc name (value : DStd.Term.t) st =
@@ -625,8 +602,7 @@ let main () =
         | None ->
           print_wrn_opt ~name:":verbosity" st_loc "boolean" value;
           st
-        | Some b ->
-          State.set produce_assignment b st
+        | Some b -> DO.ProduceAssignment.set b st
       end
     | (":global-declarations"
       | ":interactive-mode"
@@ -834,7 +810,7 @@ let main () =
         in
         let partial_model =
           solve
-            (snd @@ State.get sat_solver_key st)
+            (DO.SatSolverModule.get st)
             all_context
             (cnf, name)
         in
@@ -888,8 +864,8 @@ let main () =
         st
         |> State.set partial_model_key None
         |> State.set solver_ctx_key empty_solver_ctx
-        |> State.set optimize_key (O.get_optimize ())
-        |> State.set produce_assignment false
+        |> DO.Optimize.reset
+        |> DO.ProduceAssignment.reset
         |> State.set named_terms Util.MS.empty
 
       | {contents = `Exit; _} -> raise Exit
@@ -910,7 +886,7 @@ let main () =
         begin
           match State.get partial_model_key st with
           | Some Model ((module SAT), partial_model) ->
-            if State.get produce_assignment st then
+            if DO.ProduceAssignment.get st then
               handle_get_assignment
                 ~get_value:(SAT.get_value partial_model)
                 st

src/lib/dune

@@ -35,7 +35,8 @@
   ; modules that make up the lib
   (modules
     ; frontend
-    Cnf D_cnf D_loop Input Frontend Parsed_interface Typechecker Models
+    Cnf D_cnf D_loop D_state_option Input Frontend Parsed_interface Typechecker
+    Models
     ; reasoners
     Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel
     Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel

src/lib/frontend/d_state_option.ml

@@ -0,0 +1,117 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     The Alt-Ergo theorem prover                                        *)
+(*                                                                        *)
+(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
+(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*     Until 2013, some parts of this code were released under            *)
+(*     the Apache Software License version 2.0.                           *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module O = Options
+module State = D_loop.State
+module Typer = D_loop.Typer
+
+module type Accessor = sig
+  (** The data saved in the state. *)
+  type t
+
+  (** Returns the option stored in the state. If it has not been registered,
+      fetches the default option in the module Options. *)
+  val get : D_loop.Typer.state -> t
+end
+
+module type S = sig
+  include Accessor
+
+  (** Sets the option on the dolmen state. *)
+  val set : t -> D_loop.Typer.state -> D_loop.Typer.state
+
+  (** Resets the option to its default value in Options. *)
+  val reset : D_loop.Typer.state -> D_loop.Typer.state
+end
+
+let create_opt
+    (type t)
+    ?(on_update=(fun _ _ -> Fun.id))
+    (key : string)
+    (get : unit -> t) : (module S with type t = t) =
+  (module struct
+    type nonrec t = t
+
+    let key = State.create_key ~pipe:"" key
+
+    let set opt st =
+      st
+      |> on_update key opt
+      |> State.set key opt
+
+    let reset = set (get ())
+
+    let get st =
+      try State.get key st with
+      | State.Key_not_found _ -> get ()
+  end)
+
+module ProduceAssignment =
+  (val (create_opt "produce_assignment" (fun _ -> false)))
+
+module Optimize =
+  (val (create_opt "optimize" O.get_optimize))
+
+let get_sat_solver
+    ?(sat = O.get_sat_solver ())
+    ?(no_th = O.get_no_theory ())
+    () =
+  let module SatCont =
+    (val (Sat_solver.get sat) : Sat_solver_sig.SatContainer) in
+  let module TH =
+    (val
+      (if no_th then
+         (module Theory.Main_Empty : Theory.S)
+       else
+         (module Theory.Main_Default : Theory.S)) : Theory.S )
+  in
+  (module SatCont.Make(TH) : Sat_solver_sig.S)
+
+module SatSolverModule =
+  (val (create_opt "sat_solver_module" (fun _ -> get_sat_solver ())))
+
+let msatsolver =
+  let on_update _ sat st =
+    SatSolverModule.set (get_sat_solver ~sat ()) st
+  in
+  (create_opt ~on_update "sat_solver" O.get_sat_solver)
+
+module SatSolver = (val msatsolver)
+
+(* Some options can be initialized to gain some performance. *)
+let options_requiring_initialization = [
+  (module SatSolverModule : S);
+]
+
+let init st =
+  List.fold_left
+    (fun st (module S : S) -> S.reset st)
+    st
+    options_requiring_initialization

src/lib/frontend/d_state_option.mli

@@ -0,0 +1,68 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     The Alt-Ergo theorem prover                                        *)
+(*                                                                        *)
+(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
+(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*     Until 2013, some parts of this code were released under            *)
+(*     the Apache Software License version 2.0.                           *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** The Dolmen state option manager. Each module defined below is linked to
+    an option that can be set, fetched et reset independently from the
+    Options module, which is used as a static reference. *)
+
+module type Accessor = sig
+  (** The data saved in the state. *)
+  type t
+
+  (** Returns the option stored in the state. If it has not been registered,
+      fetches the default option in the module Options. *)
+  val get : D_loop.Typer.state -> t
+end
+
+module type S = sig
+  include Accessor
+
+  (** Sets the option on the dolmen state. *)
+  val set : t -> D_loop.Typer.state -> D_loop.Typer.state
+
+  (** Resets the option to its default value in Options. *)
+  val reset : D_loop.Typer.state -> D_loop.Typer.state
+end
+
+(** Option for enabling/disabling the get-assignment instruction. *)
+module ProduceAssignment : S with type t = bool
+
+(** Option for enabling/disabling the optimization engine. *)
+module Optimize : S with type t = bool
+
+(** The Sat solver used. When set, updates the SatSolverModule defined below. *)
+module SatSolver : S with type t = Util.sat_solver
+
+(** The Sat solver module used for the calculation. This option's value depends
+    on SatSolver: when SatSolver is updated, this one also is. *)
+module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)
+
+(** Initializes the state with options that requires some preprocessing. *)
+val init : D_loop.Typer.state -> D_loop.Typer.state

src/lib/reasoners/sat_solver.ml

@@ -28,8 +28,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let get_current () =
-  match Options.get_sat_solver () with
+let get = function
   | Util.Tableaux | Util.Tableaux_CDCL ->
     if Options.get_verbose () then
       Printer.print_dbg
@@ -42,3 +41,12 @@ let get_current () =
         ~module_name:"Sat_solver"
         "use CDCL solver";
     (module Satml_frontend : Sat_solver_sig.SatContainer)
+
+
+let get_current () = get (Options.get_sat_solver ())
+
+let get_theory ~no_th =
+  if no_th then
+    (module Theory.Main_Empty : Theory.S)
+  else
+    (module Theory.Main_Default : Theory.S)

src/lib/reasoners/sat_solver.mli

@@ -28,7 +28,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val get : Util.sat_solver -> (module Sat_solver_sig.SatContainer)
+(** Returns the SAT-solver corresponding to the argument. *)
+
 val get_current : unit -> (module Sat_solver_sig.SatContainer)
 (** returns the current activated SAT-solver depending on the value of
     `Options.sat_solver ()`. See command-line option `-sat-solver` for
     more details **)
+
+val get_theory : no_th:bool -> (module Theory.S)