Source file `satsolverregistry.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
module String_for_set =
struct
  type t = string
  let compare = compare
end ;;
module StringMap = Map.Make(String_for_set) ;;

let solvermap = ref StringMap.empty;;

let default = ref None;;

let register_solver solver_factory =
	let identifier = solver_factory#identifier in
	if StringMap.mem identifier !solvermap
	then failwith ("Solver `" ^ identifier ^ "' already registered!\n")
	else (
		solvermap := StringMap.add identifier solver_factory !solvermap;
		default := Some solver_factory
	);;

let mem_solver identifier = StringMap.mem identifier !solvermap;;

let find_solver identifier = StringMap.find identifier !solvermap;;

let enum_solvers it = StringMap.iter (fun _ f -> it f) !solvermap;;

let fold_solvers fo b = StringMap.fold (fun _ f x -> fo f x) !solvermap b;;

let get_list _ = fold_solvers (fun s l -> s::l) []

let get_default _ =
	match !default with
		Some f -> f
	|	None -> failwith "no sat solvers registered!"

let set_default identifier =
	default := Some (find_solver identifier)