Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.
For documentation, please read http://z3prover.github.io/api/html/z3.html
Raw data
{
"_id": null,
"home_page": "https://github.com/Z3Prover/z3",
"name": "z3-solver",
"maintainer": "Audrey Dutcher and Nikolaj Bjorner",
"docs_url": null,
"requires_python": null,
"maintainer_email": "audrey@rhelmot.io",
"keywords": "z3, smt, sat, prover, theorem",
"author": "The Z3 Theorem Prover Project",
"author_email": null,
"download_url": "https://files.pythonhosted.org/packages/a3/60/9a924ee28cd1d12f2482834581d9024bf05110aa1098c056e847f05f7f76/z3_solver-4.15.3.0.tar.gz",
"platform": null,
"description": "Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n",
"bugtrack_url": null,
"license": "MIT License",
"summary": "an efficient SMT solver library",
"version": "4.15.3.0",
"project_urls": {
"Homepage": "https://github.com/Z3Prover/z3"
},
"split_keywords": [
"z3",
" smt",
" sat",
" prover",
" theorem"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "6345dd8e9d7500faa05eafa589cc8f0f0b982ce575d51b455d62dab8e19dd571",
"md5": "cc5b512e156fe19033948cc9293e8efa",
"sha256": "65335aab295ded7c0ce27c85556067087a87052389ff160777d1a1d48ef0d74f"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-macosx_13_0_arm64.whl",
"has_sig": false,
"md5_digest": "cc5b512e156fe19033948cc9293e8efa",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 36882388,
"upload_time": "2025-08-16T02:27:18",
"upload_time_iso_8601": "2025-08-16T02:27:18.721724Z",
"url": "https://files.pythonhosted.org/packages/63/45/dd8e9d7500faa05eafa589cc8f0f0b982ce575d51b455d62dab8e19dd571/z3_solver-4.15.3.0-py3-none-macosx_13_0_arm64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "549ea11186061d9fead8be43bad7c75055585694124b2ccdd896ef249fe5824f",
"md5": "ff882e1c7bccf1ffe84ba1ed7186bcbe",
"sha256": "3e62e93adff2def3537ff1ca67c3d58a6ca6d1944e0b5e774f88627b199d50e7"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-macosx_13_0_x86_64.whl",
"has_sig": false,
"md5_digest": "ff882e1c7bccf1ffe84ba1ed7186bcbe",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 39637842,
"upload_time": "2025-08-16T02:27:22",
"upload_time_iso_8601": "2025-08-16T02:27:22.177109Z",
"url": "https://files.pythonhosted.org/packages/54/9e/a11186061d9fead8be43bad7c75055585694124b2ccdd896ef249fe5824f/z3_solver-4.15.3.0-py3-none-macosx_13_0_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "b90bf15168475e5493ea44fa3c5e642903f05d2b870db71ad05662ed87a06976",
"md5": "02da330a348988578f53320e0aea9899",
"sha256": "a9afd9ceb290482097474d43f08415bcc1874f433189d1449f6c1508e9c68384"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"has_sig": false,
"md5_digest": "02da330a348988578f53320e0aea9899",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 29056003,
"upload_time": "2025-08-16T02:27:27",
"upload_time_iso_8601": "2025-08-16T02:27:27.951940Z",
"url": "https://files.pythonhosted.org/packages/b9/0b/f15168475e5493ea44fa3c5e642903f05d2b870db71ad05662ed87a06976/z3_solver-4.15.3.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "a70432a97b1f04175ec56213168ee3659709e876e3feacacb891ed3c26c1a82c",
"md5": "75fa708f8d1007637117df2dbe3d27a6",
"sha256": "f61ef44552489077eedd7e6d9bed52ef1875decf86d66027742099a2703b1c77"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-manylinux_2_34_aarch64.whl",
"has_sig": false,
"md5_digest": "75fa708f8d1007637117df2dbe3d27a6",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 27074143,
"upload_time": "2025-08-16T02:27:30",
"upload_time_iso_8601": "2025-08-16T02:27:30.755026Z",
"url": "https://files.pythonhosted.org/packages/a7/04/32a97b1f04175ec56213168ee3659709e876e3feacacb891ed3c26c1a82c/z3_solver-4.15.3.0-py3-none-manylinux_2_34_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "7577da54076a584557ea34f20800c68f725fe61f1dd987493fcb410b4a26f99f",
"md5": "4562774514196a355edd8956a0c296e4",
"sha256": "0c603f6bad7423d6411adda6af55030b725e3d30f54ea91b714abcedd73b848a"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-win32.whl",
"has_sig": false,
"md5_digest": "4562774514196a355edd8956a0c296e4",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 13123666,
"upload_time": "2025-08-16T02:27:33",
"upload_time_iso_8601": "2025-08-16T02:27:33.309333Z",
"url": "https://files.pythonhosted.org/packages/75/77/da54076a584557ea34f20800c68f725fe61f1dd987493fcb410b4a26f99f/z3_solver-4.15.3.0-py3-none-win32.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "c159abc1bad8b25e9c576484ba65ca5ed225c8ed24d601ec242712f1c370b693",
"md5": "841781e9aad20ad82bdcb0ee7d40219d",
"sha256": "06abdf6c36f97c463aea827533504fd59476d015a65cf170a88bd6a53ba13ab5"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0-py3-none-win_amd64.whl",
"has_sig": false,
"md5_digest": "841781e9aad20ad82bdcb0ee7d40219d",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 16203065,
"upload_time": "2025-08-16T02:27:35",
"upload_time_iso_8601": "2025-08-16T02:27:35.763310Z",
"url": "https://files.pythonhosted.org/packages/c1/59/abc1bad8b25e9c576484ba65ca5ed225c8ed24d601ec242712f1c370b693/z3_solver-4.15.3.0-py3-none-win_amd64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "a3609a924ee28cd1d12f2482834581d9024bf05110aa1098c056e847f05f7f76",
"md5": "db64b34e16645fbfea8f71cd57779974",
"sha256": "78f69aebda5519bfd8af146a129f36cf4721a3c2667e80d9fe35cc9bb4d214a6"
},
"downloads": -1,
"filename": "z3_solver-4.15.3.0.tar.gz",
"has_sig": false,
"md5_digest": "db64b34e16645fbfea8f71cd57779974",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 4985945,
"upload_time": "2025-08-16T02:27:37",
"upload_time_iso_8601": "2025-08-16T02:27:37.706782Z",
"url": "https://files.pythonhosted.org/packages/a3/60/9a924ee28cd1d12f2482834581d9024bf05110aa1098c056e847f05f7f76/z3_solver-4.15.3.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-16 02:27:37",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "Z3Prover",
"github_project": "z3",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "z3-solver"
}
JSON
