-------------------------------------------------------------------------------- Fedora Update Notification FEDORA-2024-b9ead9f89f 2024-02-29 02:05:41.477356 -------------------------------------------------------------------------------- Name : cvc5 Product : Fedora 39 Version : 1.1.1 Release : 1.fc39 URL : https://cvc5.github.io/ Summary : Automatic theorem prover for SMT problems Description : CVC5 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fifth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3, CVC4) but does not directly incorporate code from any previous version prior to CVC4. CVC5 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. -------------------------------------------------------------------------------- Update Information: Changes in version 1.1.1: Reorient equalities propagated by equality engine (#10171), leads to fewer unique literals asserted to theories. Do not eagerly lift lambdas due to constructors (#10244). Would cause us to say "unknown" for some "sat" problems when lambdas involved e.g. datatype constructors. Add unprocessed theory conflict check (#10248). This adds an extra safeguard to when we answer "sat" to check if any theory believes there is a conflict. In this case, we should answer "unknown" (in production) and give an assertion failure in debug. This would have caught previous issues with HO+quantifiers. Update strings to gradual type system (#9821). Update BV to gradual type system (#9819). This updates BV's type system to allow arguments of BV operators to have abstract types. cmake: Update GMP version to 6.3.0 (#10259). Fixes #10174. Add support for forward declarations :fwd-decls in sygus (#10217). This allows functions-to-synthesize to appear in grammars. To do this, we rely on (higher- order) equalities in sygus verification calls. Note this requires changing the error handling of free variables in grammars, since we do not have access to the set of functions-to-synthesize at the API level. extract ff's CoCoA encoder (#10204) Always use stream input when piping from stdin (#10267). Fixes #10258. This removes the option stdin-input-per-line which was used as a way of avoiding stream inputs with the old Flex parser when piping from stdin. This fixes issues when piping from stdin, in terms of performance, diagnostic information, and spurious error reporting. Throw logic exception for POW during preregistration (#10249). We currently throw a logic exception for POW during rewriting if it cannot be eliminated. This is wrong, and leads to spurious exceptions e.g. when doing rewrite generalization analysis (e.g. for proof minimization). This PR changes the behavior so we throw an exception during preregistration instead. cmake: Require GMP 6.3. (#10271). Versions prior to 6.3 have issues on arm64 platforms, which led to multiple segfault issues in cvc5. ff: core algorithms for BitSplit (#10270). Revert behavior changes to interactive shell (#10268). This commit changed the behavior of the interactive shell to use setStringInput instead of setIncrementalStringInput / appendIncrementalStringInput. This change introduces a new private method to replicate the old behavior, where we do not reallocate a parser each line, which leads to issues (which happened to be found in #10258). It furthermore corrects an issue in incremental when using the parser API, where multiple "outermost contexts" could be pushed on a symbol manager, which leads to synchronization issues concerning scope levels in symbol manager. Also adds a test for the interactive shell that would have caught this. Add missing upward inference rule for bag.map operator (#10269). This PR fixes an issue found during model construction when mapped bags are missing elements from the original bags. The cause was simply missing upward rule for bag.map operator. Remove unnecessary quantifiers options (#10246). Moreover these option names may be confusing with forthcoming eager cbqi techniques. Also moves tracking of the "conflicting instance" flag to quantifiers inference manager, in preparation for further additions. Fix for printing success with echo (#10272). Fixes #10257. ff: hook up SplitGB solver (#10274). Minor fixes in Python API doc (#10281). Recommend installing cython as a pip package. Use standard double quotation marks. Always clone proofs when printing (#10282https://github.com/cvc5/cvc5/pull/10282). Fixes #10279. Also fixes an issue where we would segfault if unsat cores but not proofs were enabled, adds a test for this. -------------------------------------------------------------------------------- ChangeLog: * Tue Feb 20 2024 Jerry James <loganjerry@xxxxxxxxx> - 1.1.1-1 - Version 1.1.1 -------------------------------------------------------------------------------- This update can be installed with the "dnf" update program. Use su -c 'dnf upgrade --advisory FEDORA-2024-b9ead9f89f' at the command line. For more information, refer to the dnf documentation available at http://dnf.readthedocs.io/en/latest/command_ref.html#upgrade-command-label All packages are signed with the Fedora Project GPG key. More details on the GPG keys used by the Fedora Project can be found at https://fedoraproject.org/keys -------------------------------------------------------------------------------- -- _______________________________________________ package-announce mailing list -- package-announce@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to package-announce-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/package-announce@xxxxxxxxxxxxxxxxxxxxxxx Do not reply to spam, report it: https://pagure.io/fedora-infrastructure/new_issue
