Path to this page:
./
math/py-smt,
Library for SMT formula manipulation and solving
Branch: CURRENT,
Version: 0.9.6,
Package name: py312-smt-0.9.6,
Maintainer: pkgsrc-userspySMT is a solver-agnostic library for SMT Formulae manipulation and
solving.
pySMT makes working with Satisfiability Modulo Theory simple:
- Define formulae in a simple, intuitive, and solver independent way
- Solve your formulae using one of the native solvers, or by wrapping
any SMT-Lib compliant solver,
- Dump your problems in the SMT-Lib format,
- and more...
Master sites:
Filesize: 256.646 KB
Version history: (Expand)
- (2024-11-11) Updated to version: py312-smt-0.9.6
- (2024-08-07) Updated to version: py311-smt-0.9.6
- (2024-08-07) Updated to version: py311-PySMT-0.9.6
- (2023-01-09) Updated to version: py310-smt-0.9.5
- (2022-01-05) Updated to version: py39-smt-0.9.0nb2
- (2022-01-05) Updated to version: py39-smt-0.9.0nb1
CVS history: (Expand)
2024-11-11 08:29:31 by Thomas Klausner | Files touched by this commit (862) |
Log message:
py-*: remove unused tool dependency
py-setuptools includes the py-wheel functionality nowadays
|
2024-08-07 21:32:48 by Thomas Klausner | Files touched by this commit (1) |
Log message:
py-smt: fix PKGNAME
|
2024-08-07 13:01:45 by Adam Ciarcinski | Files touched by this commit (4) | |
Log message:
py-smt: updated to 0.9.6
0.9.6: 2022-06-24 -- CVC5 and upgraded solvers
* Fixed issue 613
* Fix missing file in Manifest
* Upgrade MathSAT to 5.6.6
* CI: Avoid running on PR branch push
* Upgrade MathSAT to 5.6.7
* Fix misspellings
* Upgrade Z3 to 4.8.17
* make FormulaContextualizer singleton in FormulaManager.
* README: Remove interpolants from Z3
* Parse logic str in Portfolio
* Make sudoku.py Python3 compatible
* Fix the definition of BVXnor
* Deterministic get_closer_logic
* Grammar correction
* example/parallel.py: typo fix
* Fix for pyximport
* Remove deprecated distutils
* Fixed removed imp module in Python 3.12
* [Boolector] Add support for const arrays and boolean indices/elements
* Update of all solvers
|
2023-05-11 11:18:47 by Adam Ciarcinski | Files touched by this commit (1) |
Log message:
py-smt: mark as PYTHON_SELF_CONFLICT=yes
|
2023-01-09 07:39:38 by Pierre Pronchery | Files touched by this commit (3) | |
Log message:
py-smt: update to 0.9.5
From the release notes:
Intermediate release that collects 2 years of bugfixes and improvements.
Python 2 was deprecated in version 0.9.0, and this version removes the use of \
compatible code for that version.
What's Changed
* Add support for boolean-typed array in the AtomsOracle by @mikand in #644
* Switched from nosetests to pytest by @mikand in #662
* Fixed a bug in yices quantifier support and added regression test by @mikand \
in #657
* Fix Boolector install script by @4tXJ7f in #656
* BUG: define UFNIA as logic with integer arithmetic by @johnyf in #659
* Handling of algebraic constants in simplify by @EnricoMagnago in #658
* Integer div by @EnricoMagnago in #667
* Fix CVC4 installation on macOS by @kammoh in #666
* Bug in times distributor by @EnricoMagnago in #671
* Fixed reset_assertion method for incremental-tracking solvers by @mikand in #672
* Minor Corrections by @mfarif in #673
* implement add_assertions method for solver. by @EnricoMagnago in #679
* Fix "get_model" when called from a generic solver (Fix #674) by \
@btwael in #675
* Remove six and python 2 compatibility code by @marcogario in #684
* Added fallback to Swig3 to address as much as possible issue #682 by @mikand \
in #685
* Fix to correctly pass logic to solvers started by Portfolio by @ekilmer in #683
* SmtLib model validation support by @mikand in #681
* Fix iss694 by @EnricoMagnago in #695
* Fixed CVC4 installer after upstream repository renaming by @mikand in #697
* Remove call to FNode.substitute in SmtLibExecutionCache by @EnricoMagnago in #699
* Added printing of annotations to smt lib printers by @agirardi-fbk in #703
* Integer div by @EnricoMagnago in #705
* Updated docker images to solve deprecation issue on azure pipelines by @mikand \
in #706
* Workaround to fix Z3 segfault by @mikand in #713
* Add possibility to use several BV operators as left associative by \
@agirardi-fbk in #714
* Fixed issue #613 by @mikand in #710
|
2022-01-05 16:41:32 by Thomas Klausner | Files touched by this commit (289) |
Log message:
python: egg.mk: add USE_PKG_RESOURCES flag
This flag should be set for packages that import pkg_resources
and thus need setuptools after the build step.
Set this flag for packages that need it and bump PKGREVISION.
|
2022-01-04 21:55:40 by Thomas Klausner | Files touched by this commit (1595) |
Log message:
*: bump PKGREVISION for egg.mk users
They now have a tool dependency on py-setuptools instead of a DEPENDS
|
2021-10-26 12:56:13 by Nia Alarie | Files touched by this commit (458) |
Log message:
math: Replace RMD160 checksums with BLAKE2s checksums
All checksums have been double-checked against existing RMD160 and
SHA512 hashes
|