diff --git a/packages/s/stp/.files b/packages/s/stp/.files index 189213d..ad9f334 100644 Binary files a/packages/s/stp/.files and b/packages/s/stp/.files differ diff --git a/packages/s/stp/.rev b/packages/s/stp/.rev index c921e9a..c83103e 100644 --- a/packages/s/stp/.rev +++ b/packages/s/stp/.rev @@ -141,4 +141,41 @@ Automatic submission by obs-autosubmit 992451 + + cdebffa9292eb923d3746994c4987a9c + 2.3.3+20220915 + + dimstar_suse + - 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 + 1073729 + diff --git a/packages/s/stp/.servicemark b/packages/s/stp/.servicemark deleted file mode 100644 index 626c82e..0000000 --- a/packages/s/stp/.servicemark +++ /dev/null @@ -1 +0,0 @@ -7e68606fed576d645bd4d3b2a449e94e diff --git a/packages/s/stp/0001-gcc-13-include-cstdint-for-int-_t.patch b/packages/s/stp/0001-gcc-13-include-cstdint-for-int-_t.patch new file mode 100644 index 0000000..3bc88ab --- /dev/null +++ b/packages/s/stp/0001-gcc-13-include-cstdint-for-int-_t.patch @@ -0,0 +1,28 @@ +From 46fde27d3274e84414a55c80231628f9a86c188e Mon Sep 17 00:00:00 2001 +From: Jiri Slaby +Date: Wed, 22 Mar 2023 10:22:16 +0100 +Subject: [PATCH] [gcc 13] include cstdint for *int*_t +References: https://github.com/stp/stp/pull/462 + +Otherwise we see errors like this with gcc13: +include/stp/AST/ASTNode.h:77:3: error: 'uint8_t' does not name a type +--- + include/stp/AST/ASTNode.h | 2 ++ + 1 file changed, 2 insertions(+) + +diff --git a/include/stp/AST/ASTNode.h b/include/stp/AST/ASTNode.h +index e05f8925..a05c15d6 100644 +--- a/include/stp/AST/ASTNode.h ++++ b/include/stp/AST/ASTNode.h +@@ -24,6 +24,8 @@ THE SOFTWARE. + #ifndef ASTNODE_H + #define ASTNODE_H + ++#include ++ + #include "stp/NodeFactory/HashingNodeFactory.h" + #include "stp/Util/Attributes.h" + #include "ASTInternal.h" +-- +2.35.3 + diff --git a/packages/s/stp/_servicedata b/packages/s/stp/_servicedata index f22ddbf..3355f27 100644 --- a/packages/s/stp/_servicedata +++ b/packages/s/stp/_servicedata @@ -1,4 +1,4 @@ https://github.com/stp/stp - 49a7dac043678680f222827c749a98cd60aed10e \ No newline at end of file + 33b6355fe8b342d00a07f43c238b04a1ff884b2e \ No newline at end of file diff --git a/packages/s/stp/stp-2.3.3+20220722.obscpio b/packages/s/stp/stp-2.3.3+20220722.obscpio deleted file mode 120000 index 97499ef..0000000 --- a/packages/s/stp/stp-2.3.3+20220722.obscpio +++ /dev/null @@ -1 +0,0 @@ -/ipfs/bafybeicx5gvoxut57lvbilvqoeocnag3qmjta2stnmjhmds7youfzdaocm \ No newline at end of file diff --git a/packages/s/stp/stp-2.3.3+20220915.obscpio b/packages/s/stp/stp-2.3.3+20220915.obscpio new file mode 120000 index 0000000..2afe6a4 --- /dev/null +++ b/packages/s/stp/stp-2.3.3+20220915.obscpio @@ -0,0 +1 @@ +/ipfs/bafybeicuowwofr3grutwp3jinsnqh5ucunerqcinp7dhc7c7cojmgxurzy \ No newline at end of file diff --git a/packages/s/stp/stp.changes b/packages/s/stp/stp.changes index 9abd33f..681555f 100644 --- a/packages/s/stp/stp.changes +++ b/packages/s/stp/stp.changes @@ -1,4 +1,51 @@ ------------------------------------------------------------------- +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 - add CMakeLists-use-absolute-libdir-in-rpath-handling.patch diff --git a/packages/s/stp/stp.obsinfo b/packages/s/stp/stp.obsinfo index f251d7f..01be336 100644 --- a/packages/s/stp/stp.obsinfo +++ b/packages/s/stp/stp.obsinfo @@ -1,4 +1,4 @@ name: stp -version: 2.3.3+20220722 -mtime: 1658445181 -commit: e8d153f196dcdf609add70e867f2188d58ffcc97 +version: 2.3.3+20220915 +mtime: 1663164057 +commit: 33b6355fe8b342d00a07f43c238b04a1ff884b2e diff --git a/packages/s/stp/stp.spec b/packages/s/stp/stp.spec index fceb458..93ce925 100644 --- a/packages/s/stp/stp.spec +++ b/packages/s/stp/stp.spec @@ -1,7 +1,7 @@ # # spec file for package stp # -# Copyright (c) 2022 SUSE LLC +# Copyright (c) 2023 SUSE LLC # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -18,7 +18,7 @@ %define sover 2_3 Name: stp -Version: 2.3.3+20220722 +Version: 2.3.3+20220915 Release: 0 Summary: Constraint Solver License: MIT @@ -26,6 +26,7 @@ URL: https://github.com/stp/stp/wiki Source0: %{name}-%{version}.tar.xz Patch0: py3.patch Patch1: CMakeLists-use-absolute-libdir-in-rpath-handling.patch +Patch2: 0001-gcc-13-include-cstdint-for-int-_t.patch BuildRequires: bison BuildRequires: cmake BuildRequires: flex