diff --git a/README.md b/README.md new file mode 100644 index 0000000..7b7d019 --- /dev/null +++ b/README.md @@ -0,0 +1,17 @@ +# cvc4 + +[CVC4](https://cvc4.github.io/) is an efficient open-source automatic theorem +prover for satisfiability modulo theories (SMT) problems. It can be used to +prove the validity (or, dually, the satisfiability) of first-order formulas in +a large number of built-in logical theories and their combination. + +CVC4 is the fourth in the Cooperating Validity Checker family of tools (CVC, +CVC Lite, CVC3) but does not directly incorporate code from any previous +version. A joint project of NYU and U Iowa, CVC4 aims to support the features +of CVC3 and SMT-LIBv2 while optimizing the design of the core system +architecture and decision procedures to take advantage of recent engineering +and algorithmic advances. + +CVC4 is intended to be an open and extensible SMT engine, and it can be used +as a stand-alone tool or as a library, with essentially no limit on its use +for research or commercial purposes. diff --git a/cvc4-const-map-key.patch b/cvc4-const-map-key.patch deleted file mode 100644 index ad64595..0000000 --- a/cvc4-const-map-key.patch +++ /dev/null @@ -1,47 +0,0 @@ ---- src/context/cdinsert_hashmap.h.orig 2020-06-19 10:59:27.000000000 -0600 -+++ src/context/cdinsert_hashmap.h 2022-01-22 15:49:35.129038124 -0700 -@@ -57,7 +57,7 @@ private: - /** A list of the keys in the map maintained as a stack. */ - KeyVec d_keys; - -- using HashMap = std::unordered_map; -+ using HashMap = std::unordered_map; - /** The hash_map used for element lookup. */ - HashMap d_hashMap; - -@@ -95,7 +95,7 @@ public: - * See hash_map::find() - */ - const_iterator find(const Key& k) const{ -- return d_hashMap.find(k); -+ return d_hashMap.find(const_cast(k)); - } - - /** Returns an iterator to the start of the set of keys. */ -@@ -114,7 +114,7 @@ public: - - /** Returns true if k is a mapped key. */ - bool contains(const Key& k) const { -- return find(k) != end(); -+ return find(const_cast(k)) != end(); - } - - /** -@@ -122,7 +122,7 @@ public: - * This must succeed. - */ - const Data& operator[](const Key& k) const { -- const_iterator ci = find(k); -+ const_iterator ci = find(const_cast(k)); - Assert(ci != end()); - return (*ci).second; - } -@@ -361,7 +361,7 @@ public: - * the context. - */ - const_iterator find(const Key& k) const { -- return d_insertMap->find(k); -+ return d_insertMap->find(const_cast(k)); - } - - /** diff --git a/cvc4.spec b/cvc4.spec index 957f915..0fca438 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -3,7 +3,7 @@ Name: cvc4 Version: 1.8 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Automatic theorem prover for SMT problems %global jar_version %{version}.0 @@ -25,14 +25,11 @@ Patch0: %{name}-flags.patch Patch1: %{name}-cryptominisat.patch # Remove duplicate declarations, leads to errors with recent LFSC versions Patch2: %{name}-dup-decl.patch -# Just use the default linker specied by the distro. ld.gold was the +# Just use the default linker specified by the distro. ld.gold was the # new kid on the block a while ago, primarily offering higher link # speeds. But it has aged, and has less features than ld.bfd. Let's # use ld.bfd so that package notes work without workarounds. Patch3: %{name}-do-not-use-gold.diff -# Change map keys from const to non-const -# https://bugzilla.redhat.com/show_bug.cgi?id=2043767 -Patch4: %{name}-const-map-key.patch BuildRequires: abc-devel BuildRequires: antlr3-C-devel @@ -177,8 +174,7 @@ export CXXFLAGS="$CFLAGS" -DSYMFPU_DIR:FILEPATH=%{_prefix} \ -DPYTHON_EXECUTABLE:FILEPATH=%{_bindir}/python%{python3_version} \ -DPYTHON_LIBRARY:FILEPATH=$pylib \ - -DPYTHON_INCLUDE_DIR:FILEPATH=$pyinc \ - . + -DPYTHON_INCLUDE_DIR:FILEPATH=$pyinc # Tell swig to build for python 3 sed -i 's/swig -python/& -py3/' \ @@ -262,6 +258,10 @@ export LD_LIBRARY_PATH=%{buildroot}%{_libdir} %{python3_sitearch}/pycvc4* %changelog +* Fri Mar 4 2022 Jerry James - 1.8-10 +- Remove . from %%cmake invocation to fix FTBFS (rhbz#2060821) +- Drop -const-map-key patch now that gcc has been fixed + * Sat Feb 05 2022 Jiri Vanek - 1.8-9 - Rebuilt for java-17-openjdk as system jdk