Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
devel:tools:statica
stp
stp.changes
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
File stp.changes of Package stp
------------------------------------------------------------------- Fri Jun 28 06:06:35 UTC 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 08:05:19 UTC 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 09:20:33 UTC 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 06:45:36 UTC 2022 - Jiri Slaby <jslaby@suse.cz> - add CMakeLists-use-absolute-libdir-in-rpath-handling.patch ------------------------------------------------------------------- Tue Jul 26 04:31:49 UTC 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 08:48:14 UTC 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 10:19:08 UTC 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 07:27:14 UTC 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 08:57:04 UTC 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 4 07:14:40 UTC 2020 - Jiri Slaby <jslaby@suse.cz> - fix build on 12sp5 -- define Python_ADDITIONAL_VERSIONS to 3 ------------------------------------------------------------------- Thu Jan 30 09:45:21 UTC 2020 - jslaby@suse.com - Update to version 2.3.3+20200113: * Fixing tests so build doesn't break * Removing slow running tests * Better support for python in build * less bad model printing for arrays. * Change reference to Minisat repo * extra little one. * Removing tests that take 1 minute to execute ------------------------------------------------------------------- Thu Jan 9 14:11:38 UTC 2020 - Martin Pluskal <mpluskal@suse.com> - Python3 bindings subpackage should be named correctly - More modern cmake macros ------------------------------------------------------------------- Thu Jan 9 12:25:51 UTC 2020 - Ondřej Súkup <mimi.vx@gmail.com> - build python3 bindings + patch py3.patch - drop dependecy on python devel .. not needed ------------------------------------------------------------------- Wed Jul 31 09:05:35 UTC 2019 - jslaby@suse.com - Update to version 2.3.3+20190713: * fix #330. * Partial fix for #330. * Hack to get a smtlib benchmark parsing. * Decimal output is incredibly slow for ~30,000 bits. * Timeout tests are way too slow, removing * fix. wasn't printing success like it should on some smtlib commands. * -p will now print smtlib2 format models when the smtlib2 parser is selected. smtlib2 models contain all the variables (even those that can take any value). * don't output a model if it was unsat. * fix boolean model output. ------------------------------------------------------------------- Sat Feb 23 08:31:26 UTC 2019 - jslaby@suse.com - Update to version 2.3.2+20190222: * Don't cache data in case of error * Reordering riss library, maybe that will fix the issue * Trying to fix appveyor * Let's see the output of RISS being built * No need for rdynamic hackery * It's best to name the library target "stp" not "libstp" * Fixing using <packagename>_ROOT variables * Adding compiler options * Fixing the mess that staticcompile was causing * Fixing version-number based issue with the Docker image * Removing gcc extension of C++, not needed * Let's fix up Appveyor for static build - Note that the build is fixed with bison 3.3.2. - remove 0001-CMake-fix-dirs-again.patch, in upstream now ------------------------------------------------------------------- Tue Oct 10 11:31:21 UTC 2017 - jslaby@suse.com - Update to version 2.3.1+20171008: * Reducing scope of upper&lower * Using $() instead of `` * Removing unused code * Removing unused code * Adding docker file -- not working yet * Fixing install and library location RPATH * Updating README, fixing Docker * Fixing static build * Removed unused global variable * Provide thread-safety (if C++11) * Removing tests are too long and hold up development (>10s runtime each) * Cleaning up lexer * Cleanup of smt2.lex * We can use straight-up "thread_local" here * Trying to fix the thread-local storage for C * Mark two more global variables as thread_local * Updating READMEs * No need for this parameter in AppVeyor * No need for INSTALL, it's been incorporated into the README * Updating README * Fixing indentation and some restructuring of README * Better naming of header * Removing DLL_EXPORT on variables that break the build * Using the ctest framework for testing * Actually checking things in tests, reducing their outputs * Making the interface's (vc) more explicit * Removing trailing space * Tabs to spaces conversion * Trailing spaces removed * Minimal cleanup of the lexer * Fixing std::endl -> endl; * Commenting out unused parameter * Fix indentation * Cleaner lexer * Highlighting where GlobalParserInterface is being used * Fixing the assert * No need to undefine this, it should work without * Some cleanup of bison&flex usage * Fixing moving of header file * No need for linenum * Removing helpstring * Removing unneeded files * Removing one more static variable * Reflowing code as per agreed clang-format * Further cleanup * Removing unused code * Cleanup of tests mostly * Making the visibility=hidden work * Don't care about coveralls fail * Fixing AppVeyor build * Fixing the coverage script * Removing comments from CMakeLists * Fixing ARM compile issue as in new libabc * Adding SUSE build files * Fixing fuzz-testing to use python2 * Simplifying the Docker usage * Fixing the Docker example - add 0001-CMake-fix-dirs-again.patch ------------------------------------------------------------------- Thu Aug 17 12:01:28 UTC 2017 - jslaby@suse.com - Update to version 2.2+20170815: * Removing broken link * PEP8 + print function in fuzzer * More correct printf * Fixing double-declaration * Fixing memory leak * NULL-ing ptr sent to DELETE is now automatic and more meaningful * Deleting buckets after they have been used * This will fatal error anyway, so just use the pattern and return false * added support for MSVC attributes * disabled crtdbg.h inclusion in extlib-abc for C++ debug builds * fixed unistd.h dependencies for Windows builds * added missing include directive * refactored gettimeofday() for Win32 * Adding appveyor file * Adding missing appveyor file * Fixing paths * Adding zlib for minisat to appveyor * Using minisat that's been fixed to build in VS * Better comments in the AppVeyor filBetter comments in the AppVeyor filee * Temporarily disable boost * Install for appveyor minisat * Fixing "libs" to "lib" for minisat * Debugging MiniSat finding in AppVeyor * Debugging Windows build * Debugging Windows build * Debugging Windows build * Installing CygWin * Use 64b CygWin * Trying a different way of installing CygWin * Fixing CygWin * Fixing local package dir * Fixing CygWin site location * Adding CygWin prefix path * Fixing some warnings * Fixing one more signed vs unsigned issue * Suppress warning messages from msbuild * Moving implementation of destructor * No warnings from msbuild * We need ZLIB in STP thanks to MiniSat * Warnings cannot be suppressed in msbuild * Trying to fix Boost in AppVeyor * Removing unused cygwin install command * Fixing yml for AppVeyor * Removing a warning * Fixing signedness and unreachable code warnings * Removing useless comments * Removing dead code * Removing more dead code * Fixing unused parameter warning * Trying to make symbol-hiding work * Trying to remove too much warnings * change semantics of division / remainder by zero * fix bvsmod-by-zero for negative first operand. * Adding constants.h that was missing * Removing unused include * Revert "Removing unused include" * Fix simplifications rules made incorrect by change in semantics of division-by-zero. * Work-around another division by zero semantics defect. * documented the entire old C API interface header with doxygen comments * Try to get clang/static build passing on travis ci. * Try to move from precise to trusty on travis ci. Precise ends support soon. * Revert "Try to move from precise to trusty on travis ci. Precise ends support soon." * test that static binary is really staitc. * Fix leak introduced in #f452c0e * Trying again to upgrade to trusty. * fixed DLL_PUBLIC-related linkage errors * Trying to fix static clang build * Renaming clang static build * Renaming build type in Travis * Trying to fix shared/static library building * Updating static binary check * moved DLL_PUBLIC definition, added __declspec(dllimport) definition * Trying to fix AppVeyor * Trying to fix Appveyor -- wrong staticcompile check fix * Importing Felix Kutzner's fixes. Thanks a lot! * added declarations for ..._scan_string functions * Fixing boost library include, thanks to Felix Kutzner * Some obvious fix for MSVC compile * enabled shared library building with MSVC * fixed DLL export warning for isatty * no -static for MSVC linker * Testing more of clang * made the Python binding build scripts usable with MSBuild * re-enabled DLL building with MSVC * Adding an empty global to compiler clang * No need for CPP11 build check, Trusty has CPP11 compiler * added DLL_PUBLIC markers to the C interface * Fixing Travis build instructions * made the query-file-tests usable with MSBuild * Fixing the environment for clang builds * Fixing LIT issue * Final fixes to static compilation * added DLL copying for tests * forcing gtest to use the right C/C++ runtime * added python to AppVeyor (for tests) * Just use CryptoMiniSat from GIT, it's more stable for static compilation * Better visibility into executable files generated * deactivated boost in AppVeyor (not supported yet) * adjusted lit tool path * Fixing cryptominisat GIT link * Fixing clang build issue * Adding build SHA1 * Don't specify makefile type * Trying to fix KLEE build * Fixing static binary check * Adding clang static build script * Fixing tests for static builds * All builds should run "make check" * Debugging fuzzing * Fixing Windows build * Adding clang build files * Fixing static compilation of tests * Fixing local build scripts * Fixing python test generation * Fixing cryptominisat selection in fuzzer * Debugging fuzzing issue in Travis * Fixing directory of build for static CMS * Building all combinations for gcc&clang * KLEE doesn't want to build, so let's not build it * Don't build COVERAGE using clang, it doesn't work * fixed #253: DLL_IMPORT in c_interfaces leaks API and breaks installation of STP * Leave an empty line before "exclude" in TravisCI * Specify OS for Travis * Making python build again both for Windows and Linux * removed unnecesary include of <stdio.h> in c_interface.h and moved it into implementation * reverted the python interface build scripts * enabled tests in AppVeyor * added the not tool (test dependency) to AppVeyor * repaired the installed version of library_path.py * removed node typedef in c interface * fixed bug introduced in replacing all the things * replaced 'stdX.h' headers with C++-style <cstdX> headers * enabled building with boost in AppVeyor * improved AppVeyor build time * Playing around a bit with build flags * Don't display test output of LIT, it's too much * Adding some comments to AppVeyor * Removing unused variables * Adding EOL to files * Using $() instead of `` * Removing unused code&variables, reducing scope * Removing unsued code in TravisCI * Adding badges * Fixing badges * Adding coverity badge * Fixing potential memory leak * Code cleanup * Revert "Fixing potential memory leak" * Fixing Linux build * using a single output binary directory on Windows * removed the pre-check target * fixed the python binding installation configuration * installing stp.dll in bin/ on Windows * parse license directive in smt2 format. * fixed output directory setup (thanks @delcypher) * made python binding paths more platform independent * cleaned up a fixme comment * disabled test execution on AppVeyor * Adding explanation to option --output-CNF * No need to build CMS's python interface. This will fix TravisCI * cmake: fix ENABLE_PYTHON_INTERFACE option * Some improvements in CMakeLists.txt - Enable RPATH on MacOS X: the STP dynamic library can thus be found more reliably by applications using it - Do not search for Cryptominisat, if NOCRYPTOMINISAT is set to ON - Added configuration option to disable Python interface (ENABLE_PYTHON, default ON) * [CMake] Fix #192 * Fixing cmake in TravisCI * Using auto type * Don't print cmake build&install to Travis * Use ccache * Don't cache in AppVeyor * Making cmake with 2 cores in Travis * No need for the cmake config in TravisCI * We only need the python interpreter for the tests * circumvent Xcode bug with CMake's TARGET_OBJECTS * Using a cleaner way to set C++11 and C99 standards ------------------------------------------------------------------- Mon Feb 27 09:22:51 UTC 2017 - jslaby@suse.com - require only boost-program-options in tumbleweed ------------------------------------------------------------------- Sat Feb 18 18:19:46 UTC 2017 - jslaby@suse.com - create libstp2_1 for library as required by policy ------------------------------------------------------------------- Sun Nov 20 18:29:42 UTC 2016 - jslaby@suse.com - require minisat-devel and boost-devel in -devel ------------------------------------------------------------------- Fri Nov 18 15:09:25 UTC 2016 - jslaby@suse.com - package also stp_simple, needed for cmake find_package - Update to version 2.2+20161105: * Improve performance by creating fewer strings. * GitSHA1: really disable timestamp when requested * ASTNode rvalue reference assignment and copy constructor. * simplifier: use abort() after assert(false) * bug fix. * (1) fix building. (2) make index width / value width out of the base class. Saves 8 bytes in bvconst. * Might fix the issue described in #235. Missing dependencies. * oops. fix build. ------------------------------------------------------------------- Fri Oct 28 06:59:23 UTC 2016 - jslaby@suse.com - update to 20161028 - remove simplifier-use-abort-instead-of-assert-false.patch - remove GitSHA1-really-disable-timestamp-when-requested.patch ------------------------------------------------------------------- Wed Oct 19 06:12:01 UTC 2016 - jslaby@suse.com - update to 20161005 - switch to ninja and %cmake macros - disable timestamps - add simplifier-use-abort-instead-of-assert-false.patch - add GitSHA1-really-disable-timestamp-when-requested.patch ------------------------------------------------------------------- Fri Nov 27 10:58:16 UTC 2015 - jslaby@suse.com - update to 20151122 ------------------------------------------------------------------- Tue Nov 3 10:40:57 UTC 2015 - jslaby@suse.com - update to 20151030 - package AUTHORS and LICENSE ------------------------------------------------------------------- Fri Sep 4 08:31:18 UTC 2015 - jslaby@suse.com - update to 20150904 * remove: AST-simplify-FatalError-and-mark-as-noreturn.patch ------------------------------------------------------------------- Fri Sep 4 08:09:59 UTC 2015 - jslaby@suse.com - remove: fix-no-return-in-nonvoid.patch - add: AST-simplify-FatalError-and-mark-as-noreturn.patch ------------------------------------------------------------------- Thu Sep 3 17:56:22 UTC 2015 - jslaby@suse.com - update to 20150828 * drop one hunk from fix-no-return-in-nonvoid.patch ------------------------------------------------------------------- Mon Apr 20 12:14:45 UTC 2015 - jslaby@suse.com - update to 20150418 * remove: fix-install-paths.patch * remove: no-build-timestamps.patch ------------------------------------------------------------------- Thu Apr 16 09:09:41 UTC 2015 - jslaby@suse.com - update to 20150415 * drop one hunk from fix-no-return-in-nonvoid.patch ------------------------------------------------------------------- Thu Oct 30 10:36:12 UTC 2014 - jslaby@suse.com - add no-build-timestamps.patch ------------------------------------------------------------------- Mon Oct 20 13:51:24 UTC 2014 - jslaby@suse.com - update to 20140928 * many fixes * remove-broken-functions.patch: remove, upstream ------------------------------------------------------------------- Tue Apr 15 09:49:38 UTC 2014 - jslaby@suse.com - initial commit
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor
