formalsec / smtml / 290

Committed 28 Feb 2025 09:44AM UTC coverage: 47.592% (-0.07%) from 47.662%

Build # 290

Build Type

push

github

Committed by

filipeom

Commit Message

Update CHANGES.md

Run Details

1591 of 3343 relevant lines covered (47.59%)

32.48 hits per line

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

48.0

/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
  module Make (Mappings : Mappings.S) = struct
    include Base (Mappings)

    type solver = Mappings.solver

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

    module Cache = Cache.Strong

    let cache = Cache.create 256

    let cache_hits () = Cache.hits cache

    let cache_misses () = Cache.misses cache

    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

  module Fresh () = Make (Mappings_)
  include Make (Mappings_)
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 ()	34✔
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	16✔
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;	61✔
43	Utils.run_and_time_call	61✔
44	~use:(fun time -> solver_time := !solver_time +. time)	61✔
45	(fun () -> M.Solver.check solver ~assumptions:es)	61✔
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 () }	22✔
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;	31✔
84	Stack.push top stack	31✔
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	113✔
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)	47✔
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	module Make (Mappings : Mappings.S) = struct
125	include Base (Mappings)
126
127	type solver = Mappings.solver
128
129	type t =
130	{ solver : solver
131	; mutable top : Expr.Set.t
132	; stack : Expr.Set.t Stack.t
133	}
134
135	module Cache = Cache.Strong
136
137	let cache = Cache.create 256	1✔
138
139	let cache_hits () = Cache.hits cache	2✔
140
141	let cache_misses () = Cache.misses cache	1✔
142
143	let pp_statistics fmt s = pp_statistics fmt s.solver	×
144
145	let create ?params ?logic () =
146	{ solver = create ?params ?logic ()	1✔
147	; top = Expr.Set.empty
148	; stack = Stack.create ()	1✔
149	}
150
151	let clone ({ solver; top; stack } : t) : t =
152	{ solver = clone solver; top; stack = Stack.copy stack }	×
153
154	let push ({ top; stack; solver } : t) : unit =
155	Mappings.Solver.push solver;	×
156	Stack.push top stack	×
157
158	let rec pop (s : t) (lvl : int) : unit =
159	assert (lvl <= Stack.length s.stack);	×
160	if lvl <= 0 then ()	×
161	else begin	×
162	Mappings.Solver.pop s.solver 1;
163	match Stack.pop_opt s.stack with	×
164	\| None -> assert false
165	\| Some v ->	×
166	s.top <- v;
167	pop s (lvl - 1)
168	end
169
170	let reset (s : t) =
171	Mappings.Solver.reset s.solver;	×
172	Stack.clear s.stack;	×
173	s.top <- Expr.Set.empty	×
174
175	let add (s : t) (es : Expr.t list) : unit =
176	s.top <- Expr.Set.(union (of_list es) s.top)	×
177
178	let add_set s es = s.top <- Expr.Set.union es s.top	×
179
180	let get_assertions (s : t) : Expr.t list = Expr.Set.to_list s.top [@@inline]	×
181
182	let get_statistics (s : t) : Statistics.t = get_statistics s.solver	×
183
184	let check_set s es =
185	let assert_ = Expr.Set.union es s.top in	3✔
186	match Cache.find_opt cache assert_ with	3✔
187	\| Some res -> res	2✔
188	\| None ->	1✔
189	let result = check_set s.solver assert_ in
190	Cache.add cache es result;	1✔
191	result	1✔
192
193	let check (s : t) (es : Expr.t list) = check_set s (Expr.Set.of_list es)	×
194
195	let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e	×
196
197	let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
198	model ?symbols s.solver	×
199
200	let interrupt { solver; _ } = interrupt solver	×
201	end
202
203	module Fresh () = Make (Mappings_)
204	include Make (Mappings_)
205	end

formalsec / smtml / 290

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