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
open Solver_types
let name = "bvar"
type t = bound_var
type term_view += BVar of bound_var
let pp out ((id,_ty) : t) : unit = ID.pp out id
let pp_with_ty out ((id,ty) : t) : unit =
Fmt.fprintf out "(@[%a@ %a@])" ID.pp id Type.pp ty
let k_bvar = Service.Key.make name
let build (p_id:plugin_id) Plugin.S_nil : Plugin.t =
let tc = Term.TC.lazy_make () in
let module P : Plugin.S = struct
let id = p_id
let name = name
module T_alloc = Term.Term_allocator(struct
let tc = tc
let p_id = p_id
let initial_size=256
let[@inline] equal v1 v2 = match v1, v2 with
| BVar (v1,ty1), BVar (v2,ty2) -> ID.equal v1 v2 && Type.equal ty1 ty2
| _ -> assert false
let[@inline] hash = function
| BVar (v,ty) -> CCHash.combine3 125 (ID.hash v) (Type.hash ty)
| _ -> assert false
end)
let gc_all = T_alloc.gc_all
let iter_terms = T_alloc.iter_terms
let pp out = function
| BVar v -> pp out v
| _ -> assert false
let[@inline] bvar ((id,ty):t) : term =
T_alloc.make (BVar (id,ty)) ty
let check_if_sat _ = Sat
let () =
Term.TC.lazy_complete tc ~pp
let provided_services =
[ Service.Any (k_bvar, bvar);
]
end
in
(module P : Plugin.S)
let plugin = Plugin.Factory.make ~priority:10 ~name ~requires:Plugin.K_nil ~build ()