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
module Tptp = struct
let symbol m ~attr ~loc id =
let t = match id with
| { Id.name = Simple "$_"; ns = Term } -> Term.(builtin ~loc Wildcard ())
| { Id.name = Simple "$tType" ; ns = Term } -> Term.(builtin ~loc Ttype ())
| { Id.name = Simple "$o"; ns = Term } -> Term.(builtin ~loc Prop ())
| { Id.name = Simple "$true"; ns = Term } -> Term.(builtin ~loc True ())
| { Id.name = Simple "$false"; ns = Term } -> Term.(builtin ~loc False ())
| { Id.name = Simple "$int"; ns = Term } -> Term.(builtin ~loc Int ())
| { Id.name = Simple "$less"; ns = Term } -> Term.(builtin ~loc Lt ())
| { Id.name = Simple "$lesseq"; ns = Term } -> Term.(builtin ~loc Leq ())
| { Id.name = Simple "$greater"; ns = Term } -> Term.(builtin ~loc Gt ())
| { Id.name = Simple "$greatereq"; ns = Term } -> Term.(builtin ~loc Geq ())
| { Id.name = Simple "$uminus"; ns = Term } -> Term.(builtin ~loc Minus ())
| { Id.name = Simple "$sum"; ns = Term } -> Term.(builtin ~loc Add ())
| { Id.name = Simple "$difference"; ns = Term } -> Term.(builtin ~loc Sub ())
| { Id.name = Simple "$product"; ns = 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 = Simple "Bool"; ns = Sort } -> Term.(builtin ~loc Prop ())
| { Id.name = Simple "true"; ns = Term } -> Term.(builtin ~loc True ())
| { Id.name = Simple "false"; ns = Term } -> Term.(builtin ~loc False ())
| { Id.name = Simple "not"; ns = Term } -> Term.(builtin ~loc Not ())
| { Id.name = Simple "and"; ns = Term } -> Term.(builtin ~loc And ())
| { Id.name = Simple "or"; ns = Term } -> Term.(builtin ~loc Or ())
| { Id.name = Simple "xor"; ns = Term } -> Term.(builtin ~loc Xor ())
| { Id.name = Simple "=>"; ns = Term } -> Term.(builtin ~loc Imply ())
| { Id.name = Simple "="; ns = Term } -> Term.(builtin ~loc Eq ())
| { Id.name = Simple "distinct"; ns = Term } -> Term.(builtin ~loc Distinct ())
| { Id.name = Simple "ite"; ns = 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_seq ->
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.Let_par ->
let attrs = List.map (Term.map m) attr in
let l' = List.map (binder_let_eq m) l in
Term.add_attrs attrs (Term.letand ~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