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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)
(** Optimizer Module. This module defines interfaces for interacting with
optimization solvers, including constraint management, optimization
objectives, and result retrieval. It provides a generic interface for
working with different optimization backends. *)
(** {1 Module Types} *)
(** The [S] module type defines the core interface for interacting with
optimization solvers. *)
module type S = sig
(** The type of optimization solvers. *)
type t
(** [create ()] creates a new optimization solver. *)
val create : unit -> t
(** [push solver] pushes a new context level onto the solver [solver]. *)
val push : t -> unit
(** [pop solver] pops a context level from the solver [solver]. *)
val pop : t -> unit
(** [add solver exprs] adds the expressions [exprs] to the solver [solver]. *)
val add : t -> Expr.t list -> unit
(** [protect solver f] executes the function [f] within a protected context,
ensuring that the solver state is restored after execution. *)
val protect : t -> (unit -> 'a) -> 'a
(** [check solver] checks the satisfiability of the solver [solver]. Returns
[`Sat], [`Unsat], or [`Unknown]. *)
val check : t -> [ `Sat | `Unsat | `Unknown ]
(** [model solver] retrieves the model from the solver [solver], if one
exists. *)
val model : t -> Model.t option
(** [maximize solver expr] maximizes the expression [expr] in the solver
[solver]. Returns the optimal value if found. *)
val maximize : t -> Expr.t -> Value.t option
(** [minimize solver expr] minimizes the expression [expr] in the solver
[solver]. Returns the optimal value if found. *)
val minimize : t -> Expr.t -> Value.t option
(** [get_statistics solver] retrieves statistics from the solver [solver]. *)
val get_statistics : t -> Statistics.t
end
(** The [Intf] module type defines the interface for creating and working with
optimization solvers, including a functor for instantiating solvers and a
predefined Z3 solver implementation. *)
module type Intf = sig
(** The [S] module type, which defines the core optimizer interface. *)
module type S = S
(** [Make] is a functor that creates an optimizer instance from a given
mappings module. *)
module Make (_ : Mappings_intf.S) : S
(** [Z3] is a predefined optimizer implementation using the Z3 solver. *)
module Z3 : S
end