z3/examples/python at master - z3 - ProxGit

ada/z3

mirror of https://github.com/AdaCore/z3.git synced 2026-02-12 12:40:40 -08:00

Files

History

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

fix #2365

2019-06-30 08:40:41 +03:00

Add few more testcases

2018-12-28 13:28:15 -05:00

Fix typos in examples.

2019-08-14 22:00:50 -07:00

marco: immediately shrink to core if not subset (#5203 )

2021-04-20 12:29:52 -07:00

use structured proof hints

2022-05-28 09:37:41 -07:00

all_interval_series.py

travis timeouts

2021-02-21 13:13:19 +00:00

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

PYTHON_PATH should say PYTHONPATH.

2019-01-18 16:18:16 -08:00

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

Add comments

2018-05-19 11:16:20 +02:00

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

fix #5080 assertion is violated on legal input, add an example

2021-03-05 15:01:39 -08:00

README

python example

2012-10-28 12:19:45 -07:00

simplify_formula.py

formula simplification example

2022-08-11 09:33:36 +03:00

socrates.py

Fix typos in examples.

2019-08-14 22:00:50 -07:00

trafficjam.py

fix traffic jam

2019-06-10 17:45:55 -07:00

union_sort.py

fix justification for implied equalities in special relations

2019-04-03 17:08:10 -07:00

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.