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
module Tptp = struct
let symbol m ~attr ~loc id =
let t = match id with
| { Id.name = "$_"; ns = Id.Term } -> Term.(builtin ?loc Wildcard ())
| { Id.name = "$tType" ; ns = Id.Term } -> Term.(builtin ?loc Ttype ())
| { Id.name = "$o"; ns = Id.Term } -> Term.(builtin ?loc Prop ())
| { Id.name = "$true"; ns = Id.Term } -> Term.(builtin ?loc True ())
| { Id.name = "$false"; ns = Id.Term } -> Term.(builtin ?loc False ())
| { Id.name = "$int"; ns = Id.Term } -> Term.(builtin ?loc Int ())
| { Id.name = "$less"; ns = Id.Term } -> Term.(builtin ?loc Lt ())
| { Id.name = "$lesseq"; ns = Id.Term } -> Term.(builtin ?loc Leq ())
| { Id.name = "$greater"; ns = Id.Term } -> Term.(builtin ?loc Gt ())
| { Id.name = "$greatereq"; ns = Id.Term } -> Term.(builtin ?loc Geq ())
| { Id.name = "$uminus"; ns = Id.Term } -> Term.(builtin ?loc Minus ())
| { Id.name = "$sum"; ns = Id.Term } -> Term.(builtin ?loc Add ())
| { Id.name = "$difference"; ns = Id.Term } -> Term.(builtin ?loc Sub ())
| { Id.name = "$product"; ns = Id.Term } -> Term.(builtin ?loc Mult ())
| _ -> Term.(const ?loc id)
in
let attrs = List.map (Term.map m) attr in
Term.add_attrs attrs t
let mapper =
{ Term.id_mapper with symbol }
end
module Smtlib = struct
let symbol m ~attr ~loc id =
let t = match id with
| { Id.name = "Bool"; ns = Id.Sort } -> Term.(builtin ?loc Prop ())
| { Id.name = "true"; ns = Id.Term } -> Term.(builtin ?loc True ())
| { Id.name = "false"; ns = Id.Term } -> Term.(builtin ?loc False ())
| { Id.name = "not"; ns = Id.Term } -> Term.(builtin ?loc Not ())
| { Id.name = "and"; ns = Id.Term } -> Term.(builtin ?loc And ())
| { Id.name = "or"; ns = Id.Term } -> Term.(builtin ?loc Or ())
| { Id.name = "xor"; ns = Id.Term } -> Term.(builtin ?loc Xor ())
| { Id.name = "=>"; ns = Id.Term } -> Term.(builtin ?loc Imply ())
| { Id.name = "="; ns = Id.Term } -> Term.(builtin ?loc Eq ())
| { Id.name = "distinct"; ns = Id.Term } -> Term.(builtin ?loc Distinct ())
| { Id.name = "ite"; ns = Id.Term } -> Term.(builtin ?loc Ite ())
| _ -> Term.(const ?loc id)
in
let attrs = List.map (Term.map m) attr in
Term.add_attrs attrs t
let binder_let_eq m t =
match t with
| { Term.term = Term.Colon (u, v) ; _ } ->
Term.eq ?loc:t.Term.loc (Term.map m u) (Term.map m v)
| _ -> assert false
let binder m ~attr ~loc b l body =
match b with
| Term.Let ->
let attrs = List.map (Term.map m) attr in
let l' = List.map (binder_let_eq m) l in
Term.add_attrs attrs (Term.letin ?loc l' (Term.map m body))
| _ -> Term.(id_mapper.binder m ~attr ~loc b l body)
let mapper =
{ Term.id_mapper with symbol; binder }
end