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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
(***************************************************************************)
(* This file is part of the third-party OCaml library `smtml`. *)
(* Copyright (C) 2023-2024 formalsec *)
(* *)
(* This program is free software: you can redistribute it and/or modify *)
(* it under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with this program. If not, see <https://www.gnu.org/licenses/>. *)
(***************************************************************************)
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 = M.Solver.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 get_assertions (_solver : t) : Expr.t list = assert false
let check (solver : M.solver) (es : Expr.t list) : satisfiability =
solver_count := !solver_count + 1;
Utils.run_and_time_call
~use:(fun time -> solver_time := !solver_time +. time)
(fun () -> M.Solver.check solver ~assumptions:es)
let get_value (solver : M.solver) (e : Expr.t) : Expr.t =
match M.Solver.model solver with
| Some m -> Expr.make @@ Val (M.value m e)
| None -> Log.err "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 Make_batch (Mappings : Mappings_intf.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 = Mappings.Solver.make ?params ?logic ()
; top = []
; stack = Stack.create ()
}
let clone ({ solver; top; stack } : t) : t =
{ 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;
s.top <- Stack.pop s.stack;
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 get_assertions (s : t) : Expr.t list = s.top [@@inline]
let check (s : t) (es : Expr.t list) : satisfiability =
check s.solver (es @ s.top)
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
(* TODO: Our base solver can be incrmental itself? *)
module Batch (M : Mappings_intf.S) : Solver_intf.S = Make_batch (M)
module Cached (M : Mappings_intf.S) : sig
include Solver_intf.S
module Cache : Cache_intf.S
end = struct
include Make_batch (M)
module Cache = Cache.Strong
let cache = Cache.create 256
let check s es =
match Cache.find_opt cache es with
| Some res -> res
| None ->
let result = check s es in
Cache.add cache es result;
result
end
module Incremental (M : Mappings_intf.S) : Solver_intf.S = Base (M)
module Z3_batch : Solver_intf.S = Batch (Z3_mappings)
module Z3_incremental : Solver_intf.S = Incremental (Z3_mappings)