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
In the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/z3prover/z3.git
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": "",
"maintainer_email": "audrey@rhelmot.io",
"keywords": "z3,smt,sat,prover,theorem",
"author": "The Z3 Theorem Prover Project",
"author_email": "",
"download_url": "https://files.pythonhosted.org/packages/3a/fd/e3f5850fd04480a942aca9f9f7520d3fa5b57731335c221a11f55bb6d91a/z3-solver-4.13.0.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\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/z3prover/z3.git\n",
"bugtrack_url": null,
"license": "MIT License",
"summary": "an efficient SMT solver library",
"version": "4.13.0.0",
"project_urls": {
"Homepage": "https://github.com/Z3Prover/z3"
},
"split_keywords": [
"z3",
"smt",
"sat",
"prover",
"theorem"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "4e5b934de9f1f31b1d0f3a8da0ff2e3092136fbffe737eca52965818464af4c3",
"md5": "1f250f93592d593db4b0eb7a082c0fd8",
"sha256": "bca7d59a699a440247537c2180c519d682c9df3520a16ce288fced61a70d253d"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-macosx_11_0_arm64.whl",
"has_sig": false,
"md5_digest": "1f250f93592d593db4b0eb7a082c0fd8",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 27144281,
"upload_time": "2024-03-07T19:19:36",
"upload_time_iso_8601": "2024-03-07T19:19:36.033887Z",
"url": "https://files.pythonhosted.org/packages/4e/5b/934de9f1f31b1d0f3a8da0ff2e3092136fbffe737eca52965818464af4c3/z3_solver-4.13.0.0-py2.py3-none-macosx_11_0_arm64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "9c20f28dfa982bc820760117e5615d59d695d12a6fb31660f53a749be27cccca",
"md5": "fc5901390310ead5a7a28e5a395d6fc4",
"sha256": "4a4731fded91b32e1861e1c7c96e500da743bb9431246cac51f7c3ffc0f21b5d"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-macosx_11_0_x86_64.whl",
"has_sig": false,
"md5_digest": "fc5901390310ead5a7a28e5a395d6fc4",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 30107615,
"upload_time": "2024-03-07T19:19:45",
"upload_time_iso_8601": "2024-03-07T19:19:45.679792Z",
"url": "https://files.pythonhosted.org/packages/9c/20/f28dfa982bc820760117e5615d59d695d12a6fb31660f53a749be27cccca/z3_solver-4.13.0.0-py2.py3-none-macosx_11_0_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "0e8c9058d3998fdc2148f3e6d3497e949d5dfc77c66b1cc1cb461554c0bba954",
"md5": "a2624198f0d229339758f43466dc4352",
"sha256": "9d622022a3511c059915c56b2c231c84b5c1be1b82f457d7560dda3d916474fe"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-manylinux2014_aarch64.whl",
"has_sig": false,
"md5_digest": "a2624198f0d229339758f43466dc4352",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 55585725,
"upload_time": "2024-03-07T19:19:49",
"upload_time_iso_8601": "2024-03-07T19:19:49.810450Z",
"url": "https://files.pythonhosted.org/packages/0e/8c/9058d3998fdc2148f3e6d3497e949d5dfc77c66b1cc1cb461554c0bba954/z3_solver-4.13.0.0-py2.py3-none-manylinux2014_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "c6790255fe0efee7ea9db8987ced14c70028a0007d4d4aaaed8965310bbd7bb1",
"md5": "65dc49a5ebeaad9c76945db97da93123",
"sha256": "8c42de82b6e3ff7ee61287d03c7af8a99f9f6554cdd1204c6b9bca96ff1cb7fb"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-manylinux2014_x86_64.whl",
"has_sig": false,
"md5_digest": "65dc49a5ebeaad9c76945db97da93123",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 57305826,
"upload_time": "2024-03-07T19:19:54",
"upload_time_iso_8601": "2024-03-07T19:19:54.261836Z",
"url": "https://files.pythonhosted.org/packages/c6/79/0255fe0efee7ea9db8987ced14c70028a0007d4d4aaaed8965310bbd7bb1/z3_solver-4.13.0.0-py2.py3-none-manylinux2014_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "b927ca09e1f4642b42a2972047f508bc4ecb0c5acf975c910eb0fdeaf9ec21d0",
"md5": "3fe1512e70a2cb278608368deb161d75",
"sha256": "13468e1018c817b7f794898d3100f02541d15c13ab56c0785c5acdea32a066cf"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-win32.whl",
"has_sig": false,
"md5_digest": "3fe1512e70a2cb278608368deb161d75",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 55429050,
"upload_time": "2024-03-07T19:19:58",
"upload_time_iso_8601": "2024-03-07T19:19:58.867343Z",
"url": "https://files.pythonhosted.org/packages/b9/27/ca09e1f4642b42a2972047f508bc4ecb0c5acf975c910eb0fdeaf9ec21d0/z3_solver-4.13.0.0-py2.py3-none-win32.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "25c0dd978c813288f6860bcfb9e4d2d1d3b311a42a2237a4766e5a0adbcaa79b",
"md5": "fdcd1b43b7098b10ccfe5c893b78979b",
"sha256": "3555436cfe9a5fa2d1b432fb9a5e4460e487649c22e5e68a56f7d81594d043e9"
},
"downloads": -1,
"filename": "z3_solver-4.13.0.0-py2.py3-none-win_amd64.whl",
"has_sig": false,
"md5_digest": "fdcd1b43b7098b10ccfe5c893b78979b",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 58378460,
"upload_time": "2024-03-07T19:20:03",
"upload_time_iso_8601": "2024-03-07T19:20:03.281880Z",
"url": "https://files.pythonhosted.org/packages/25/c0/dd978c813288f6860bcfb9e4d2d1d3b311a42a2237a4766e5a0adbcaa79b/z3_solver-4.13.0.0-py2.py3-none-win_amd64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "3afde3f5850fd04480a942aca9f9f7520d3fa5b57731335c221a11f55bb6d91a",
"md5": "b20f12a6ba24306545aa1a1edca76d6d",
"sha256": "52588e92aec7cb338fd6288ce93758ae01770f62ca0c80e8f4f2b2333feaf51b"
},
"downloads": -1,
"filename": "z3-solver-4.13.0.0.tar.gz",
"has_sig": false,
"md5_digest": "b20f12a6ba24306545aa1a1edca76d6d",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 4848532,
"upload_time": "2024-03-07T19:20:07",
"upload_time_iso_8601": "2024-03-07T19:20:07.192914Z",
"url": "https://files.pythonhosted.org/packages/3a/fd/e3f5850fd04480a942aca9f9f7520d3fa5b57731335c221a11f55bb6d91a/z3-solver-4.13.0.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-03-07 19:20:07",
"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"
}