Version 1.8. Drop upstreamed patches: -abc, -swig4, -drat.
This commit is contained in:
parent
9ac0724d02
commit
398dc0c060
@ -1,54 +0,0 @@
|
|||||||
--- cmake/FindABC.cmake.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ cmake/FindABC.cmake 2019-04-16 16:01:44.519958231 -0600
|
|
||||||
@@ -2,7 +2,6 @@
|
|
||||||
# ABC_FOUND - system has ABC lib
|
|
||||||
# ABC_INCLUDE_DIR - the ABC include directory
|
|
||||||
# ABC_LIBRARIES - Libraries needed to use ABC
|
|
||||||
-# ABC_ARCH_FLAGS - Platform specific compile flags
|
|
||||||
|
|
||||||
|
|
||||||
# Check default location of ABC built with contrib/get-abc.
|
|
||||||
@@ -14,28 +13,19 @@ endif()
|
|
||||||
# install rule.
|
|
||||||
find_path(ABC_INCLUDE_DIR
|
|
||||||
NAMES base/abc/abc.h
|
|
||||||
- PATHS ${ABC_HOME}/src
|
|
||||||
+ PATHS /usr/include/abc
|
|
||||||
NO_DEFAULT_PATH)
|
|
||||||
find_library(ABC_LIBRARIES
|
|
||||||
NAMES abc
|
|
||||||
- PATHS ${ABC_HOME}
|
|
||||||
- NO_DEFAULT_PATH)
|
|
||||||
-find_program(ABC_ARCH_FLAGS_PROG
|
|
||||||
- NAMES arch_flags
|
|
||||||
- PATHS ${ABC_HOME}
|
|
||||||
+ PATHS /usr/lib64 /usr/lib
|
|
||||||
NO_DEFAULT_PATH)
|
|
||||||
|
|
||||||
-if(ABC_ARCH_FLAGS_PROG)
|
|
||||||
- execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG}
|
|
||||||
- OUTPUT_VARIABLE ABC_ARCH_FLAGS)
|
|
||||||
-endif()
|
|
||||||
-
|
|
||||||
include(FindPackageHandleStandardArgs)
|
|
||||||
find_package_handle_standard_args(ABC
|
|
||||||
DEFAULT_MSG
|
|
||||||
- ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
|
|
||||||
+ ABC_INCLUDE_DIR ABC_LIBRARIES)
|
|
||||||
|
|
||||||
-mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
|
|
||||||
+mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES)
|
|
||||||
if(ABC_LIBRARIES)
|
|
||||||
message(STATUS "Found ABC libs: ${ABC_LIBRARIES}")
|
|
||||||
endif()
|
|
||||||
--- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ CMakeLists.txt 2019-04-16 15:54:30.334111544 -0600
|
|
||||||
@@ -379,7 +379,7 @@ endif()
|
|
||||||
if(USE_ABC)
|
|
||||||
set(ABC_HOME "${ABC_DIR}")
|
|
||||||
find_package(ABC REQUIRED)
|
|
||||||
- add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
|
|
||||||
+ add_definitions(-DCVC4_USE_ABC)
|
|
||||||
endif()
|
|
||||||
|
|
||||||
if(USE_CADICAL)
|
|
@ -1,8 +1,8 @@
|
|||||||
--- src/prop/cryptominisat.cpp.orig 2019-04-09 10:14:31.000000000 -0600
|
--- src/prop/cryptominisat.cpp.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ src/prop/cryptominisat.cpp 2020-04-26 14:04:26.086833393 -0600
|
+++ src/prop/cryptominisat.cpp 2020-06-21 11:51:21.496211208 -0600
|
||||||
@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
|
@@ -73,15 +73,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
|
||||||
d_okay(true),
|
|
||||||
d_statistics(registry, name)
|
void CryptoMinisatSolver::init()
|
||||||
{
|
{
|
||||||
- d_true = newVar();
|
- d_true = newVar();
|
||||||
- d_false = newVar();
|
- d_false = newVar();
|
||||||
@ -10,15 +10,15 @@
|
|||||||
- std::vector<CMSat::Lit> clause(1);
|
- std::vector<CMSat::Lit> clause(1);
|
||||||
- clause[0] = CMSat::Lit(d_true, false);
|
- clause[0] = CMSat::Lit(d_true, false);
|
||||||
- d_solver->add_clause(clause);
|
- d_solver->add_clause(clause);
|
||||||
-
|
-
|
||||||
- clause[0] = CMSat::Lit(d_false, true);
|
- clause[0] = CMSat::Lit(d_false, true);
|
||||||
- d_solver->add_clause(clause);
|
- d_solver->add_clause(clause);
|
||||||
+ d_true = undefSatVariable;
|
+ d_true = undefSatVariable;
|
||||||
+ d_false = undefSatVariable;
|
+ d_false = undefSatVariable;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
CryptoMinisatSolver::~CryptoMinisatSolver() {}
|
||||||
@@ -154,10 +147,32 @@ SatVariable CryptoMinisatSolver::newVar
|
@@ -158,10 +151,32 @@ SatVariable CryptoMinisatSolver::newVar
|
||||||
}
|
}
|
||||||
|
|
||||||
SatVariable CryptoMinisatSolver::trueVar() {
|
SatVariable CryptoMinisatSolver::trueVar() {
|
||||||
|
@ -1,20 +0,0 @@
|
|||||||
--- proofs/signatures/drat.plf.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ proofs/signatures/drat.plf 2019-09-09 17:42:41.118932870 -0600
|
|
||||||
@@ -322,7 +322,7 @@
|
|
||||||
|
|
||||||
|
|
||||||
; Do unit propagation on `f`, constructing a UP model for it.
|
|
||||||
-(program build_up_model ((f cnf)) clause
|
|
||||||
+(program build_up_model ((f cnf)) UPConstructionResult
|
|
||||||
(match (unit_search f)
|
|
||||||
(USRBottom UPCRBottom)
|
|
||||||
(USRNoUnit (UPCRModel cln))
|
|
||||||
@@ -335,7 +335,7 @@
|
|
||||||
|
|
||||||
; Given some starting assignment (`up_model`), continue UP to construct a larger
|
|
||||||
; model.
|
|
||||||
-(program extend_up_model ((f cnf) (up_model clause)) clause
|
|
||||||
+(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult
|
|
||||||
(do (clause_into_global up_model)
|
|
||||||
(let result (build_up_model f)
|
|
||||||
(do (clause_undo_into_global up_model)
|
|
@ -1,18 +1,16 @@
|
|||||||
--- cmake/ConfigProduction.cmake.orig 2019-04-09 10:14:31.000000000 -0600
|
--- cmake/ConfigProduction.cmake.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ cmake/ConfigProduction.cmake 2020-04-26 17:24:03.338855205 -0600
|
+++ cmake/ConfigProduction.cmake 2020-06-21 11:47:20.134513759 -0600
|
||||||
@@ -1,7 +1,7 @@
|
@@ -1,5 +1,5 @@
|
||||||
-# OPTLEVEL=3
|
-# OPTLEVEL=3
|
||||||
+# OPTLEVEL=2
|
|
||||||
# enable_optimized=yes
|
|
||||||
cvc4_set_option(ENABLE_OPTIMIZED ON)
|
|
||||||
-set(OPTIMIZATION_LEVEL 3)
|
-set(OPTIMIZATION_LEVEL 3)
|
||||||
|
+# OPTLEVEL=2
|
||||||
+set(OPTIMIZATION_LEVEL 2)
|
+set(OPTIMIZATION_LEVEL 2)
|
||||||
# enable_debug_symbols=no
|
# enable_debug_symbols=no
|
||||||
cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
|
cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
|
||||||
# enable_statistics=yes
|
# enable_statistics=yes
|
||||||
--- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600
|
--- CMakeLists.txt.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ CMakeLists.txt 2020-04-26 17:23:30.427884359 -0600
|
+++ CMakeLists.txt 2020-06-21 11:45:03.767689990 -0600
|
||||||
@@ -125,7 +125,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth
|
@@ -175,7 +175,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth
|
||||||
#-----------------------------------------------------------------------------#
|
#-----------------------------------------------------------------------------#
|
||||||
# Internal cmake variables
|
# Internal cmake variables
|
||||||
|
|
||||||
@ -21,9 +19,9 @@
|
|||||||
set(GPL_LIBS "")
|
set(GPL_LIBS "")
|
||||||
|
|
||||||
#-----------------------------------------------------------------------------#
|
#-----------------------------------------------------------------------------#
|
||||||
--- src/parser/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600
|
--- src/parser/CMakeLists.txt.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ src/parser/CMakeLists.txt 2019-04-17 11:21:41.680050119 -0600
|
+++ src/parser/CMakeLists.txt 2020-06-21 11:45:48.007632818 -0600
|
||||||
@@ -81,10 +81,6 @@ foreach(lang Cvc Smt1 Smt2 Tptp)
|
@@ -81,10 +81,6 @@ foreach(lang Cvc Smt2 Tptp)
|
||||||
set_source_files_properties(${gen_src_files} PROPERTIES LANGUAGE CXX)
|
set_source_files_properties(${gen_src_files} PROPERTIES LANGUAGE CXX)
|
||||||
set_source_files_properties(${gen_src_files} PROPERTIES GENERATED TRUE)
|
set_source_files_properties(${gen_src_files} PROPERTIES GENERATED TRUE)
|
||||||
|
|
||||||
@ -34,8 +32,8 @@
|
|||||||
# Add generated source files to the parser source files
|
# Add generated source files to the parser source files
|
||||||
list(APPEND libcvc4parser_src_files ${gen_src_files})
|
list(APPEND libcvc4parser_src_files ${gen_src_files})
|
||||||
endforeach()
|
endforeach()
|
||||||
--- src/prop/bvminisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600
|
--- src/prop/bvminisat/mtl/template.mk.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ src/prop/bvminisat/mtl/template.mk 2019-04-17 11:22:27.662986017 -0600
|
+++ src/prop/bvminisat/mtl/template.mk 2020-06-21 11:46:23.831586522 -0600
|
||||||
@@ -22,7 +22,7 @@ CXX ?= g++
|
@@ -22,7 +22,7 @@ CXX ?= g++
|
||||||
CFLAGS ?= -Wall -Wno-parentheses
|
CFLAGS ?= -Wall -Wno-parentheses
|
||||||
LFLAGS ?= -Wall
|
LFLAGS ?= -Wall
|
||||||
@ -45,8 +43,8 @@
|
|||||||
|
|
||||||
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
|
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
|
||||||
LFLAGS += -lz
|
LFLAGS += -lz
|
||||||
--- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600
|
--- src/prop/minisat/mtl/template.mk.orig 2020-06-19 10:59:27.000000000 -0600
|
||||||
+++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600
|
+++ src/prop/minisat/mtl/template.mk 2020-06-21 11:46:37.670568635 -0600
|
||||||
@@ -22,7 +22,7 @@ CXX ?= g++
|
@@ -22,7 +22,7 @@ CXX ?= g++
|
||||||
CFLAGS ?= -Wall -Wno-parentheses
|
CFLAGS ?= -Wall -Wno-parentheses
|
||||||
LFLAGS ?= -Wall
|
LFLAGS ?= -Wall
|
||||||
|
@ -1,44 +0,0 @@
|
|||||||
--- src/bindings/java/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ src/bindings/java/CMakeLists.txt 2019-06-06 11:58:39.836849929 -0600
|
|
||||||
@@ -131,6 +131,7 @@ set(gen_java_files
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
|
|
||||||
+ ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/Options.java
|
|
||||||
@@ -177,7 +178,6 @@ set(gen_java_files
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
|
|
||||||
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
|
|
||||||
@@ -204,12 +204,12 @@ set(gen_java_files
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/StringType.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java
|
|
||||||
- ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
|
|
||||||
+ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
|
|
||||||
${CMAKE_CURRENT_BINARY_DIR}/Timer.java
|
|
||||||
--- src/smt/smt_engine.i.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ src/smt/smt_engine.i 2019-06-06 11:24:53.214450924 -0600
|
|
||||||
@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acs
|
|
||||||
swigCPtr = 0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
+
|
|
||||||
+%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
|
|
||||||
+
|
|
||||||
#endif // SWIGJAVA
|
|
||||||
|
|
||||||
%ignore CVC4::SmtEngine::setLogic(const char*);
|
|
122
cvc4.spec
122
cvc4.spec
@ -2,8 +2,8 @@
|
|||||||
# we currently build without glpk support.
|
# we currently build without glpk support.
|
||||||
|
|
||||||
Name: cvc4
|
Name: cvc4
|
||||||
Version: 1.7
|
Version: 1.8
|
||||||
Release: 15%{?dist}
|
Release: 1%{?dist}
|
||||||
Summary: Automatic theorem prover for SMT problems
|
Summary: Automatic theorem prover for SMT problems
|
||||||
|
|
||||||
# License breakdown:
|
# License breakdown:
|
||||||
@ -17,17 +17,10 @@ Summary: Automatic theorem prover for SMT problems
|
|||||||
License: Boost and BSD and MIT
|
License: Boost and BSD and MIT
|
||||||
URL: http://cvc4.cs.stanford.edu/
|
URL: http://cvc4.cs.stanford.edu/
|
||||||
Source0: https://github.com/CVC4/CVC4/archive/%{version}/%{name}-%{version}.tar.gz
|
Source0: https://github.com/CVC4/CVC4/archive/%{version}/%{name}-%{version}.tar.gz
|
||||||
# Fix detection of ABC
|
|
||||||
Patch0: %{name}-abc.patch
|
|
||||||
# Do not override Fedora flags
|
# Do not override Fedora flags
|
||||||
Patch1: %{name}-flags.patch
|
Patch0: %{name}-flags.patch
|
||||||
# Adapt to swig 4
|
|
||||||
Patch2: %{name}-swig4.patch
|
|
||||||
# Fix drat signature wrt side condition return types
|
|
||||||
# https://github.com/CVC4/CVC4/commit/57524fd9f204f8e85e5e37af1444a6f76d809aee
|
|
||||||
Patch3: %{name}-drat.patch
|
|
||||||
# Adapt to cryptominisat 5.7
|
# Adapt to cryptominisat 5.7
|
||||||
Patch4: %{name}-cryptominisat.patch
|
Patch1: %{name}-cryptominisat.patch
|
||||||
|
|
||||||
BuildRequires: abc-devel
|
BuildRequires: abc-devel
|
||||||
BuildRequires: antlr3-C-devel
|
BuildRequires: antlr3-C-devel
|
||||||
@ -35,28 +28,28 @@ BuildRequires: antlr3-tool
|
|||||||
BuildRequires: boost-devel
|
BuildRequires: boost-devel
|
||||||
BuildRequires: cadical-devel
|
BuildRequires: cadical-devel
|
||||||
BuildRequires: cmake
|
BuildRequires: cmake
|
||||||
BuildRequires: cryptominisat-devel
|
BuildRequires: cmake(cryptominisat5)
|
||||||
BuildRequires: cxxtest
|
BuildRequires: cxxtest
|
||||||
BuildRequires: drat2er-devel
|
BuildRequires: drat2er-devel
|
||||||
|
BuildRequires: drat-trim-devel
|
||||||
BuildRequires: gcc-c++
|
BuildRequires: gcc-c++
|
||||||
BuildRequires: ghostscript
|
BuildRequires: ghostscript
|
||||||
BuildRequires: gmp-devel
|
BuildRequires: gmp-devel
|
||||||
BuildRequires: java-devel
|
BuildRequires: java-devel
|
||||||
BuildRequires: jpackage-utils
|
BuildRequires: javapackages-tools
|
||||||
|
BuildRequires: kissat-devel
|
||||||
BuildRequires: lfsc-devel
|
BuildRequires: lfsc-devel
|
||||||
BuildRequires: libtool
|
BuildRequires: libtool
|
||||||
BuildRequires: perl-interpreter
|
BuildRequires: perl-interpreter
|
||||||
|
BuildRequires: pkgconfig(readline)
|
||||||
BuildRequires: python3-devel
|
BuildRequires: python3-devel
|
||||||
BuildRequires: readline-devel
|
BuildRequires: %{py3_dist cython}
|
||||||
|
BuildRequires: %{py3_dist toml}
|
||||||
BuildRequires: swig
|
BuildRequires: swig
|
||||||
BuildRequires: symfpu-devel
|
BuildRequires: symfpu-devel
|
||||||
|
|
||||||
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
# This can be removed when Fedora 30 reaches EOL
|
|
||||||
Obsoletes: %{name}-doc < 1.7
|
|
||||||
Provides: %{name}-doc = %{version}-%{release}
|
|
||||||
|
|
||||||
%description
|
%description
|
||||||
CVC4 is an efficient open-source automatic theorem prover for
|
CVC4 is an efficient open-source automatic theorem prover for
|
||||||
satisfiability modulo theories (SMT) problems. It can be used to prove
|
satisfiability modulo theories (SMT) problems. It can be used to prove
|
||||||
@ -92,7 +85,7 @@ SMT problems.
|
|||||||
Summary: Java interface to %{name}
|
Summary: Java interface to %{name}
|
||||||
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
Requires: java-headless
|
Requires: java-headless
|
||||||
Requires: jpackage-utils
|
Requires: javapackages-tools
|
||||||
|
|
||||||
%description java
|
%description java
|
||||||
Java interface to %{name}.
|
Java interface to %{name}.
|
||||||
@ -107,6 +100,12 @@ Python 3 interface to %{name}.
|
|||||||
%prep
|
%prep
|
||||||
%autosetup -p0 -n CVC4-%{version}
|
%autosetup -p0 -n CVC4-%{version}
|
||||||
|
|
||||||
|
# Adapt to way kissat is packaged for Fedora
|
||||||
|
sed -i 's,#include <kissat/kissat\.h>,#include <kissat.h>,' src/prop/kissat.h
|
||||||
|
|
||||||
|
# We want to know about use of deprecated interfaces
|
||||||
|
sed -i '/Wno-deprecated/d' CMakeLists.txt
|
||||||
|
|
||||||
# The Java interface uses type punning
|
# The Java interface uses type punning
|
||||||
sed -i '/include_directories/aadd_compile_options("-fno-strict-aliasing")' \
|
sed -i '/include_directories/aadd_compile_options("-fno-strict-aliasing")' \
|
||||||
src/bindings/java/CMakeLists.txt
|
src/bindings/java/CMakeLists.txt
|
||||||
@ -116,12 +115,13 @@ sed -i 's/\${CMAKE_INSTALL_PREFIX}/\\$ENV{DESTDIR}&/' src/CMakeLists.txt
|
|||||||
|
|
||||||
# Fix installation directory on 64-bit arches
|
# Fix installation directory on 64-bit arches
|
||||||
if [ "%{_lib}" = "lib64" ]; then
|
if [ "%{_lib}" = "lib64" ]; then
|
||||||
sed -i 's/DESTINATION lib/&64/' src/CMakeLists.txt src/parser/CMakeLists.txt
|
sed -i 's/LIBRARY_INSTALL_DIR lib/&64/' CMakeLists.txt
|
||||||
fi
|
fi
|
||||||
|
|
||||||
# Python extensions should not link against libpython; see
|
# Python extensions should not link against libpython; see
|
||||||
# https://github.com/python/cpython/pull/12946
|
# https://github.com/python/cpython/pull/12946
|
||||||
sed -i 's/ \${PYTHON_LIBRARIES}//' src/bindings/python/CMakeLists.txt
|
sed -i 's/ \${PYTHON_LIBRARIES}//' src/bindings/python/CMakeLists.txt \
|
||||||
|
src/api/python/CMakeLists.txt
|
||||||
|
|
||||||
# One test exhausts all memory on 32-bit platforms; skip it
|
# One test exhausts all memory on 32-bit platforms; skip it
|
||||||
%ifarch %{arm} %{ix86}
|
%ifarch %{arm} %{ix86}
|
||||||
@ -134,32 +134,32 @@ pylib=$(ls -1 %{_libdir}/libpython3.*.so)
|
|||||||
export CFLAGS="%{optflags} -fsigned-char -DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
|
export CFLAGS="%{optflags} -fsigned-char -DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
|
||||||
export CXXFLAGS="$CFLAGS"
|
export CXXFLAGS="$CFLAGS"
|
||||||
%cmake \
|
%cmake \
|
||||||
-DCMAKE_SKIP_RPATH:BOOL=YES \
|
|
||||||
-DCMAKE_SKIP_INSTALL_RPATH:BOOL=YES \
|
|
||||||
-DBUILD_BINDINGS_JAVA:BOOL=ON \
|
|
||||||
-DBUILD_BINDINGS_PYTHON:BOOL=ON \
|
-DBUILD_BINDINGS_PYTHON:BOOL=ON \
|
||||||
|
-DBUILD_SWIG_BINDINGS_JAVA:BOOL=ON \
|
||||||
|
-DBUILD_SWIG_BINDINGS_PYTHON:BOOL=ON \
|
||||||
|
-DCMAKE_JAVA_COMPILE_FLAGS:STRING="-source;1.8;-target;1.8" \
|
||||||
-DENABLE_GPL:BOOL=ON \
|
-DENABLE_GPL:BOOL=ON \
|
||||||
-DENABLE_OPTIMIZED:STRING=ON \
|
-DENABLE_OPTIMIZED:BOOL=ON \
|
||||||
-DENABLE_PORTFOLIO:STRING=ON \
|
-DENABLE_PORTFOLIO:BOOL=ON \
|
||||||
-DENABLE_PROOFS:STRING=ON \
|
-DENABLE_PROOFS:BOOL=ON \
|
||||||
-DENABLE_SHARED:STRING=ON \
|
-DENABLE_SHARED:BOOL=ON \
|
||||||
-DUSE_ABC:STRING=ON \
|
-DUSE_ABC:BOOL=ON \
|
||||||
-DABC_DIR:STRING=%{_prefix} \
|
-DABC_ARCH_FLAGS:FILEPATH="-I%{_includedir}/abc" \
|
||||||
-DUSE_CADICAL:BOOL=ON \
|
-DUSE_CADICAL:BOOL=ON \
|
||||||
-DCADICAL_DIR:STRING=%{_prefix} \
|
|
||||||
-DUSE_CRYPTOMINISAT:BOOL=ON \
|
-DUSE_CRYPTOMINISAT:BOOL=ON \
|
||||||
-DCRYPTOMINISAT_DIR:STRING=%{_prefix} \
|
-DCryptoMiniSat_INCLUDE_DIR:FILEPATH=%{_includedir}/cryptominisat5 \
|
||||||
-DUSE_DRAT2ER:BOOL=ON \
|
-DUSE_DRAT2ER:BOOL=ON \
|
||||||
-DDRAT2ER_DIR:STRING=%{_prefix} \
|
-DDrat2Er_INCLUDE_DIR:FILEPATH=%{_includedir} \
|
||||||
-DDrat2Er_INCLUDE_DIR:STRING=%{_includedir}/drat2er \
|
|
||||||
-DDrat2Er_LIBRARIES:STRING=-ldrat2er \
|
-DDrat2Er_LIBRARIES:STRING=-ldrat2er \
|
||||||
-DDratTrim_LIBRARIES:STRING=-ldrat2er \
|
-DDratTrim_LIBRARIES:STRING=-ldrat-trim \
|
||||||
|
-DUSE_KISSAT:BOOL=ON \
|
||||||
|
-DKissat_INCLUDE_DIR:FILEPATH=%{_includedir} \
|
||||||
|
-DKissat_LIBRARIES:STRING=-lkissat \
|
||||||
-DUSE_LFSC:BOOL=ON \
|
-DUSE_LFSC:BOOL=ON \
|
||||||
-DLFSC_DIR:STRING=%{_prefix} \
|
|
||||||
-DUSE_PYTHON3:BOOL=ON \
|
-DUSE_PYTHON3:BOOL=ON \
|
||||||
-DUSE_READLINE:STRING=ON \
|
-DUSE_READLINE:BOOL=ON \
|
||||||
-DUSE_SYMFPU:BOOL=ON \
|
-DUSE_SYMFPU:BOOL=ON \
|
||||||
-DSYMFPU_DIR:STRING=%{_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 \
|
||||||
@ -167,19 +167,32 @@ export CXXFLAGS="$CFLAGS"
|
|||||||
|
|
||||||
# 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/' \
|
||||||
src/bindings/python/CMakeFiles/CVC4_swig_compilation.dir/build.make
|
%{__cmake_builddir}/src/bindings/python/CMakeFiles/CVC4_swig_compilation.dir/build.make
|
||||||
|
|
||||||
make %{?_smp_mflags}
|
%cmake_build
|
||||||
make doc
|
make doc
|
||||||
|
|
||||||
%install
|
%install
|
||||||
%make_install
|
# The Python API install target ignores DESTDIR, so force the issue.
|
||||||
|
sed -e 's,"%{_prefix}","%{buildroot}%{_prefix}",g' \
|
||||||
|
-e 's,--prefix=%{_prefix},--prefix=%{buildroot}%{_prefix},' \
|
||||||
|
-i %{__cmake_builddir}/src/api/python/cmake_install.cmake
|
||||||
|
|
||||||
# BUG: CVC4 1.7 does not install the Java interface
|
%cmake_install
|
||||||
mkdir -p %{buildroot}%{_javadir}
|
|
||||||
cp -p src/bindings/java/CVC4.jar %{buildroot}%{_javadir}
|
# Link the JNI interface to where Fedora mandates it should go
|
||||||
mkdir -p %{buildroot}%{_jnidir}/%{name}
|
mkdir -p %{buildroot}%{_jnidir}/%{name}
|
||||||
cp -p src/bindings/java/libcvc4jni.so %{buildroot}%{_jnidir}/%{name}
|
ln -s ../../%{_lib}/libcvc4jni.so %{buildroot}%{_jnidir}/%{name}
|
||||||
|
|
||||||
|
# Fix a symlink that points to the build directory
|
||||||
|
rm %{buildroot}%{_javadir}/%{name}/CVC4.jar
|
||||||
|
ln -s CVC4-%{version}.jar %{buildroot}%{_javadir}/%{name}/CVC4.jar
|
||||||
|
|
||||||
|
# The cython interface is installed into the wrong directory
|
||||||
|
if [ "%{python3_sitelib}" != "%{python3_sitearch}" ]; then
|
||||||
|
mv %{buildroot}%{python3_sitelib}/pycvc4* %{buildroot}%{python3_sitearch}
|
||||||
|
rm -fr %{buildroot}%{prefix}/lib/python3*
|
||||||
|
fi
|
||||||
|
|
||||||
%check
|
%check
|
||||||
# The tests use a large amount of stack space.
|
# The tests use a large amount of stack space.
|
||||||
@ -194,38 +207,43 @@ sed 's,loadLibrary("cvc4jni"),load("%{buildroot}%{_jnidir}/%{name}/libcvc4jni.so
|
|||||||
|
|
||||||
export LC_ALL=C.UTF-8
|
export LC_ALL=C.UTF-8
|
||||||
export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
|
export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
|
||||||
make check
|
%cmake_build --target check
|
||||||
|
|
||||||
%files
|
%files
|
||||||
%doc AUTHORS NEWS README.md THANKS
|
%doc AUTHORS NEWS README.md THANKS
|
||||||
%{_bindir}/%{name}
|
%{_bindir}/%{name}
|
||||||
%{_bindir}/p%{name}
|
|
||||||
%{_datadir}/%{name}/
|
%{_datadir}/%{name}/
|
||||||
%{_mandir}/man1/%{name}.1*
|
%{_mandir}/man1/%{name}.1*
|
||||||
%{_mandir}/man1/p%{name}.1*
|
|
||||||
%{_mandir}/man5/%{name}.5*
|
%{_mandir}/man5/%{name}.5*
|
||||||
|
|
||||||
%files libs
|
%files libs
|
||||||
%license COPYING licenses/channel.h-LICENSE
|
%license COPYING
|
||||||
%{_libdir}/lib%{name}.so.6
|
%{_libdir}/lib%{name}.so.7
|
||||||
%{_libdir}/lib%{name}parser.so.6
|
%{_libdir}/lib%{name}parser.so.7
|
||||||
|
|
||||||
%files devel
|
%files devel
|
||||||
%{_includedir}/%{name}/
|
%{_includedir}/%{name}/
|
||||||
%{_libdir}/lib%{name}.so
|
%{_libdir}/lib%{name}.so
|
||||||
%{_libdir}/lib%{name}parser.so
|
%{_libdir}/lib%{name}parser.so
|
||||||
|
%{_libdir}/cmake/CVC4/
|
||||||
%{_mandir}/man3/*
|
%{_mandir}/man3/*
|
||||||
|
|
||||||
%files java
|
%files java
|
||||||
%{_javadir}/CVC4.jar
|
%{_javadir}/%{name}/
|
||||||
%{_jnidir}/%{name}/
|
%{_jnidir}/%{name}/
|
||||||
|
%{_libdir}/libcvc4jni.so
|
||||||
|
|
||||||
%files python3
|
%files python3
|
||||||
%{python3_sitearch}/CVC4.py
|
%{python3_sitearch}/CVC4.py
|
||||||
%{python3_sitearch}/_CVC4.so
|
%{python3_sitearch}/_CVC4.so
|
||||||
%{python3_sitearch}/__pycache__/CVC4.*
|
%{python3_sitearch}/__pycache__/CVC4.*
|
||||||
|
%{python3_sitearch}/pycvc4*
|
||||||
|
|
||||||
%changelog
|
%changelog
|
||||||
|
* Mon Aug 3 2020 Jerry James <loganjerry@gmail.com> - 1.8-1
|
||||||
|
- Version 1.8
|
||||||
|
- Drop upstreamed patches: -abc, -swig4, -drat
|
||||||
|
|
||||||
* Sat Aug 01 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.7-15
|
* Sat Aug 01 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.7-15
|
||||||
- Second attempt - Rebuilt for
|
- Second attempt - Rebuilt for
|
||||||
https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
|
https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
|
||||||
|
2
sources
2
sources
@ -1 +1 @@
|
|||||||
SHA512 (cvc4-1.7.tar.gz) = b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6
|
SHA512 (cvc4-1.8.tar.gz) = 19e318a62f0a6dfeea4db5225b150550f1e7afcf42a3547bad1ff2030aca7a7713fe29e7059f2dc391eaa18b0cd4183f99ab2dca5008979cb8881b46b8dc01f2
|
||||||
|
Loading…
Reference in New Issue
Block a user