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 /src/trace/smtMaps.mli | |
| parent | d35b057995b4940af0e66bb081b3fe3ac7ff97f3 (diff) | |
| download | smtcoq-20e37ecc9acf75ece81948c6dfd7420130621a12.tar.gz smtcoq-20e37ecc9acf75ece81948c6dfd7420130621a12.zip | |
Missing files
Diffstat (limited to 'src/trace/smtMaps.mli')
| -rw-r--r-- | src/trace/smtMaps.mli | 25 |
1 files changed, 25 insertions, 0 deletions
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 |