Source file `selector.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
(** Solver, which delegates at runtime to the configured solver. *)

open Batteries
open Goblint_constraint.ConstrSys
open Goblint_constraint.SolverTypes
open GobConfig

(* Registered solvers. *)
let solvers = ref []

(** Register your solvers here!!! *)
let add_solver (x : string * (module DemandEqIncrSolver)) = solvers := x::!solvers

(** Dynamically choose the solver. *)
let choose_solver solver =
  try List.assoc solver !solvers
  with Not_found ->
    raise @@ ConfigError ("Solver '"^solver^"' not found. Abort!")

(** The solver that actually uses the implementation based of [GobConfig.get_string "solver"]. *)
module Make =
  functor (Arg: IncrSolverArg) ->
  functor (S:DemandEqConstrSys) ->
  functor (VH:Hashtbl.S with type key = S.v) ->
  struct
    type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *)

    let copy_marshal (marshal: marshal) =
      let module Sol = (val choose_solver (get_string "solver") : DemandEqIncrSolver) in
      let module F = Sol (Arg) (S) (VH) in
      Obj.repr (F.copy_marshal (Obj.obj marshal))

    let relift_marshal (marshal: marshal) =
      let module Sol = (val choose_solver (get_string "solver") : DemandEqIncrSolver) in
      let module F = Sol (Arg) (S) (VH) in
      Obj.repr (F.relift_marshal (Obj.obj marshal))

    let solve xs vs (old_data: marshal option) =
      let module Sol = (val choose_solver (get_string "solver") : DemandEqIncrSolver) in
      let module F = Sol (Arg) (S) (VH) in
      let (vh, marshal) = F.solve xs vs (Option.map Obj.obj old_data) in
      (vh, Obj.repr marshal)
  end

let _ =
  let module T1 : DemandEqIncrSolver = Make in
  ()