diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-25 18:33:28 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-25 18:33:28 +0200 |
| commit | 20e37ecc9acf75ece81948c6dfd7420130621a12 (patch) | |
| tree | 5c2638aac02f5f47d7a13bb3f96a368df08e8a6e | |
| parent | d35b057995b4940af0e66bb081b3fe3ac7ff97f3 (diff) | |
| download | smtcoq-20e37ecc9acf75ece81948c6dfd7420130621a12.tar.gz smtcoq-20e37ecc9acf75ece81948c6dfd7420130621a12.zip | |
Missing files
| -rw-r--r-- | src/trace/smtMaps.ml | 35 | ||||
| -rw-r--r-- | src/trace/smtMaps.mli | 25 |
2 files changed, 60 insertions, 0 deletions
diff --git a/src/trace/smtMaps.ml b/src/trace/smtMaps.ml new file mode 100644 index 0000000..86239fb --- /dev/null +++ b/src/trace/smtMaps.ml @@ -0,0 +1,35 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* 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 () diff --git a/src/trace/smtMaps.mli b/src/trace/smtMaps.mli new file mode 100644 index 0000000..7808854 --- /dev/null +++ b/src/trace/smtMaps.mli @@ -0,0 +1,25 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* 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 *) +val get_btype : string -> SmtBtype.btype +val add_btype : string -> SmtBtype.btype -> unit + +(* SMT function symbols *) +val get_fun : string -> SmtAtom.indexed_op +val add_fun : string -> SmtAtom.indexed_op -> unit +val remove_fun : string -> unit + +(* Clean-up of all the maps *) +val clear : unit -> unit |