Skip to main content

z3++

Project description

z4

PyPI

z3 with some improvements:

  • BitVec:

    • Change the right shift operation to be logical instead of arithmetic
  • Add the ByteVec class

  • Add some helper methods for solving:

    • easy_solve
    • find_all_solutions
    • easy_prove
  • Add some helper methods for optimizing:

    • maximize
    • minimize
  • Add some helper functions for z3 variables/constants:

    • BoolToInt
    • Sgn
    • TruncDiv

Features implemented upstream

These features were first provided by z4, before z3 included these features. They have now been removed from z4.

Usage

Install with pip install z4-solver.

easy_solve

import z4

a, b = z4.Ints("a b")
print(z4.easy_solve([a <= 10, b <= 10, a + b == 15]))

Output:

[b = 5, a = 10]

find_all_solutions

import z4

a, b = z4.Ints("a b")
print(*z4.find_all_solutions([a <= 10, b <= 10, a + b == 15]), sep="\n")

Output:

[b = 5, a = 10]
[b = 6, a = 9]
[b = 7, a = 8]
[b = 8, a = 7]
[b = 9, a = 6]
[b = 10, a = 5]

easy_prove

Let's try and prove that 2 * a >= a for all integers a:

import z4

a = z4.Int("a")
print(z4.easy_prove(2 * a >= a))

Output

Traceback (most recent call last):
  ...
z4.Z3CounterExample: [a = -1]

This isn't true so we get an exception with the counter-example a = -1. Of course 2 * -1 = -2 which is less than -1.

Let's try again with the assumption that a must be non-negative:

print(z4.easy_prove(z4.Implies(a >= 0, 2 * a >= a)))

Output:

True

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

z4_solver-2024.12.14.1.tar.gz (24.0 kB view details)

Uploaded Source

Built Distribution

z4_solver-2024.12.14.1-py3-none-any.whl (16.4 kB view details)

Uploaded Python 3

File details

Details for the file z4_solver-2024.12.14.1.tar.gz.

File metadata

  • Download URL: z4_solver-2024.12.14.1.tar.gz
  • Upload date:
  • Size: 24.0 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: uv/0.5.9

File hashes

Hashes for z4_solver-2024.12.14.1.tar.gz
Algorithm Hash digest
SHA256 fb7bc4de7309162b02f5ada3e2e872fe2b2adc8931ef732b868f55cb97242d3a
MD5 37fd0194646be468db9fab1d6fc2a4d6
BLAKE2b-256 1fcc13844191feac88cf273175b009cf783728c63c09e283f8860f8c43ab23ba

See more details on using hashes here.

File details

Details for the file z4_solver-2024.12.14.1-py3-none-any.whl.

File metadata

File hashes

Hashes for z4_solver-2024.12.14.1-py3-none-any.whl
Algorithm Hash digest
SHA256 d5ca36cb1709583880ecce6ee73eae9efd6bf30b5a210ddedf188d90769c24f4
MD5 5e42ce07ea072fcc81ecff6ea40c5567
BLAKE2b-256 0186527549af900f7034b0cba141be987f5b1e5096e6399d5c0b490c6892e563

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page