Please read this before reporting a bug:
https://wiki.archlinux.org/title/Bug_reporting_guidelines
Do NOT report bugs when a package is just outdated, or it is in the AUR. Use the 'flag out of date' link on the package page, or the Mailing List.
REPEAT: Do NOT report bugs for outdated packages!
https://wiki.archlinux.org/title/Bug_reporting_guidelines
Do NOT report bugs when a package is just outdated, or it is in the AUR. Use the 'flag out of date' link on the package page, or the Mailing List.
REPEAT: Do NOT report bugs for outdated packages!
FS#68010 - [yices] Enable support for Non-Linear Arithmetic and MC-SAT
Attached to Project:
Community Packages
Opened by Dario Ostuni (dariost) - Saturday, 26 September 2020, 17:38 GMT
Last edited by Felix Yan (felixonmars) - Thursday, 17 December 2020, 21:53 GMT
Opened by Dario Ostuni (dariost) - Saturday, 26 September 2020, 17:38 GMT
Last edited by Felix Yan (felixonmars) - Thursday, 17 December 2020, 21:53 GMT
|
DetailsDescription:
It would be nice to enable MC-SAT for the yices package to make it support Non-Linear Arithmetic logics and more. The steps needed to enable it are described in their README here: https://github.com/SRI-CSL/yices2#support-for-non-linear-arithmetic-and-mc-sat The work needed to enable this feature would be to create packages for the required dependencies for this feature, namely libpoly (https://github.com/SRI-CSL/libpoly) and CUDD (https://github.com/ivmai/cudd), and then enable a compilation flag on yices. This feature is not present in Arch Linux yices package as of version 2.6.2-1. |
This task depends upon
Closed by Felix Yan (felixonmars)
Thursday, 17 December 2020, 21:53 GMT
Reason for closing: Implemented
Additional comments about closing: yices 2.6.2-2
Thursday, 17 December 2020, 21:53 GMT
Reason for closing: Implemented
Additional comments about closing: yices 2.6.2-2