Revisions of stp

Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 1153133 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 15)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 1073729 from Jiri Slaby's avatar Jiri Slaby (jirislaby) (revision 14)
- 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
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 992451 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 13)
Automatic submission by obs-autosubmit
Richard Brown's avatar Richard Brown (RBrownFactory) accepted request 991176 from Jiri Slaby's avatar Jiri Slaby (jirislaby) (revision 12)
- 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.
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 977898 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 11)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 964258 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 10)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 875288 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 9)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 847740 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 8)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 770494 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 7)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 721465 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 5)
Automatic submission by obs-autosubmit
Stephan Kulow's avatar Stephan Kulow (coolo) accepted request 678883 from Jiri Slaby's avatar Jiri Slaby (jirislaby) (revision 4)
- 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
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 534437 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 3)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 480945 from Factory Maintainer's avatar Factory Maintainer (factory-maintainer) (revision 2)
Automatic submission by obs-autosubmit
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 458928 from Jiri Slaby's avatar Jiri Slaby (jirislaby) (revision 1)
stp is needed by klee
Displaying all 15 revisions
openSUSE Build Service is sponsored by