formalsec / smtml / 274

Committed 05 Feb 2025 01:53PM UTC coverage: 47.698% (+0.2%) from 47.539%

Build # 274

Build Type

push

github

Committed by

filipeom

Commit Message

fix doc

Run Details

1544 of 3237 relevant lines covered (47.7%)

32.65 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

75.0

/src/params.ml

(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

type _ param =
  | Timeout : int param
  | Model : bool param
  | Unsat_core : bool param
  | Ematching : bool param
  | Parallel : bool param
  | Num_threads : int param

let discr : type a. a param -> int = function
  | Timeout -> 0
  | Model -> 1
  | Unsat_core -> 2
  | Ematching -> 3
  | Parallel -> 4
  | Num_threads -> 5

module Key = struct
  type t = K : 'a param -> t

  let v v = K v

  let compare (K a) (K b) = compare (discr a) (discr b)
end

module Pmap = Map.Make (Key)

type param' = P : 'a param * 'a -> param'

let p k v = P (k, v)

type t = param' Pmap.t

let default_timeout = 2147483647

let default_model = true

let default_unsat_core = false

let default_ematching = true

let default_parallel = false

let default_num_threads = 1

let default_value (type a) (param : a param) : a =
  match param with
  | Timeout -> default_timeout
  | Model -> default_model
  | Unsat_core -> default_unsat_core
  | Ematching -> default_ematching
  | Parallel -> default_parallel
  | Num_threads -> default_num_threads

let default () =
  Pmap.empty
  |> Pmap.add (Key.v Timeout) (p Timeout default_timeout)
  |> Pmap.add (Key.v Model) (p Model default_model)
  |> Pmap.add (Key.v Unsat_core) (p Unsat_core default_unsat_core)
  |> Pmap.add (Key.v Ematching) (p Ematching default_ematching)

let set (type a) (params : t) (param : a param) (value : a) : t =
  Pmap.add (Key.v param) (p param value) params

let opt (type a) (params : t) (param : a param) (opt_value : a option) : t =
  Option.fold ~none:params ~some:(set params param) opt_value

let ( $ ) (type a) (params : t) ((param, value) : a param * a) : t =
  set params param value

let get (type a) (params : t) (param : a param) : a =
  match (param, Pmap.find_opt (Key.v param) params) with
  | _, None -> assert false
  | Timeout, Some (P (Timeout, v)) -> v
  | Model, Some (P (Model, v)) -> v
  | Unsat_core, Some (P (Unsat_core, v)) -> v
  | Ematching, Some (P (Ematching, v)) -> v
  | Parallel, Some (P (Parallel, v)) -> v
  | Num_threads, Some (P (Num_threads, v)) -> v
  | (Timeout | Model | Unsat_core | Ematching | Parallel | Num_threads), _ ->
    assert false

let to_list params = List.map snd @@ Pmap.bindings params

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	type _ param =
6	\| Timeout : int param
7	\| Model : bool param
8	\| Unsat_core : bool param
9	\| Ematching : bool param
10	\| Parallel : bool param
11	\| Num_threads : int param
12
13	let discr : type a. a param -> int = function
14	\| Timeout -> 0	69✔
15	\| Model -> 1	114✔
16	\| Unsat_core -> 2	76✔
17	\| Ematching -> 3	73✔
18	\| Parallel -> 4	4✔
19	\| Num_threads -> 5	4✔
20
21	module Key = struct
22	type t = K : 'a param -> t
23
24	let v v = K v	115✔
25
26	let compare (K a) (K b) = compare (discr a) (discr b)	170✔
27	end
28
29	module Pmap = Map.Make (Key)
30
31	type param' = P : 'a param * 'a -> param'
32
33	let p k v = P (k, v)	114✔
34
35	type t = param' Pmap.t
36
37	let default_timeout = 2147483647
38
39	let default_model = true
40
41	let default_unsat_core = false
42
43	let default_ematching = true
44
45	let default_parallel = false
46
47	let default_num_threads = 1
48
49	let default_value (type a) (param : a param) : a =
50	match param with	4✔
51	\| Timeout -> default_timeout	1✔
52	\| Model -> default_model	1✔
53	\| Unsat_core -> default_unsat_core	1✔
54	\| Ematching -> default_ematching	1✔
55	\| Parallel -> default_parallel	×
56	\| Num_threads -> default_num_threads	×
57
58	let default () =
59	Pmap.empty	22✔
60	\|> Pmap.add (Key.v Timeout) (p Timeout default_timeout)	22✔
61	\|> Pmap.add (Key.v Model) (p Model default_model)	22✔
62	\|> Pmap.add (Key.v Unsat_core) (p Unsat_core default_unsat_core)	22✔
63	\|> Pmap.add (Key.v Ematching) (p Ematching default_ematching)	22✔
64
65	let set (type a) (params : t) (param : a param) (value : a) : t =
66	Pmap.add (Key.v param) (p param value) params	26✔
67
68	let opt (type a) (params : t) (param : a param) (opt_value : a option) : t =
69	Option.fold ~none:params ~some:(set params param) opt_value	×
70
71	let ( $ ) (type a) (params : t) ((param, value) : a param * a) : t =
72	set params param value	26✔
73
74	let get (type a) (params : t) (param : a param) : a =
75	match (param, Pmap.find_opt (Key.v param) params) with	1✔
76	\| _, None -> assert false
77	\| Timeout, Some (P (Timeout, v)) -> v	×
78	\| Model, Some (P (Model, v)) -> v	×
79	\| Unsat_core, Some (P (Unsat_core, v)) -> v	1✔
80	\| Ematching, Some (P (Ematching, v)) -> v	×
81	\| Parallel, Some (P (Parallel, v)) -> v	×
82	\| Num_threads, Some (P (Num_threads, v)) -> v	×
83	\| (Timeout \| Model \| Unsat_core \| Ematching \| Parallel \| Num_threads), _ ->
84	assert false
85
86	let to_list params = List.map snd @@ Pmap.bindings params	22✔

formalsec / smtml / 274

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous