This script generates CSV/SVG/PNG/MIDI files to explore the quantifier instantiations of a Z3 trace, (hopefully) helping to identify matching loops. See below for an example.
- The CSV file lists the quantifier and generation of each instantiation, in the same order as they appear in the Z3 trace.
- The SVG and PNG images visualize the order in which the quantifiers are matched and instantiated. Each quantifier is associated with a column and time progresses downwords. Each match is a green square and each instantiation is a red square, whose color intensity represents the generation of the instantiation.
- The MIDI file represents just the quantifier instantiations. Each quantifier is associated with a pitch and each instantiation generates a note whose volume increases with the generation of the instantiation.
Python 3.6 or later.
Optionally, to generate the SVG/PNG/MIDI files:
pip install --user svgwrite==1.4.2 cairosvg==2.5.2 midiutil==1.2.1
usage: python script.py [-h] [-i INPUT] [--csv CSV] [--svg SVG] [--png PNG] [--midi MIDI]
[--max-instantiations MAX_INSTANTIATIONS]
[--skip-instantiations SKIP_INSTANTIATIONS] [--tempo TEMPO]
Explore quantifier instantiations.
optional arguments:
-h, --help show this help message and exit
-i INPUT, --input INPUT
path of the Z3 trace (default: read from stdin)
--csv CSV output path of the CSV file
--svg SVG output path of the SVG file
--png PNG output path of the PNG file
--midi MIDI output path of the MIDI file
--max-instantiations MAX_INSTANTIATIONS
maximum number of quantifier instantiations to load (default: all)
--skip-instantiations SKIP_INSTANTIATIONS
number of *loaded* quantifier instantiations to skip (default: 0)
--tempo TEMPO beats per minute (default: 480)
Command:
python script.py \
--input z3.log \
--max-instantiations 5500 \
--skip-instantiations 5000 \
--csv example/example.csv \
--svg example/example.svg \
--midi example/example.midOutput:
Loading trace file 'z3.log'...
Tool version: Z3 4.8.6
Only the first 5500 quantifier instantiations will be loaded.
Number of quantifiers: 222
Number of used quantifiers: 42
Number of unique matches: 1274
Number of quantifier instantiations: 5500
Creating CSV file at 'example/example.csv'...
CSV file created
Creating SVG image...
The first 5000 quantifier instantiations will be ignored.
SVG image created
Creating SVG file at 'example/example.svg'...
SVG file created
Creating MIDI file at 'example/example.mid'...
MIDI file created
Generated files: example.csv, example.svg, example.mid
Explanation of the generated image:
To generate a z3.log file:
z3 trace=true smt.qi.profile=true smt.qi.profile_freq=10000 program.smt2The smt.qi.profile=true smt.qi.profile_freq=10000 arguments make Z3 periodically report the number of quantifier instantiations, which is usefuly if you want to check the progress or kill Z3 when too many quantifiers have been instantiated.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent
