diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 26990849e2..9b1fc9e066 100644 --- a/src/bin/common/solving_loop.ml +++ b/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,17 +143,17 @@ 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 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 @@ -316,11 +317,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 +342,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,11 +481,8 @@ 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 |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -506,7 +498,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 +507,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 +523,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 +613,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 +821,7 @@ let main () = in let partial_model = solve - (snd @@ State.get sat_solver_key st) + (snd @@ DO.SatSolver.get st) all_context (cnf, name) in @@ -888,8 +875,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 +897,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 diff --git a/src/lib/dune b/src/lib/dune index ef5d8311ab..2599188186 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml new file mode 100644 index 0000000000..626ab7f00e --- /dev/null +++ b/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 Input = sig + type k + + type t + + val get : unit -> k + + val key : string + + val on_update : k -> unit + + val map : k -> t +end + +module type S = sig + type k + + type t + + val set : k -> Typer.state -> Typer.state + + val get : Typer.state -> t + + val reset : Typer.state -> Typer.state +end + +module Make(O:Input) : S with type k = O.k and type t = O.t = struct + type k = O.k + type t = O.t + + let key = State.create_key ~pipe:"" O.key + + let set opt st = + let st = State.set key (O.map opt) st in + O.on_update opt; + st + + let get st = + try State.get key st with + | State.Key_not_found _ -> O.map (O.get ()) + + let reset = set (O.get ()) +end + +let create_opt + (type k) + (type t) + ?(on_update=ignore) + key + (get : unit -> k) + (map : (k -> t)) = + (module ( + Make ( + struct + type nonrec k = k + type nonrec t = t + let key = key + let get = get + let on_update = on_update + let map = map + end) + ) : S with type k = k and type t = t) + +module ProduceAssignment = + (val (create_opt "produce_assignment" (fun _ -> false)) Fun.id) + +module Optimize = + (val (create_opt "optimize" O.get_optimize) Fun.id) + +let msatsolver = + let map s = + let module SatCont = + (val (Sat_solver.get s) : 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 + s, + (module SatCont.Make(TH) : Sat_solver_sig.S) + in + (create_opt "sat_solver" O.get_sat_solver map) + +module SatSolver = (val msatsolver) diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli new file mode 100644 index 0000000000..9cbcd2af74 --- /dev/null +++ b/src/lib/frontend/d_state_option.mli @@ -0,0 +1,52 @@ +(**************************************************************************) +(* *) +(* 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 type S = sig + (** The type of options. It should match the type in the module Options. *) + type k + + (** The data saved in the state. May differ from the saved option. *) + type t + + (** Sets the option on the dolmen state, with a transformation from k to t. *) + val set : k -> D_loop.Typer.state -> D_loop.Typer.state + + (** 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 + + (** Resets the option to its default value in Options. *) + val reset : D_loop.Typer.state -> D_loop.Typer.state +end + +module ProduceAssignment : S with type k = bool and type t = bool +module Optimize : S with type k = bool and type t = bool +module SatSolver : S with type k = Util.sat_solver + and type t = Util.sat_solver * (module Sat_solver_sig.S) diff --git a/src/lib/reasoners/sat_solver.ml b/src/lib/reasoners/sat_solver.ml index 856dd67145..ce12d75b4e 100644 --- a/src/lib/reasoners/sat_solver.ml +++ b/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) diff --git a/src/lib/reasoners/sat_solver.mli b/src/lib/reasoners/sat_solver.mli index 5bd86e5819..316ac4383a 100644 --- a/src/lib/reasoners/sat_solver.mli +++ b/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)