Skip to content

Commit

Permalink
Adding a generic option manager for the dolmen state
Browse files Browse the repository at this point in the history
  • Loading branch information
@Stevendeo
Stevendeo committed Nov 17, 2023
1 parent 2a9a770 commit 761eb1a
Show file tree
Hide file tree
Showing 6 changed files with 208 additions and 46 deletions.
61 changes: 18 additions & 43 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
open AltErgoLib
open D_loop

module DO = D_state_option
module O = Options

type solver_ctx = {
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -486,11 +469,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
Expand All @@ -506,7 +486,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
Expand All @@ -515,17 +495,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
Expand All @@ -535,7 +511,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 =
Expand Down Expand Up @@ -625,8 +601,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"
Expand Down Expand Up @@ -834,7 +809,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
Expand Down Expand Up @@ -888,8 +863,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
Expand All @@ -910,7 +885,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
Expand Down
3 changes: 2 additions & 1 deletion src/lib/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
117 changes: 117 additions & 0 deletions src/lib/frontend/d_state_option.ml
View file
Original file line number Diff line number Diff line change
@@ -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)
56 changes: 56 additions & 0 deletions src/lib/frontend/d_state_option.mli
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
(**************************************************************************)
(* *)
(* 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 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)
12 changes: 10 additions & 2 deletions src/lib/reasoners/sat_solver.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
5 changes: 5 additions & 0 deletions src/lib/reasoners/sat_solver.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

0 comments on commit 761eb1a

Please sign in to comment.