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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)
type t =
| Assert of Expr.t
| Check_sat of Expr.t list
| Declare_const of
{ id : Symbol.t
; sort : Symbol.t
}
| Echo of string
| Exit
| Get_assertions
| Get_assignment
| Get_info of string
| Get_option of string
| Get_model
| Get_value of Expr.t list
| Pop of int
| Push of int
| Reset
| Reset_assertions
| Set_info of Expr.t
| Set_logic of Ty.logic
| Set_option of Expr.t
type script = t list
let pp fmt (instr : t) =
match instr with
| Assert e -> Fmt.pf fmt "@[<hov 1>(assert@ %a@])" Expr.pp e
| Check_sat [] -> Fmt.string fmt "(check-sat)"
| Check_sat assumptuions ->
Fmt.pf fmt "(check-sat-assuming@ (%a))"
(Fmt.list ~sep:Fmt.sp Expr.pp)
assumptuions
| Declare_const { id; sort } ->
Fmt.pf fmt "(declare-const %a %a)" Symbol.pp id Symbol.pp sort
| Echo line -> Fmt.pf fmt "(echo %S)" line
| Exit -> Fmt.string fmt "(exit)"
| Get_assertions -> Fmt.string fmt "(get-assertions)"
| Get_assignment -> Fmt.string fmt "(get-assignment)"
| Get_info info -> Fmt.pf fmt "(get-info %a)" Fmt.string info
| Get_option opt -> Fmt.pf fmt "(get-option %a)" Fmt.string opt
| Get_model -> Fmt.string fmt "(get-model)"
| Get_value htes ->
Fmt.pf fmt "(get-value %a)" (Fmt.parens (Fmt.list ~sep:Fmt.sp Expr.pp)) htes
| Pop n -> Fmt.pf fmt "(pop %d)" n
| Push n -> Fmt.pf fmt "(push %d)" n
| Reset -> Fmt.string fmt "(reset)"
| Reset_assertions -> Fmt.string fmt "(reset-assertions)"
| Set_info info -> Fmt.pf fmt "(set-info %a)" Expr.pp info
| Set_logic logic -> Fmt.pf fmt "(set-logic %a)" Ty.pp_logic logic
| Set_option opt -> Fmt.pf fmt "(set-option %a)" Expr.pp opt
let to_string (instr : t) : string = Fmt.str "%a" pp instr