Source file Semantic.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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
open Base
open Sygus
open Parser
open Serializer
open Sexplib
module Command = struct
type t = command
let of_sexp = command_of_sexp
let sexp_of = sexp_of_command
let pp fmt c = Sexp.pp fmt (sexp_of c)
let pp_hum fmt c = Sexp.pp_hum fmt (sexp_of c)
end
module Term = struct
type t = sygus_term
let of_sexp = sygus_term_of_sexp
let sexp_of = sexp_of_sygus_term
let pp fmt c = Sexp.pp fmt (sexp_of c)
let pp_hum fmt c = Sexp.pp_hum fmt (sexp_of c)
end
module Ident = struct
type t = identifier
let of_sexp = identifier_of_sexp
let sexp_of = sexp_of_identifier
let pp fmt c = Sexp.pp fmt (sexp_of c)
let pp_hum fmt c = Sexp.pp_hum fmt (sexp_of c)
end
module Lit = struct
type t = literal
let of_sexp = literal_of_sexp
let sexp_of = sexp_of_literal
let pp fmt c = Sexp.pp fmt (sexp_of c)
let pp_hum fmt c = Sexp.pp_hum fmt (sexp_of c)
end
module Sort = struct
type t = sygus_sort
let of_sexp = sygus_sort_of_sexp
let sexp_of = sexp_of_sygus_sort
let pp fmt c = Sexp.pp fmt (sexp_of c)
let pp_hum fmt c = Sexp.pp_hum fmt (sexp_of c)
end
let is_setter_command (c : Command.t) =
match c with
| CSetFeature _ | CSetInfo _ | CSetLogic _ | CSetOption _ -> true
| _ -> false
;;
let is_well_formed (p : program) : bool =
let setter_then_other l =
let _, b =
List.fold l ~init:(false, true) ~f:(fun (b0, b1) c ->
let b = is_setter_command c in
b0 && b, b1 && ((not b) || (b && b0)))
in
b
in
match p with
| [] -> true
| hd :: tl ->
(match hd with
| CSetLogic _ -> setter_then_other tl
| _ -> setter_then_other p)
;;
let declares (c : command) : symbol list =
match c with
| CCheckSynth
| CInvConstraint _
| CSetFeature _
| CSetInfo _
| CSetOption _
| CSetLogic _
| CAssume _
| COptimizeSynth _
| CChcConstraint _
| CConstraint _ -> []
| COracle (ODeclareFun (s, _, _, _)) -> [ s ]
| COracle _ -> []
| CDeclareVar (s, _)
| CSynthFun (s, _, _, _)
| CSynthInv (s, _, _)
| CDeclareSort (s, _)
| CDefineFun (s, _, _, _)
| CDefineSort (s, _) -> [ s ]
| CDeclareWeight (s, _) -> [ s ]
| CDeclareDataType (s, constrs) -> s :: List.map ~f:fst constrs
| CDeclareDataTypes (sl, cd) ->
List.map ~f:fst sl @ List.concat_map ~f:(List.map ~f:fst) cd
;;
let compare_declares (c1 : command) (c2 : command) =
List.compare String.compare (declares c1) (declares c2)
;;
let max_definition =
Command.of_sexp
(Sexp.of_string "(define-fun max ((x Int) (y Int)) Int (ite (>= x y) x y))")
;;
let min_definition =
Command.of_sexp
(Sexp.of_string "(define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))")
;;
let rec rename (subs : (symbol * symbol) list) (t : sygus_term) : sygus_term =
match t with
| SyId (IdSimple s) ->
(match List.Assoc.find ~equal:String.equal subs s with
| Some s' -> SyId (IdSimple s')
| None -> t)
| SyApp (IdSimple f, args) ->
let args' = List.map ~f:(rename subs) args in
(match List.Assoc.find ~equal:String.equal subs f with
| Some f' -> SyApp (IdSimple f', args')
| None -> SyApp (IdSimple f, args'))
| SyApp (f, args) -> SyApp (f, List.map ~f:(rename subs) args)
| SyExists (vars, body) ->
let subs' =
List.filter ~f:(fun (l, _) -> List.Assoc.mem ~equal:String.equal vars l) subs
in
SyExists (vars, rename subs' body)
| SyForall (vars, body) ->
let subs' =
List.filter ~f:(fun (l, _) -> List.Assoc.mem ~equal:String.equal vars l) subs
in
SyForall (vars, rename subs' body)
| SyLit _ | SyId _ -> t
| SyLet (bindings, body) ->
let bindings' =
List.map ~f:(fun (varname, body) -> varname, rename subs body) bindings
in
let subs' =
List.filter ~f:(fun (l, _) -> List.Assoc.mem ~equal:String.equal bindings l) subs
in
let body' = rename subs' body in
SyLet (bindings', body')
;;
let write_command (out : Stdio.Out_channel.t) (c : command) : unit =
let comm_s = Fmt.(to_to_string Command.pp c) in
Stdio.Out_channel.(
output_lines out [ comm_s ];
flush out)
;;