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
type t =
| Assert of Expr.t
| Check_sat of Expr.t list
| Declare_const of
{ id : Symbol.t
; sort : Symbol.t
}
| Declare_fun of
{ id : Symbol.t
; args : Symbol.t list
; 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 Logic.t
| Set_option of Expr.t
let pp fmt (instr : t) =
match instr with
| Assert e -> Fmt.pf fmt "@[<hov 1>(assert@ %a@])" Expr.Smtlib.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.Smtlib.pp)
assumptuions
| Declare_const { id; sort } ->
Fmt.pf fmt "(declare-const %a %a)" Symbol.Smtlib.pp id Symbol.Smtlib.pp sort
| Declare_fun { id; args; sort } ->
Fmt.pf fmt "(declare-fun %a (%a) %a)" Symbol.Smtlib.pp id
(Fmt.list ~sep:Fmt.sp Symbol.Smtlib.pp)
args Symbol.Smtlib.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.Smtlib.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.Smtlib.pp info
| Set_logic logic -> Fmt.pf fmt "(set-logic %a)" Logic.pp logic
| Set_option opt -> Fmt.pf fmt "(set-option %a)" Expr.Smtlib.pp opt
let to_string (instr : t) : string = Fmt.str "%a" pp instr
module Script = struct
type nonrec t = t list
let const (id : Symbol.t) =
let sort = Symbol.make3 id.ty id.name Symbol.sort in
Declare_const { id; sort }
let assert_ e = Assert e
let of_exprs (exprs : Expr.t list) : t =
let syms = Expr.get_symbols exprs in
List.map const syms @ List.map assert_ exprs @ [ Check_sat [] ]
let pp = Fmt.list pp
end