Remove . from %%cmake invocation to fix FTBFS (rhbz#2060821).
Drop -const-map-key patch now that gcc has been fixed.
This commit is contained in:
parent
32c7ee2a19
commit
c1a05910da
|
@ -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.
|
|
@ -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<const Key, const Data, HashFcn>;
|
|
||||||
+ using HashMap = std::unordered_map<Key, const Data, HashFcn>;
|
|
||||||
/** 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<Key&>(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<Key&>(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<Key&>(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<Key&>(k));
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
14
cvc4.spec
14
cvc4.spec
|
@ -3,7 +3,7 @@
|
||||||
|
|
||||||
Name: cvc4
|
Name: cvc4
|
||||||
Version: 1.8
|
Version: 1.8
|
||||||
Release: 9%{?dist}
|
Release: 10%{?dist}
|
||||||
Summary: Automatic theorem prover for SMT problems
|
Summary: Automatic theorem prover for SMT problems
|
||||||
|
|
||||||
%global jar_version %{version}.0
|
%global jar_version %{version}.0
|
||||||
|
@ -25,14 +25,11 @@ Patch0: %{name}-flags.patch
|
||||||
Patch1: %{name}-cryptominisat.patch
|
Patch1: %{name}-cryptominisat.patch
|
||||||
# Remove duplicate declarations, leads to errors with recent LFSC versions
|
# Remove duplicate declarations, leads to errors with recent LFSC versions
|
||||||
Patch2: %{name}-dup-decl.patch
|
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
|
# 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
|
# speeds. But it has aged, and has less features than ld.bfd. Let's
|
||||||
# use ld.bfd so that package notes work without workarounds.
|
# use ld.bfd so that package notes work without workarounds.
|
||||||
Patch3: %{name}-do-not-use-gold.diff
|
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: abc-devel
|
||||||
BuildRequires: antlr3-C-devel
|
BuildRequires: antlr3-C-devel
|
||||||
|
@ -177,8 +174,7 @@ export CXXFLAGS="$CFLAGS"
|
||||||
-DSYMFPU_DIR:FILEPATH=%{_prefix} \
|
-DSYMFPU_DIR:FILEPATH=%{_prefix} \
|
||||||
-DPYTHON_EXECUTABLE:FILEPATH=%{_bindir}/python%{python3_version} \
|
-DPYTHON_EXECUTABLE:FILEPATH=%{_bindir}/python%{python3_version} \
|
||||||
-DPYTHON_LIBRARY:FILEPATH=$pylib \
|
-DPYTHON_LIBRARY:FILEPATH=$pylib \
|
||||||
-DPYTHON_INCLUDE_DIR:FILEPATH=$pyinc \
|
-DPYTHON_INCLUDE_DIR:FILEPATH=$pyinc
|
||||||
.
|
|
||||||
|
|
||||||
# Tell swig to build for python 3
|
# Tell swig to build for python 3
|
||||||
sed -i 's/swig -python/& -py3/' \
|
sed -i 's/swig -python/& -py3/' \
|
||||||
|
@ -262,6 +258,10 @@ export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
|
||||||
%{python3_sitearch}/pycvc4*
|
%{python3_sitearch}/pycvc4*
|
||||||
|
|
||||||
%changelog
|
%changelog
|
||||||
|
* Fri Mar 4 2022 Jerry James <loganjerry@gmail.com> - 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 <jvanek@redhat.com> - 1.8-9
|
* Sat Feb 05 2022 Jiri Vanek <jvanek@redhat.com> - 1.8-9
|
||||||
- Rebuilt for java-17-openjdk as system jdk
|
- Rebuilt for java-17-openjdk as system jdk
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue