Source file `interpret.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
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
(***************************************************************************)
(* 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 Interpret_intf

module Make (Solver : Solver_intf.S) = struct
  open Ast

  type solver = Solver.t

  type exec_state = solver state

  let init_state stmts =
    let params = Params.(default () $ (Model, false)) in
    let solver = Solver.create ~params () in
    Solver.push solver;
    { stmts; smap = Hashtbl.create 16; solver; pc = [] }

  let eval stmt (state : exec_state) : exec_state =
    let { solver; pc; _ } = state in
    let st pc = { state with pc } in
    match stmt with
    | Assert e ->
      Solver.add solver [ e ];
      st (e :: pc)
    | Check_sat ->
      ( match Solver.check solver [] with
      | `Sat -> Format.printf "sat@."
      | `Unsat -> Format.printf "unsat@."
      | `Unknown -> Format.printf "unknown@." );
      st pc
    | Push ->
      Solver.push solver;
      st pc
    | Pop n ->
      Solver.pop solver n;
      st pc
    | Let_const _x -> st pc
    | Get_model ->
      assert (`Sat = Solver.check solver []);
      let model = Solver.model solver in
      Format.printf "%a@."
        (Format.pp_print_option (Model.pp ~no_values:false))
        model;
      st pc
    | Set_logic logic ->
      let solver = Solver.create ~logic () in
      Solver.push solver;
      { state with solver }

  let rec loop (state : exec_state) : exec_state =
    match state.stmts with
    | [] -> state
    | stmt :: stmts -> loop (eval stmt { state with stmts })

  let start ?state (stmts : Ast.script) : exec_state =
    let st =
      match state with
      | None -> init_state stmts
      | Some st ->
        Solver.pop st.solver 1;
        Solver.push st.solver;
        { st with stmts; pc = [] }
    in
    loop st
end