From b5a89eb4abd2ca62a37958ba5f394cfe47b0a1da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Jul 2022 11:03:43 -0700 Subject: [PATCH] add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration --- doc/mk_api_doc.py | 1 + src/api/ml/z3.mli | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 7ca47b89a92..670634e0720 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -335,6 +335,7 @@ def doc_path(path): for modulename in ( 'z3', + 'z3.z3', 'z3.z3consts', 'z3.z3core', 'z3.z3num', diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index a7c62901805..b7fa27b5ecd 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -49,6 +49,13 @@ type context val mk_context : (string * string) list -> context (** Interaction logging for Z3 + Interaction logs are used to record calls into the API into a text file. + The text file can be replayed using z3. It has to be the same version of z3 + to ensure that low level codes emitted in a log are compatible with the + version of z3 replaying the log. The file suffix ".log" is understood + by z3 as the format of the file being an interaction log. You can use the + optional comman-line parameter "-log" to force z3 to treat an input file + as an interaction log. Note that this is a global, static log and if multiple Context objects are created, it logs the interaction with all of them. *) module Log :