pool/stp
SHA256
17
0
Fork 2
Code Issues Pull Requests Activity
Files
factory
stp/stp.changes
Ana Guerrero 6033f7a05f Accepting request 1267368 from devel:tools:statica 
- Update to version 2.3.4+20240918:
  * Added dummy diagnostic-output-channel support
  * Make timestamp in generated file use $SOURCE_DATE_EPOCH
  * Use sysconfig, not distutils, to find python root
  * Move to CMS @ 5.11.22
  * Bump CMS revision to b735c94

- Add missing BuildRequires python3-setuptools

OBS-URL: https://build.opensuse.org/request/show/1267368
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/stp?expand=0&rev=18
2025-04-07 15:37:24 +00:00

604 lines
24 KiB
Plaintext
Raw Permalink Blame History

-------------------------------------------------------------------
Fri Mar 28 06:58:48 UTC 2025 - jslaby@suse.cz
- Update to version 2.3.4+20240918:
* Added dummy diagnostic-output-channel support
* Make timestamp in generated file use $SOURCE_DATE_EPOCH
* Use sysconfig, not distutils, to find python root
* Move to CMS @ 5.11.22
* Bump CMS revision to b735c94
-------------------------------------------------------------------
Mon Mar 10 10:26:08 UTC 2025 - Marius Grossu <marius.grossu@suse.com>
- Add missing BuildRequires python3-setuptools
-------------------------------------------------------------------
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
Reference in New Issue View Git Blame Copy Permalink