Skip to content

Commit

Permalink
add missing generation of z3.z3 for pydoc and add some explanations t…
Browse files Browse the repository at this point in the history
…o logging function declaration
  • Loading branch information
NikolajBjorner committed Jul 17, 2022
1 parent 95c3dd9 commit b5a89eb
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 0 deletions.
1 change: 1 addition & 0 deletions doc/mk_api_doc.py
Original file line number Diff line number Diff line change
Expand Up @@ -335,6 +335,7 @@ def doc_path(path):

for modulename in (
'z3',
'z3.z3',
'z3.z3consts',
'z3.z3core',
'z3.z3num',
Expand Down
7 changes: 7 additions & 0 deletions src/api/ml/z3.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down

0 comments on commit b5a89eb

Please sign in to comment.