Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: stp | Distribution: openSUSE Tumbleweed |
Version: 2.3.4+20240611 | Vendor: openSUSE |
Release: 1.1 | Build date: Fri Jun 28 08:06:35 2024 |
Group: Unspecified | Build host: reproducible |
Size: 169868 | Source RPM: stp-2.3.4+20240611-1.1.src.rpm |
Packager: http://bugs.opensuse.org | |
Url: https://github.com/stp/stp/wiki | |
Summary: Constraint Solver |
STP is an efficient decision procedure for the validity (or satisfiability) of formulas from a quantifier-free many-sorted theory of fixed-width bitvectors and (non-extensional) one-dimensional arrays. The functions in STP's input language include concatenation, extraction, left/right shift, sign-extension, unary minus, addition, multiplication, (signed) modulo/division, bitwise Boolean operations, if-then-else terms, and array reads and writes. The predicates in the language include equality and (signed) comparators between bitvector terms.
MIT
* Fri Jun 28 2024 jslaby@suse.cz - Update to version 2.3.4+20240611: * use simple CNF encoding when simplifications are disabled * Update ci.yml -- oops fix. * Update ci.yml - hack to stop mystery failure. * Allow it to more naturally create >64-bit constants * Return >64 bit values properly * fix CMS version. Disable CMS assertions * Add new GMP dependency to dockerfile * Get the current lastest CMS when building * Add that we require GMP * get later version to fix compiler error * Install cadiback dependency (#482) * Thu Feb 22 2024 jslaby@suse.cz - Update to version 2.3.3+20231214: * Partially fix Appveyor (windows) automated build. (#478) * Trying again to get clang building the api tests * fixes #476 * Trying to get uint32_t found on clang. * Partial revert previous checkin because some code needs this include. * Improved word wrap. * Update index.rst * Update README.markdown * Remove nonsensical sbrk usage * fix compiler warnings. * Build script for docker based on the quick install for Ubuntu 20 * add extra test case for let, currently not functional * Implement smtlib2 format "let" properly. Fixes #388 * Adding let tests * Update README.markdown * Improve build instructions * [gcc 13] include cstdint for *int*_t - remove 0001-gcc-13-include-cstdint-for-int-_t.patch (upstream) * Wed Mar 22 2023 jslaby@suse.cz - Update to version 2.3.3+20220915: * Fix compilation error on libstdc++-7-dev * disable SQLITE when building cms * Fix so user flags are respected * Convert ordered collections to faster unordered collections. * copy on write to reduce the number of malloc/free * Cleanup the dependency building code * Small changes to make core simplification algorithms faster. * Improve again on the performance of QF_BV benchmark problems. * Handle an extra case in unconstrained variable elimination. * Improve again on the performance of QF_BV benchmark problems. * Fix test cases so that they work when stp has pure variable removal disabled. * Tune the parameters to improve performance on QF_BV benchmark problems * Adding REQUIRE for Perl * Remove some mentions of the CVC format from our documentation. * Remove mention of CVC from front readme. * Update codeql-analysis.yml * fix #128 * Clarrify as discussed in #4, that the bitvector library is also licensed under the artistic licence. * move cvc_to_c utility out of unit testing into tools. * remove tests which are not currently being used * Update main.cpp * Adds an extra simplification rule. fix #381. * Fix #383. Makes bvxnor 2-arity only. * oops. Fix inadvertent checkin * Write through unapplied simplfications. Previously this was unsound if unconstrained variable elimination (UVE) was disabled. UVE wrote through unapplied simplifications so masked the problem. * rename tests which aren't really unit tests. * Improve testing. The intention of these is that the combination of simplifications reduces them to true or false before reaching the SAT solver. * Enable some generated tests that weren't previously enabled * remove old test generators. FuzzSMT is much better than these * Add failing instance * Update codeql-analysis.yml * Fix testing failures. Lit 15 is trying to run the test suites which I think is causing a CI failure. * Remove disabled CVC test file. In some configurations it seems to be run resulting in a spurious test failure * Cleanup memory leak on shutdown. * Add the dissertation which also describes parts of STP * silence some compiler warnings * Fixing up some of the tools * Update index.rst * Rewrite Dockerfile * fix #363 * Correcting command line argument for '--max_time' - add 0001-gcc-13-include-cstdint-for-int-_t.patch * Wed Jul 27 2022 Jiri Slaby <jslaby@suse.cz> - add CMakeLists-use-absolute-libdir-in-rpath-handling.patch * Tue Jul 26 2022 Jiri Slaby <jslaby@suse.cz> - fix rpath (don't use relative lib64) - switch python to noarch - Update to version 2.3.3+20220722: * Added reviewer's suggestions * Fixed the broken link on SMT-LIBv2 documentation. * Fix cli to disable new simplifications with --disablesimplifications * enable sharing-aware rewrites by default. * Extra simplification rule. * re-enabling removal of BVOR to evaluate how important it is. * some more simplification rules. * Improved simplifications * Faster/better Always true identification * First attempt at sharing aware rewrites. * Create 100000... * Nicer implementation of Always true. * Remove the unnecessary use of a SCARY iterator that may break on older compilers * Cleanup memory leaks. Nicer signed comparison on unsigned interval. * Nicer domain analyis. * extra test case for strength reduction. * Strength reduction now iterates through. This should make it idempotent and deterministic. * Make the new PropagateEqualities deterministic * Find non-overlapping extracts of variables and replace them with fresh variables. * Changes to how domain information about bit-vector nodes is stored. * and some more. * Wed May 11 2022 jslaby@suse.cz - Update to version 2.3.3+20220507: * Don't save a pointer to node factor in case it gets updated later * Improved pure literal removal and unit test * Simplify less than one to equal to zero. * handle more cases and better testing of simplifying node factory * refactor. Clean up initialisation of STP in a tool. * Make initialising STP slightly easier. * remove some more default functions. * refactor. Remove substitition map out of simplifier class. * Remove a flag that wasn't read. * Remove a dead path and the associated flag. * Refactor. Use node factory rather than STPMgr. * Remove simplifier from substitution map. * Make more things private in Simplifier * refactor. Moving some code out of simplify * deleting some default generated constructors * Wed Mar 16 2022 jslaby@suse.cz - Update to version 2.3.3+20220314: * doc: fix typo * stop aig rewriting if the number of and nodes doesn't reduce. * Add command line option to control whether size reducing simplifications fixed point. * refactor. Order the user flags. * remove unreachable option * Enable the setting of more options via the command-line arguments. * fixes 421 * Trial assigning to flags at definition time. * remove unused includes * Fix. adaed499e3d24bcf906852a6c428df07b5a6cee2 shouldn't have turned on flattening when simplifications are disabled. * Fix. Nodes that are complements shouldn't evaluate as being equal. * and much more * Fri Feb 19 2021 jslaby@suse.cz - Update to version 2.3.3+20210104: * Creating an API to get the value/index size from a 'Type' * Wed Nov 04 2020 jslaby@suse.cz - Update to version 2.3.3+20201027: * Ensuring that we do not create double frames when creating a new frame; closes #385 * Fix build for minisat, using stp/minisat * First look for installed MiniSat, then the built one * Fixing warnings by GitHub static code analysis * Allow finding minisat through CONFIG first * Create codeql-analysis.yml * Ensuring documentation consistency with the use of semicolon vs. period * Correcting double backticks in README * Updating README to update build steps and document how to run CMake without installing STP's dependencies system-wide * Importing the latest 'GetGitRevisionDescription' CMake modules from rpavlik/cmake-modules * Ensuring that all CMake targets are correct to support no-op builds * Updating code to use C++11 autos for readability * and much more - switch to obs_scm * Wed Nov 04 2020 Jiri Slaby <jslaby@suse.cz> - fix build on 12sp5 -- define Python_ADDITIONAL_VERSIONS to 3
/usr/bin/stp /usr/bin/stp_simple /usr/share/doc/packages/stp /usr/share/doc/packages/stp/AUTHORS /usr/share/doc/packages/stp/README.markdown /usr/share/licenses/stp /usr/share/licenses/stp/LICENSE
Generated by rpm2html 1.8.1
Fabrice Bellet, Sun Aug 18 01:11:36 2024