- 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
OBS-URL: https://build.opensuse.org/request/show/1073729
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/stp?expand=0&rev=14
- 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.
OBS-URL: https://build.opensuse.org/request/show/991176
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/stp?expand=0&rev=12
- 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
OBS-URL: https://build.opensuse.org/request/show/678883
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/stp?expand=0&rev=4
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
