mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-17 11:03:43 -07:00
parent 95c3dd9224
commit b5a89eb4ab
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/mk_api_doc.py
View file

@ -335,6 +335,7 @@ try:
for modulename in ( for modulename in (
'z3', 'z3',
'z3.z3',
'z3.z3consts', 'z3.z3consts',
'z3.z3core', 'z3.z3core',
'z3.z3num', 'z3.z3num',

7
src/api/ml/z3.mli
View file

@ -49,6 +49,13 @@ type context
val mk_context : (string * string) list -> context val mk_context : (string * string) list -> context
(** Interaction logging for Z3 (** 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 Note that this is a global, static log and if multiple Context
objects are created, it logs the interaction with all of them. *) objects are created, it logs the interaction with all of them. *)
module Log : module Log :