blob: 8b1bc9f7e8237d33dfec5934fa577bd62533679b (
plain)
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
(** Maps that store SMT objects **)
(* SMT types *)
let btypes : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 17
let get_btype id =
try Hashtbl.find btypes id
with | Not_found -> failwith ("SmtMaps.get_btype : sort symbol \""^id^"\" not found\n")
let add_btype id cl = Hashtbl.add btypes id cl
let clear_btypes () = Hashtbl.clear btypes
(* SMT function symbols *)
let funs : (string, SmtAtom.indexed_op) Hashtbl.t = Hashtbl.create 17
let get_fun id =
try Hashtbl.find funs id
with | Not_found -> failwith ("SmtMaps.get_fun : function symbol \""^id^"\" not found\n")
let add_fun id cl = Hashtbl.add funs id cl
let remove_fun id = Hashtbl.remove funs id
let clear_funs () = Hashtbl.clear funs
(* Clean-up of all the maps *)
let clear () =
clear_btypes ();
clear_funs ()
|
