z3/examples/python at c154b9df9090c8c49e806db74c13d925b8f45e52 - mirrors/z3

mirrors/z3

mirror of https://github.com/Z3Prover/z3 synced 2025-11-08 23:35:07 +00:00

Bruce Mitchener 53f89a81c1 Fix some typos. (#7115 )		2024-02-07 23:06:43 -08:00
..
bounded model checking	three smt2 examples added and one python example updated (#5690 )	2021-12-01 16:21:12 -08:00
complex
data
hamiltonian
mus	marco: immediately shrink to core if not subset (#5203 )	2021-04-20 12:29:52 -07:00
tutorial	use structured proof hints	2022-05-28 09:37:41 -07:00
all_interval_series.py
bincover.py	Add branch and bound solver, for fun	2023-12-23 11:58:29 -08:00
CMakeLists.txt	Ensure that the 'OUTPUT' locations in CMake for Python examples is accurate (#4499 )	2020-06-04 15:04:01 -07:00
efsmt.py	handle return status	2022-04-04 20:19:15 +02:00
example.py
hs.py	updated experiment	2021-03-26 14:58:23 -07:00
mini_ic3.py	updated mini	2022-01-26 15:44:49 -08:00
mini_quip.py	Implement mini_quip	2019-01-04 18:30:02 -05:00
parallel.py
prooflogs.py	add example for monitoring proof logs	2022-10-19 13:37:51 -07:00
proofreplay.py	Fix some typos. (#7115 )	2024-02-07 23:06:43 -08:00
rc2.py
README
simplify_formula.py	formula simplification example	2022-08-11 09:33:36 +03:00
socrates.py
trafficjam.py
union_sort.py
visitor.py	add example for #5933	2022-04-05 04:26:40 +02:00

README

The example is copied to the build directory during configuration.
You can execute it using
    python example.py
in the build directory after you build Z3.