Source file interpret_intf.ml

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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

(** {1 Execution State and Interpreter Interface} *)

(** Represents the execution state of the interpreter *)
type 'a state =
  { stmts : Ast.Script.t  (** The script being executed *)
  ; smap : (string, Ty.t) Hashtbl.t  (** A mapping of variable names to types *)
  ; solver : 'a  (** The underlying solver instance *)
  ; expected_status : [ `Sat | `Unsat | `Unknown ] option
      (** The status of the execution*)
  }

(** {2 Interpreter Interface} *)
module type S = sig
  (** The type representing a solver *)
  type solver

  (** The type representing the execution state of interpreter *)
  type exec_state

  (** Initializes execution with an optional state *)
  val start :
    ?state:exec_state -> Ast.Script.t -> no_strict_status:bool -> exec_state
end

(** {2 Interpreter functor interface} *)
module type Intf = sig
  (** Functor for creating a solver execution module *)
  module Make (Solver : Solver_intf.S) :
    S with type solver = Solver.t and type exec_state = Solver.t state
end