[glueminisat] Update to release 2.2.7 from upstream.

jcp jcp at fedoraproject.org
Tue Aug 13 21:25:47 UTC 2013


commit 8f85c957805e57b8d5c6508dc3dc60a98166c712
Author: John C. Peterson <jcp at eskimo.com>
Date:   Tue Aug 13 14:24:48 2013 -0700

    Update to release 2.2.7 from upstream.

 .gitignore               |    1 +
 glueminisat-FPU.patch    |   24 +++---
 glueminisat-printf.patch |  211 ++++++++++++++++++++++-----------------------
 glueminisat.spec         |   90 +++++++++++++++-----
 sources                  |    2 +-
 5 files changed, 184 insertions(+), 144 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index f1debb8..583dab7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /glueminisat-2.2.5.tar.gz
+/glueminisat-2.2.7.tar.gz
diff --git a/glueminisat-FPU.patch b/glueminisat-FPU.patch
index 1926761..d1b139c 100644
--- a/glueminisat-FPU.patch
+++ b/glueminisat-FPU.patch
@@ -1,22 +1,22 @@
-diff -uNr glueminisat-2.2.5.orig/core/Main.cc glueminisat-2.2.5/core/Main.cc
---- glueminisat-2.2.5.orig/core/Main.cc	2011-03-02 00:24:12.000000000 -0800
-+++ glueminisat-2.2.5/core/Main.cc	2012-04-24 09:55:10.845923073 -0700
-@@ -80,7 +80,7 @@
- 		setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
+diff -uNr glueminisat-2.2.7.orig/code/core/Main.cc glueminisat-2.2.7/code/core/Main.cc
+--- glueminisat-2.2.7.orig/code/core/Main.cc	2013-04-30 00:02:26.000000000 -0700
++++ glueminisat-2.2.7/code/core/Main.cc	2013-07-05 20:54:54.783981465 -0700
+@@ -82,7 +82,7 @@
+         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
          // printf("This is MiniSat 2.0 beta\n");
-         
+ 
 -#if defined(__linux__)
 +#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
          fpu_control_t oldcw, newcw;
          _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
          printf("WARNING: for repeatability, setting FPU to use double precision\n");
-diff -uNr glueminisat-2.2.5.orig/simp/Main.cc glueminisat-2.2.5/simp/Main.cc
---- glueminisat-2.2.5.orig/simp/Main.cc	2011-03-02 00:57:40.000000000 -0800
-+++ glueminisat-2.2.5/simp/Main.cc	2012-04-24 09:53:34.629957638 -0700
-@@ -80,7 +80,7 @@
- 		setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
+diff -uNr glueminisat-2.2.7.orig/code/simp/Main.cc glueminisat-2.2.7/code/simp/Main.cc
+--- glueminisat-2.2.7.orig/code/simp/Main.cc	2013-04-30 00:02:26.000000000 -0700
++++ glueminisat-2.2.7/code/simp/Main.cc	2013-07-05 20:54:54.783981465 -0700
+@@ -82,7 +82,7 @@
+         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
          // printf("This is MiniSat 2.0 beta\n");
-         
+ 
 -#if defined(__linux__)
 +#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
          fpu_control_t oldcw, newcw;
diff --git a/glueminisat-printf.patch b/glueminisat-printf.patch
index cc60917..7aff606 100644
--- a/glueminisat-printf.patch
+++ b/glueminisat-printf.patch
@@ -1,188 +1,183 @@
-diff -uNr glueminisat-2.2.5.orig/core/Main.cc glueminisat-2.2.5/core/Main.cc
---- glueminisat-2.2.5.orig/core/Main.cc	2011-03-02 00:24:12.000000000 -0800
-+++ glueminisat-2.2.5/core/Main.cc	2012-04-24 10:15:41.887958169 -0700
-@@ -146,21 +146,21 @@
+diff -uNr glueminisat-2.2.7.orig/code/core/Main.cc glueminisat-2.2.7/code/core/Main.cc
+--- glueminisat-2.2.7.orig/code/core/Main.cc	2013-04-30 00:02:26.000000000 -0700
++++ glueminisat-2.2.7/code/core/Main.cc	2013-07-05 20:56:20.143637420 -0700
+@@ -151,8 +151,8 @@
              printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
-         
+ 
          if (S.verbosity > 0){
--            printf("===============================[ Problem Statistics ]===============================\n");
--            printf("|                                                                                  |\n"); }
+-            printf("=============================[ Problem Statistics ]==============================\n");
+-            printf("|                                                                               |\n"); }
 +            printf("=============================[ Problem Statistics ]=============================\n");
-+            printf("|                                                                          |\n"); }
-         
-         parse_DIMACS(in, S);
-         gzclose(in);
-         FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
-         
++            printf("|                                                                              |\n"); }
+ 
+         // added by nabesima
+         S.output = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+@@ -162,13 +162,13 @@
+         // FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+ 
          if (S.verbosity > 0){
--            printf("|  Number of variables:  %12d                                              |\n", S.nVars());
--            printf("|  Number of clauses:    %12d                                              |\n", S.nClauses()); }
-+            printf("|  Number of variables:  %12d                                      |\n", S.nVars());
-+            printf("|  Number of clauses:    %12d                                      |\n", S.nClauses()); }
-         
+-            printf("|  Number of variables:  %12d                                           |\n", S.nVars());
+-            printf("|  Number of clauses:    %12d                                           |\n", S.nClauses()); }
++            printf("|  Number of variables:  %12d                                          |\n", S.nVars());
++            printf("|  Number of clauses:    %12d                                          |\n", S.nClauses()); }
+ 
          double parsed_time = cpuTime();
          if (S.verbosity > 0){
--            printf("|  Parse time:           %12.2f s                                            |\n", parsed_time - initial_time);
--            printf("|                                                                                  |\n"); }
-+            printf("|  Parse time:           %12.4f s                                    |\n", parsed_time - initial_time);
-+            printf("|                                                                          |\n"); }
-  
+-            printf("|  Parse time:           %12.2f s                                         |\n", parsed_time - initial_time);
+-            printf("|                                                                               |\n"); }
++            printf("|  Parse time:           %12.4f s                                        |\n", parsed_time - initial_time);
++            printf("|                                                                              |\n"); }
+ 
          // Change to signal-handlers that will only notify the solver and allow it to terminate
          // voluntarily:
-@@ -170,7 +170,7 @@
-         if (!S.simplify()){
-             if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+@@ -180,7 +180,7 @@
+             //if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+             if (S.output != NULL) fprintf(S.output, "0\n"), fclose(S.output);
              if (S.verbosity > 0){
--                printf("=============================================================================\n");
+-                printf("==========================================================================\n");
 +                printf("================================================================================\n");
                  printf("Solved by unit propagation\n");
                  printStats(S);
                  printf("\n"); }
-@@ -214,7 +214,7 @@
+@@ -241,7 +241,7 @@
          return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
  #endif
      } catch (OutOfMemoryException&){
--        printf("=============================================================================\n");
+-        printf("=========================================================================\n");
 +        printf("================================================================================\n");
          printf("INDETERMINATE\n");
          exit(0);
      }
-diff -uNr glueminisat-2.2.5.orig/core/Solver.cc glueminisat-2.2.5/core/Solver.cc
---- glueminisat-2.2.5.orig/core/Solver.cc	2011-02-27 22:04:33.000000000 -0800
-+++ glueminisat-2.2.5/core/Solver.cc	2012-04-24 10:10:42.733250577 -0700
-@@ -101,7 +101,7 @@
- 	printf("act=%f\n", c.activity());
+diff -uNr glueminisat-2.2.7.orig/code/core/Solver.cc glueminisat-2.2.7/code/core/Solver.cc
+--- glueminisat-2.2.7.orig/code/core/Solver.cc	2013-05-02 07:57:31.000000000 -0700
++++ glueminisat-2.2.7/code/core/Solver.cc	2013-07-05 20:56:20.144637404 -0700
+@@ -212,7 +212,7 @@
+     printf("\n");
  }
- void Solver::printLog() {
--	printf("| %9d | %7d %8d %8d | %8d %6.0f %6.1f %6.1f | %6.3f %% |\n",
-+	printf("|%9d|%7d %8d %8d|%8d %7.0f %7.1f %7.1f| %7.4f%%|\n",
+ void Solver::printLog() const {
+-    printf("| %9d | %7d %8d | %8d %6.0f %6.1f | %7.1f %6.1f %6.2f |\n",
++    printf("|%9d |%8d %8d |%9d %6.0f %6.1f |%7.1f %7.1f %6.3f |\n",
             (int)conflicts,
-            (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
-            nLearnts(), (double)learnts_literals/nLearnts(), (double)tot_lbds/nLearnts(), wholeDLVs/conflicts, progressEstimate()*100);
-@@ -862,7 +862,7 @@
- 
- 	// added by nabesima
-     if (verbosity >= 1) {
--    	printf("< ReduceDB %-3"PRIu64" (%4"PRIu64" restarts, %4.0f cnfs/res, %4.1f%% reduced, %4db %5dg %5dg3) >\n",
-+    	printf("< ReduceDB%-3"PRIu64" (%4"PRIu64"restarts, %4.0fcnfs/res, %4.1f%%reduced, %4db %5dg %5dg3) >\n",
-     		reduce_dbs, starts, (double)conflicts / starts, (double)nLearnts() / org_learnts * 100.0,
-     		num_bin, num_glue, num_glue3);
-     	printLog();
-@@ -1226,10 +1226,10 @@
+            (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(),
+            nLearnts(), (double)learnts_literals/nLearnts(), (double)tot_lbds/nLearnts(),
+@@ -1946,10 +1946,10 @@
          printf("===============================================================================\n");
          */
-     	// modified by nabesima
--        printf("===============================[ Search Statistics ]================================\n");
--        printf("| Conflicts |          ORIGINAL         |          LEARNT               | Progress |\n");
--        printf("|           |    Vars  Clauses Literals |  Clauses Lit/Cl LBD/Cl DLV/Cl |          |\n");
--        printf("====================================================================================\n");
+         // modified by nabesima
+-        printf("==============================[ Search Statistics ]==============================\n");
+-        printf("| Conflicts |     ORIGINAL     |         LEARNT         | Props/   DLV/  Prgrss |\n");
+-        printf("|           |   Vars   Clauses |  Clauses Lit/Cl LBD/Cl |   Conf    Conf   [%%]  |\n");
+-        printf("=================================================================================\n");
 +        printf("=============================[ Search Statistics ]==============================\n");
-+        printf("|Conflicts|         ORIGINAL        |             LEARNT             | Progress|\n");
-+        printf("|         |   Vars  Clauses Literals| Clauses  Lit/Cl  LBD/Cl  DLV/Cl|         |\n");
++        printf("|Conflicts |     ORIGINAL     |         LEARNT         | Props/    DLV/ Prgrss |\n");
++        printf("|          |    Vars  Clauses |  Clauses Lit/Cl LBD/Cl |   Conf    Conf   [%%]  |\n");
 +        printf("================================================================================\n");
-     }
  
-     // Search:
-@@ -1246,7 +1246,7 @@
+         printLog();
+     }
+@@ -1999,7 +1999,7 @@
      if (verbosity >= 1) {
-     	//printf("===============================================================================\n");
+         //printf("===============================================================================\n");
          printLog();
--        printf("====================================================================================\n");
+-        printf("=================================================================================\n");
 +        printf("================================================================================\n");
      }
  
- 
-@@ -1386,7 +1386,7 @@
- 
-     relocAll(to);
-     if (verbosity >= 2)
--        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
-+        printf("|  Garbage collection:   %12d bytes => %12d bytes              |\n", 
-                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
-     to.moveTo(ca);
- }
-diff -uNr glueminisat-2.2.5.orig/simp/Main.cc glueminisat-2.2.5/simp/Main.cc
---- glueminisat-2.2.5.orig/simp/Main.cc	2011-03-02 00:57:40.000000000 -0800
-+++ glueminisat-2.2.5/simp/Main.cc	2012-04-24 10:16:16.276234939 -0700
-@@ -150,20 +150,20 @@
+     if (status == l_True){
+diff -uNr glueminisat-2.2.7.orig/code/simp/Main.cc glueminisat-2.2.7/code/simp/Main.cc
+--- glueminisat-2.2.7.orig/code/simp/Main.cc	2013-04-30 00:02:26.000000000 -0700
++++ glueminisat-2.2.7/code/simp/Main.cc	2013-07-05 20:56:20.145637388 -0700
+@@ -156,8 +156,8 @@
              printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
-         
+ 
          if (S.verbosity > 0){
--            printf("===============================[ Problem Statistics ]===============================\n");
--            printf("|                                                                                  |\n"); }
+-            printf("=============================[ Problem Statistics ]==============================\n");
+-            printf("|                                                                               |\n"); }
 +            printf("=============================[ Problem Statistics ]=============================\n");
 +            printf("|                                                                              |\n"); }
-         
+ 
+         S.output = (argc >= 3) ? fopen(argv[2], "wb") : NULL;    // added by nabesima
          parse_DIMACS(in, S);
-         gzclose(in);
-         FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+@@ -165,12 +165,12 @@
+         //FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;    // modified by nabesima
  
          if (S.verbosity > 0){
--            printf("|  Number of variables:  %12d                                              |\n", S.nVars());
--            printf("|  Number of clauses:    %12d                                              |\n", S.nClauses()); }
+-            printf("|  Number of variables:  %12d                                           |\n", S.nVars());
+-            printf("|  Number of clauses:    %12d                                           |\n", S.nClauses()); }
 +            printf("|  Number of variables:  %12d                                          |\n", S.nVars());
 +            printf("|  Number of clauses:    %12d                                          |\n", S.nClauses()); }
-         
+ 
          double parsed_time = cpuTime();
          if (S.verbosity > 0)
--            printf("|  Parse time:           %12.2f s                                            |\n", parsed_time - initial_time);
+-            printf("|  Parse time:           %12.2f s                                         |\n", parsed_time - initial_time);
 +            printf("|  Parse time:           %12.4f s                                        |\n", parsed_time - initial_time);
  
          // Change to signal-handlers that will only notify the solver and allow it to terminate
          // voluntarily:
-@@ -173,13 +173,13 @@
+@@ -181,15 +181,15 @@
          S.eliminate(true);
          double simplified_time = cpuTime();
          if (S.verbosity > 0){
--            printf("|  Simplification time:  %12.2f s                                            |\n", simplified_time - parsed_time);
--            printf("|                                                                                  |\n"); }
+-            printf("|  Simplification time:  %12.2f s                                         |\n", simplified_time - parsed_time);
+-            printf("|                                                                               |\n"); }
 +            printf("|  Simplification time:  %12.4f s                                        |\n", simplified_time - parsed_time);
 +            printf("|                                                                              |\n"); }
  
          if (!S.okay()){
-             if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+             // modified by nabesima
+             if (S.output != NULL) fprintf(S.output, "0\n"), fclose(S.output);
+             //if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
              if (S.verbosity > 0){
--                printf("====================================================================================\n");
+-                printf("=================================================================================\n");
 +                printf("================================================================================\n");
                  printf("Solved by simplification\n");
                  printStats(S);
                  printf("\n"); }
-@@ -191,7 +191,7 @@
+@@ -201,7 +201,7 @@
  
          if (dimacs){
              if (S.verbosity > 0)
--                printf("=================================[ Writing DIMACS ]=================================\n");
+-                printf("===============================[ Writing DIMACS ]================================\n");
 +                printf("===============================[ Writing DIMACS ]===============================\n");
              S.toDimacs((const char*)dimacs);
              if (S.verbosity > 0)
                  printStats(S);
-@@ -234,7 +234,7 @@
+@@ -261,7 +261,7 @@
          return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
  #endif
      } catch (OutOfMemoryException&){
--        printf("====================================================================================\n");
+-        printf("=================================================================================\n");
 +        printf("================================================================================\n");
          printf("INDETERMINATE\n");
          exit(0);
      }
-diff -uNr glueminisat-2.2.5.orig/simp/SimpSolver.cc glueminisat-2.2.5/simp/SimpSolver.cc
---- glueminisat-2.2.5.orig/simp/SimpSolver.cc	2010-07-10 09:07:36.000000000 -0700
-+++ glueminisat-2.2.5/simp/SimpSolver.cc	2012-04-24 09:57:12.291351846 -0700
-@@ -655,7 +655,7 @@
-     }
- 
-     if (verbosity >= 1 && elimclauses.size() > 0)
--        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
-+        printf("|  Eliminated clauses:     %10.2f Mb                                       |\n", 
-                double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
- 
-     return ok;
-@@ -711,7 +711,7 @@
+diff -uNr glueminisat-2.2.7.orig/code/simp/SimpSolver.cc glueminisat-2.2.7/code/simp/SimpSolver.cc
+--- glueminisat-2.2.7.orig/code/simp/SimpSolver.cc	2013-05-01 21:42:24.000000000 -0700
++++ glueminisat-2.2.7/code/simp/SimpSolver.cc	2013-07-05 20:56:20.145637388 -0700
+@@ -757,7 +757,7 @@
      relocAll(to);
      Solver::relocAll(to);
      if (verbosity >= 2)
--        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
+-        printf("|  Garbage collection:   %12d bytes => %12d bytes                     |\n",
 +        printf("|  Garbage collection:   %12d bytes => %12d bytes              |\n", 
                 ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
      to.moveTo(ca);
  }
+@@ -904,7 +904,7 @@
+ 
+         int org_num_vars = nFreeVars();
+         if (verbosity >= 1)
+-            printf("|  Probing:              %12d vars                                      |\n", vars.size());
++            printf("|  Probing:              %12d vars                                     |\n", vars.size());
+         if (!probeVars(vars))
+             return false;
+         if (nFreeVars() == org_num_vars)
+@@ -916,7 +916,7 @@
+         if (!lazySimplify())
+             return false;
+         if (verbosity >= 1)
+-            printf("|  Eliminated:           %12d vars, %7d clauses                     |\n",
++            printf("|  Eliminated:           %12d vars, %7d clauses                            |\n",
+                     org_num_vars - nFreeVars(), org_num_clauses - clauses.size());
+ 
+             if (prb_equiv_vars > 0) {
diff --git a/glueminisat.spec b/glueminisat.spec
index 501d5bf..09c34c4 100644
--- a/glueminisat.spec
+++ b/glueminisat.spec
@@ -1,7 +1,7 @@
 
 Name:           glueminisat
-Version:        2.2.5
-Release:        6%{?dist}
+Version:        2.2.7
+Release:        1%{?dist}
 Summary:        Boolean SAT solver that implements literal blocks distance (LBD)
 
 License:        MIT
@@ -25,6 +25,8 @@ Patch0:         %{name}-FPU.patch
 Patch1:         %{name}-printf.patch
 # Copies of both patches above sent to Hidetomo Nabeshima on Mon Apr 23, 2012
 BuildRequires:  zlib-devel
+Requires(post):  %{_sbindir}/update-alternatives
+Requires(preun): %{_sbindir}/update-alternatives
 
 %description
 GlueMiniSat is a boolean, propositional satisfiability (SAT) problem
@@ -60,45 +62,87 @@ line options -minisat or -glucose, respectively.
 cp -p %{SOURCE1} .
 cp -p %{SOURCE2} .
 # Show key execution steps, so we can see that the right flags are used.
-sed -i 's/@$(CXX)/$(CXX)/' mtl/template.mk
-
+sed -i 's/@$(CXX)/$(CXX)/' code/mtl/template.mk
 
 %build
-# Build "simp", which adds simplification capabilities, instead of just "core"
-# The target "r" signifies that we are building the "released" version
-make %{?_smp_mflags} -C simp r \
-  MROOT=`pwd` \
-  COPTIMIZE="${RPM_OPT_FLAGS} -ffloat-store" \
-  LFLAGS="${RPM_OPT_FLAGS} -ffloat-store -lz"
-cp -p simp/%{name}_release %{name}
+# Build the "core" executable, (which omits the simplification capabilities)
+# The target "r" signifies that we are building the "release" version
+make %{?_smp_mflags} -C code/core r \
+  MROOT=`pwd`/code \
+  COPTIMIZE="${RPM_OPT_FLAGS}" \
+  LFLAGS="${RPM_OPT_FLAGS} -lz"
+cp -p code/core/%{name}-core_release %{name}_core
+# Build the "simp" executable, (which includes the simplification capabilities)
+# The target "r" signifies that we are building the "release" version
+make %{?_smp_mflags} -C code/simp r \
+  MROOT=`pwd`/code \
+  COPTIMIZE="${RPM_OPT_FLAGS}" \
+  LFLAGS="${RPM_OPT_FLAGS} -lz"
+cp -p code/simp/%{name}-simp_release %{name}_simp
 
 %install
 mkdir -p ${RPM_BUILD_ROOT}%{_bindir}
-install -m 0755 %{name} ${RPM_BUILD_ROOT}%{_bindir}
+# Install %{name}_core as a specific alternative for the generic name %{name}
+install -m 0755 %{name}_core ${RPM_BUILD_ROOT}%{_bindir}/%{name}_core
+# Install %{name}_simp as a specific alternative for the generic name %{name}
+install -m 0755 %{name}_simp ${RPM_BUILD_ROOT}%{_bindir}/%{name}_simp
+# Touch the generic path name (to be installed as a ghosted file)
+touch ${RPM_BUILD_ROOT}%{_bindir}/%{name}
+# Installation/removal in the alternatives system is done by the scripts below
 
 %check
 # The test file "glueminisat-test.in" is a brief quote from
 # http://www.satcompetition.org/2004/format-solvers2004.html
 # Exit value is 10 for satisfiable, 20 for unsatisfiable
-./glueminisat glueminisat-test.in glueminisat-test.out || true
-echo
-echo "RESULTS:"
-cat glueminisat-test.out
-result=`head -1 glueminisat-test.out`
-if [ "$result" = "SAT" ]; then
-  echo "SUCCESS - Correctly found that it was satisfiable"
+./glueminisat_core glueminisat-test.in glueminisat-test-core.out || true
+echo "TEST RESULTS (core):"
+cat glueminisat-test-core.out
+result_core=`head -1 glueminisat-test-core.out`
+./glueminisat_simp glueminisat-test.in glueminisat-test-simp.out || true
+echo "TEST RESULTS (simp):"
+cat glueminisat-test-simp.out
+result_simp=`head -1 glueminisat-test-simp.out`
+if [ "$result_core" = "SAT" -a "$result_simp" = "SAT" ]; then
+  echo "SUCCESS - all of the tests succeeded."
   true
 else
-  echo "Failed test."
+  echo "Failed one or more of the tests."
   false
 fi
 
+%post
+# Setup the alternatives for %{name}
+%{_sbindir}/update-alternatives \
+  --install %{_bindir}/%{name} %{name} %{_bindir}/%{name}_simp 60
+%{_sbindir}/update-alternatives \
+  --install %{_bindir}/%{name} %{name} %{_bindir}/%{name}_core 40
+
+%preun
+if [ $1 -eq 0 ]; then
+  # package removal, not an upgrade
+  %{_sbindir}/update-alternatives \
+  --remove %{name} %{_bindir}/%{name}_core
+  %{_sbindir}/update-alternatives \
+  --remove %{name} %{_bindir}/%{name}_simp
+fi
+
 %files
-%doc LICENSE README README.minisat
-%doc %{name}-intro.html %{name}-test.in %{name}-test.out
-%attr(755,root,root) %{_bindir}/%{name}
+%doc license.txt readme.txt readme.minisat %{name}-intro.html
+%doc %{name}-test.in %{name}-test-core.out %{name}-test-simp.out
+%attr(755,root,root) %{_bindir}/%{name}_core
+%attr(755,root,root) %{_bindir}/%{name}_simp
+%ghost %{_bindir}/%{name}
 
 %changelog
+* Tue Aug 13 2013 John C. Peterson <jcp at eskimo.com> - 2.2.7-1
+- Updated to the latest release from upstream. Some of the fixes from the
+  previous glueminisat-printf.patch were incorporated by upstream into 2.2.7.
+  Modified the patch to address new problems of a similar (cosmetic) nature.
+- Now builds both the "core" and "simp" executables and installs them as
+  alternatives for the generic executable named "glueminisat".
+- Some minor changes to the build process to support the alternatives.
+- Eliminated the -ffloat-store compiler option (as it's configured at runtime)
+
 * Sat Aug 03 2013 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 2.2.5-6
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
 
diff --git a/sources b/sources
index 6e29a1e..c80a289 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-1b96e19f7c0c5e0bec8c26c4eead9261  glueminisat-2.2.5.tar.gz
+9519374b4e4677212d3ed3cb731ba4f9  glueminisat-2.2.7.tar.gz


More information about the scm-commits mailing list