Metadata-Version: 2.1
Name: z4-solver
Version: 2021.12.25.0
Summary: z3++
Home-page: https://github.com/Tyilo/z4
License: GPL-3.0-only
Author: Asger Hautop Drewsen
Author-email: asgerdrewsen@gmail.com
Requires-Python: >=3.7,<4.0
Classifier: License :: OSI Approved :: GNU General Public License v3 (GPLv3)
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Requires-Dist: z3-solver (>=4.8,<5.0)
Project-URL: Repository, https://github.com/Tyilo/z4
Description-Content-Type: text/markdown

z4
============

[z3](https://github.com/Z3Prover/z3) with some improvements:
* Change the right shift operation on `BitVec`'s to be logical instead of arithmetic
* Add the `ByteVec` class
* Some helper methods for solving:
  * `easy_solve`
  * `find_all_solutions`
  * `easy_prove`
* Add some helper functions for z3 variables/constants:
  * `BoolToInt`
  * `Sgn`
  * `Abs`
  * `TruncDiv`

