From eb73525431098824c2187b23f54a808ff567857f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 26 Apr 2020 17:26:14 -0600 Subject: [PATCH] Add -cryptominisat patch to adapt to changes in 5.7.0. --- cvc4-cryptominisat.patch | 53 ++++++++++++++++++++++++++++++ cvc4-flags.patch | 69 ++++++++++++++++++++++++++++++++++++++-- cvc4.spec | 3 ++ 3 files changed, 123 insertions(+), 2 deletions(-) create mode 100644 cvc4-cryptominisat.patch diff --git a/cvc4-cryptominisat.patch b/cvc4-cryptominisat.patch new file mode 100644 index 0000000..33b43d5 --- /dev/null +++ b/cvc4-cryptominisat.patch @@ -0,0 +1,53 @@ +--- src/prop/cryptominisat.cpp.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/prop/cryptominisat.cpp 2020-04-26 14:04:26.086833393 -0600 +@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver + d_okay(true), + d_statistics(registry, name) + { +- d_true = newVar(); +- d_false = newVar(); +- +- std::vector clause(1); +- clause[0] = CMSat::Lit(d_true, false); +- d_solver->add_clause(clause); +- +- clause[0] = CMSat::Lit(d_false, true); +- d_solver->add_clause(clause); ++ d_true = undefSatVariable; ++ d_false = undefSatVariable; + } + + +@@ -154,10 +147,32 @@ SatVariable CryptoMinisatSolver::newVar + } + + SatVariable CryptoMinisatSolver::trueVar() { ++ if (d_true == undefSatVariable) { ++ d_true = newVar(); ++ d_false = newVar(); ++ ++ std::vector clause(1); ++ clause[0] = CMSat::Lit(d_true, false); ++ d_solver->add_clause(clause); ++ ++ clause[0] = CMSat::Lit(d_false, true); ++ d_solver->add_clause(clause); ++ } + return d_true; + } + + SatVariable CryptoMinisatSolver::falseVar() { ++ if (d_true == undefSatVariable) { ++ d_true = newVar(); ++ d_false = newVar(); ++ ++ std::vector clause(1); ++ clause[0] = CMSat::Lit(d_true, false); ++ d_solver->add_clause(clause); ++ ++ clause[0] = CMSat::Lit(d_false, true); ++ d_solver->add_clause(clause); ++ } + return d_false; + } + diff --git a/cvc4-flags.patch b/cvc4-flags.patch index 5a8e62d..4793ace 100644 --- a/cvc4-flags.patch +++ b/cvc4-flags.patch @@ -1,5 +1,17 @@ ---- CMakeLists.txt.orig 2019-04-16 15:54:30.334111544 -0600 -+++ CMakeLists.txt 2019-04-17 11:23:52.404867885 -0600 +--- cmake/ConfigProduction.cmake.orig 2019-04-09 10:14:31.000000000 -0600 ++++ cmake/ConfigProduction.cmake 2020-04-26 17:24:03.338855205 -0600 +@@ -1,7 +1,7 @@ +-# OPTLEVEL=3 ++# OPTLEVEL=2 + # enable_optimized=yes + cvc4_set_option(ENABLE_OPTIMIZED ON) +-set(OPTIMIZATION_LEVEL 3) ++set(OPTIMIZATION_LEVEL 2) + # enable_debug_symbols=no + cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) + # enable_statistics=yes +--- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 ++++ CMakeLists.txt 2020-04-26 17:23:30.427884359 -0600 @@ -125,7 +125,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth #-----------------------------------------------------------------------------# # Internal cmake variables @@ -33,6 +45,59 @@ CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS LFLAGS += -lz +--- src/prop/cryptominisat.cpp.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/prop/cryptominisat.cpp 2020-04-26 14:04:26.086833393 -0600 +@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver + d_okay(true), + d_statistics(registry, name) + { +- d_true = newVar(); +- d_false = newVar(); +- +- std::vector clause(1); +- clause[0] = CMSat::Lit(d_true, false); +- d_solver->add_clause(clause); +- +- clause[0] = CMSat::Lit(d_false, true); +- d_solver->add_clause(clause); ++ d_true = undefSatVariable; ++ d_false = undefSatVariable; + } + + +@@ -154,10 +147,32 @@ SatVariable CryptoMinisatSolver::newVar + } + + SatVariable CryptoMinisatSolver::trueVar() { ++ if (d_true == undefSatVariable) { ++ d_true = newVar(); ++ d_false = newVar(); ++ ++ std::vector clause(1); ++ clause[0] = CMSat::Lit(d_true, false); ++ d_solver->add_clause(clause); ++ ++ clause[0] = CMSat::Lit(d_false, true); ++ d_solver->add_clause(clause); ++ } + return d_true; + } + + SatVariable CryptoMinisatSolver::falseVar() { ++ if (d_true == undefSatVariable) { ++ d_true = newVar(); ++ d_false = newVar(); ++ ++ std::vector clause(1); ++ clause[0] = CMSat::Lit(d_true, false); ++ d_solver->add_clause(clause); ++ ++ clause[0] = CMSat::Lit(d_false, true); ++ d_solver->add_clause(clause); ++ } + return d_false; + } + --- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600 +++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600 @@ -22,7 +22,7 @@ CXX ?= g++ diff --git a/cvc4.spec b/cvc4.spec index 295ddd7..c0b3a63 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -26,6 +26,8 @@ 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 +Patch4: %{name}-cryptominisat.patch BuildRequires: abc-devel BuildRequires: antlr3-C-devel @@ -222,6 +224,7 @@ make check %changelog * Sat Apr 25 2020 Jerry James - 1.7-9 - Rebuild for cryptominisat 5.7.0 +- Add -cryptominisat patch to adapt to changes in 5.7.0 * Tue Jan 28 2020 Fedora Release Engineering - 1.7-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild