Revisions of stp
Ana Guerrero (anag+factory)
accepted
request 1185725
from
Factory Maintainer (factory-maintainer)
(revision 16)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 1153133
from
Factory Maintainer (factory-maintainer)
(revision 15)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 1073729
from
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 (dimstar_suse)
accepted
request 992451
from
Factory Maintainer (factory-maintainer)
(revision 13)
Automatic submission by obs-autosubmit
Richard Brown (RBrownFactory)
accepted
request 991176
from
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 (dimstar_suse)
accepted
request 977898
from
Factory Maintainer (factory-maintainer)
(revision 11)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 964258
from
Factory Maintainer (factory-maintainer)
(revision 10)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 875288
from
Factory Maintainer (factory-maintainer)
(revision 9)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 847740
from
Factory Maintainer (factory-maintainer)
(revision 8)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 770494
from
Factory Maintainer (factory-maintainer)
(revision 7)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 762244
from
Martin Pluskal (pluskalm)
(revision 6)
Dominique Leuenberger (dimstar_suse)
accepted
request 721465
from
Factory Maintainer (factory-maintainer)
(revision 5)
Automatic submission by obs-autosubmit
Stephan Kulow (coolo)
accepted
request 678883
from
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 (dimstar_suse)
accepted
request 534437
from
Factory Maintainer (factory-maintainer)
(revision 3)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 480945
from
Factory Maintainer (factory-maintainer)
(revision 2)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 458928
from
Jiri Slaby (jirislaby)
(revision 1)
stp is needed by klee
Displaying all 16 revisions