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

46.58

/src/solver.ml

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

include Solver_intf

let ( let+ ) o f = Option.map f o

module Base (M : Mappings_intf.S) = struct
  type t = M.solver

  type solver = t

  let solver_time = ref 0.0

  let solver_count = ref 0

  let pp_statistics _fmt _solver = ()

  let create ?params ?logic () : t = M.Solver.make ?params ?logic ()

  let interrupt solver = M.Solver.interrupt solver

  let clone (solver : t) : t = M.Solver.clone solver

  let push (solver : t) : unit = M.Solver.push solver

  let pop (solver : t) (lvl : int) : unit = M.Solver.pop solver lvl

  let reset (solver : t) : unit = M.Solver.reset solver

  let add (solver : t) (es : Expr.t list) : unit = M.Solver.add solver es

  let add_set s es = add s @@ Expr.Set.to_list es

  let get_assertions (_solver : t) : Expr.t list = assert false

  let get_statistics (solver : t) : Statistics.t =
    M.Solver.get_statistics solver

  let check (solver : M.solver) (es : Expr.t list) =
    incr solver_count;
    Utils.run_and_time_call
      ~use:(fun time -> solver_time := !solver_time +. time)
      (fun () -> M.Solver.check solver ~assumptions:es)

  let check_set solver es = check solver @@ Expr.Set.to_list es

  let get_value (solver : M.solver) (e : Expr.t) : Expr.t =
    match M.Solver.model solver with
    | Some m -> Expr.value @@ M.value m e
    | None ->
      Fmt.failwith "get_value: Trying to get a value from an unsat solver"

  let model ?(symbols : Symbol.t list option) (s : M.solver) : Model.t option =
    let+ model = M.Solver.model s in
    M.values_of_model ?symbols model
end

module Incremental (M : Mappings_intf.S) : Solver_intf.S =
  Base [@inlined hint] (M)

module Batch (Mappings : Mappings.S) = struct
  include Base (Mappings)

  type solver = Mappings.solver

  type t =
    { solver : solver
    ; mutable top : Expr.t list
    ; stack : Expr.t list Stack.t
    }

  let pp_statistics fmt s = pp_statistics fmt s.solver

  let create ?params ?logic () =
    { solver = create ?params ?logic (); top = []; stack = Stack.create () }

  let clone ({ solver; top; stack } : t) : t =
    { solver = clone solver; top; stack = Stack.copy stack }

  let push ({ top; stack; solver } : t) : unit =
    Mappings.Solver.push solver;
    Stack.push top stack

  let rec pop (s : t) (lvl : int) : unit =
    assert (lvl <= Stack.length s.stack);
    if lvl <= 0 then ()
    else begin
      Mappings.Solver.pop s.solver 1;
      match Stack.pop_opt s.stack with
      | None -> assert false
      | Some v ->
        s.top <- v;
        pop s (lvl - 1)
    end

  let reset (s : t) =
    Mappings.Solver.reset s.solver;
    Stack.clear s.stack;
    s.top <- []

  let add (s : t) (es : Expr.t list) : unit = s.top <- es @ s.top

  let add_set s es = s.top <- Expr.Set.to_list es @ s.top

  let get_assertions (s : t) : Expr.t list = s.top [@@inline]

  let get_statistics (s : t) : Statistics.t = get_statistics s.solver

  let check (s : t) (es : Expr.t list) = check s.solver (es @ s.top)

  let check_set s es = check s @@ Expr.Set.to_list es

  let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e

  let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
    model ?symbols s.solver

  let interrupt { solver; _ } = interrupt solver
end

module Cached (Mappings : Mappings.S) = struct
  include Base (Mappings)
  module Cache = Cache.Strong

  let cache = Cache.create 256

  type solver = Mappings.solver

  type t =
    { solver : solver
    ; mutable top : Expr.Set.t
    ; stack : Expr.Set.t Stack.t
    }

  let pp_statistics fmt s = pp_statistics fmt s.solver

  let create ?params ?logic () =
    { solver = create ?params ?logic ()
    ; top = Expr.Set.empty
    ; stack = Stack.create ()
    }

  let clone ({ solver; top; stack } : t) : t =
    { solver = clone solver; top; stack = Stack.copy stack }

  let push ({ top; stack; solver } : t) : unit =
    Mappings.Solver.push solver;
    Stack.push top stack

  let rec pop (s : t) (lvl : int) : unit =
    assert (lvl <= Stack.length s.stack);
    if lvl <= 0 then ()
    else begin
      Mappings.Solver.pop s.solver 1;
      match Stack.pop_opt s.stack with
      | None -> assert false
      | Some v ->
        s.top <- v;
        pop s (lvl - 1)
    end

  let reset (s : t) =
    Mappings.Solver.reset s.solver;
    Stack.clear s.stack;
    s.top <- Expr.Set.empty

  let add (s : t) (es : Expr.t list) : unit =
    s.top <- Expr.Set.(union (of_list es) s.top)

  let add_set s es = s.top <- Expr.Set.union es s.top

  let get_assertions (s : t) : Expr.t list = Expr.Set.to_list s.top [@@inline]

  let get_statistics (s : t) : Statistics.t = get_statistics s.solver

  let check_set s es =
    let assert_ = Expr.Set.union es s.top in
    match Cache.find_opt cache assert_ with
    | Some res -> res
    | None ->
      let result = check_set s.solver assert_ in
      Cache.add cache es result;
      result

  let check (s : t) (es : Expr.t list) = check_set s (Expr.Set.of_list es)

  let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e

  let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
    model ?symbols s.solver

  let interrupt { solver; _ } = interrupt solver
end

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	include Solver_intf
6
7	let ( let+ ) o f = Option.map f o	15✔
8
9	module Base (M : Mappings_intf.S) = struct
10	type t = M.solver
11
12	type solver = t
13
14	let solver_time = ref 0.0
15
16	let solver_count = ref 0
17
18	let pp_statistics _fmt _solver = ()	×
19
20	let create ?params ?logic () : t = M.Solver.make ?params ?logic ()	30✔
21
22	let interrupt solver = M.Solver.interrupt solver	×
23
24	let clone (solver : t) : t = M.Solver.clone solver	×
25
26	let push (solver : t) : unit = M.Solver.push solver	3✔
27
28	let pop (solver : t) (lvl : int) : unit = M.Solver.pop solver lvl	3✔
29
30	let reset (solver : t) : unit = M.Solver.reset solver	×
31
32	let add (solver : t) (es : Expr.t list) : unit = M.Solver.add solver es	12✔
33
34	let add_set s es = add s @@ Expr.Set.to_list es	×
35
36	let get_assertions (_solver : t) : Expr.t list = assert false	×
37
38	let get_statistics (solver : t) : Statistics.t =
39	M.Solver.get_statistics solver	×
40
41	let check (solver : M.solver) (es : Expr.t list) =
42	incr solver_count;	57✔
43	Utils.run_and_time_call	57✔
44	~use:(fun time -> solver_time := !solver_time +. time)	57✔
45	(fun () -> M.Solver.check solver ~assumptions:es)	57✔
46
47	let check_set solver es = check solver @@ Expr.Set.to_list es	1✔
48
49	let get_value (solver : M.solver) (e : Expr.t) : Expr.t =
50	match M.Solver.model solver with	6✔
51	\| Some m -> Expr.value @@ M.value m e	6✔
52	\| None ->	×
53	Fmt.failwith "get_value: Trying to get a value from an unsat solver"
54
55	let model ?(symbols : Symbol.t list option) (s : M.solver) : Model.t option =
56	let+ model = M.Solver.model s in	15✔
57	M.values_of_model ?symbols model	15✔
58	end
59
60	module Incremental (M : Mappings_intf.S) : Solver_intf.S =
61	Base [@inlined hint] (M)
62
63	module Batch (Mappings : Mappings.S) = struct
64	include Base (Mappings)
65
66	type solver = Mappings.solver
67
68	type t =
69	{ solver : solver
70	; mutable top : Expr.t list
71	; stack : Expr.t list Stack.t
72	}
73
74	let pp_statistics fmt s = pp_statistics fmt s.solver	×
75
76	let create ?params ?logic () =
77	{ solver = create ?params ?logic (); top = []; stack = Stack.create () }	20✔
78
79	let clone ({ solver; top; stack } : t) : t =
80	{ solver = clone solver; top; stack = Stack.copy stack }	×
81
82	let push ({ top; stack; solver } : t) : unit =
83	Mappings.Solver.push solver;	29✔
84	Stack.push top stack	29✔
85
86	let rec pop (s : t) (lvl : int) : unit =
87	assert (lvl <= Stack.length s.stack);	22✔
88	if lvl <= 0 then ()	11✔
89	else begin	11✔
90	Mappings.Solver.pop s.solver 1;
91	match Stack.pop_opt s.stack with	11✔
92	\| None -> assert false
93	\| Some v ->	11✔
94	s.top <- v;
95	pop s (lvl - 1)
96	end
97
98	let reset (s : t) =
99	Mappings.Solver.reset s.solver;	×
100	Stack.clear s.stack;	×
101	s.top <- []	×
102
103	let add (s : t) (es : Expr.t list) : unit = s.top <- es @ s.top	111✔
104
105	let add_set s es = s.top <- Expr.Set.to_list es @ s.top	×
106
107	let get_assertions (s : t) : Expr.t list = s.top [@@inline]	×
108
109	let get_statistics (s : t) : Statistics.t = get_statistics s.solver	×
110
111	let check (s : t) (es : Expr.t list) = check s.solver (es @ s.top)	45✔
112
113	let check_set s es = check s @@ Expr.Set.to_list es	×
114
115	let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e	×
116
117	let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
118	model ?symbols s.solver	12✔
119
120	let interrupt { solver; _ } = interrupt solver	×
121	end
122
123	module Cached (Mappings : Mappings.S) = struct
124	include Base (Mappings)
125	module Cache = Cache.Strong
126
127	let cache = Cache.create 256	1✔
128
129	type solver = Mappings.solver
130
131	type t =
132	{ solver : solver
133	; mutable top : Expr.Set.t
134	; stack : Expr.Set.t Stack.t
135	}
136
137	let pp_statistics fmt s = pp_statistics fmt s.solver	×
138
139	let create ?params ?logic () =
140	{ solver = create ?params ?logic ()	1✔
141	; top = Expr.Set.empty
142	; stack = Stack.create ()	1✔
143	}
144
145	let clone ({ solver; top; stack } : t) : t =
146	{ solver = clone solver; top; stack = Stack.copy stack }	×
147
148	let push ({ top; stack; solver } : t) : unit =
149	Mappings.Solver.push solver;	×
150	Stack.push top stack	×
151
152	let rec pop (s : t) (lvl : int) : unit =
153	assert (lvl <= Stack.length s.stack);	×
154	if lvl <= 0 then ()	×
155	else begin	×
156	Mappings.Solver.pop s.solver 1;
157	match Stack.pop_opt s.stack with	×
158	\| None -> assert false
159	\| Some v ->	×
160	s.top <- v;
161	pop s (lvl - 1)
162	end
163
164	let reset (s : t) =
165	Mappings.Solver.reset s.solver;	×
166	Stack.clear s.stack;	×
167	s.top <- Expr.Set.empty	×
168
169	let add (s : t) (es : Expr.t list) : unit =
170	s.top <- Expr.Set.(union (of_list es) s.top)	×
171
172	let add_set s es = s.top <- Expr.Set.union es s.top	×
173
174	let get_assertions (s : t) : Expr.t list = Expr.Set.to_list s.top [@@inline]	×
175
176	let get_statistics (s : t) : Statistics.t = get_statistics s.solver	×
177
178	let check_set s es =
179	let assert_ = Expr.Set.union es s.top in	3✔
180	match Cache.find_opt cache assert_ with	3✔
181	\| Some res -> res	2✔
182	\| None ->	1✔
183	let result = check_set s.solver assert_ in
184	Cache.add cache es result;	1✔
185	result	1✔
186
187	let check (s : t) (es : Expr.t list) = check_set s (Expr.Set.of_list es)	×
188
189	let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e	×
190
191	let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
192	model ?symbols s.solver	×
193
194	let interrupt { solver; _ } = interrupt solver	×
195	end

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