gentoo resync : 02.02.2022

6 files changed, 84 insertions, 619 deletions

diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest
index 3e2e561057fe..ed887b8cb2cf 100644
--- a/sci-mathematics/minisat/Manifest
+++ b/sci-mathematics/minisat/Manifest
@@ -1,7 +1,5 @@
-AUX minisat-2.2.0_p20130925-nusmv.patch 17540 BLAKE2B 4dee908cb3b7f466ea2fa908667d37ebd3298069f6b09dafb1e5fd50a1e4f0bba318151efd38385b7e7571f0aa753dd34191fa3b08f64ad626f777c0df8528db SHA512 cfad7fb104f8630396f745144da7c052b1e6d5eb3ac9f3cc86a71c9d1353664ea9ece3cbd977f12a9d3a18efc245e33eb97bb949516c5620d3f6b76aa3c1586c
+AUX minisat-2.2.1-cmake.patch 1971 BLAKE2B f194354706bafb51111648221b9ccb03c808caf245a45a0cc00bfd06d5167e46963bfe3c66164dd9df34373cc74ea36e4b11b69b9806363decc925b4db469d07 SHA512 5ceb69491e6a5dd6d7438f567a9c92f7c39e7e93fae776f901e6df1b855d2242941df3bf34e8e147992a9ed5b5120704172c4c9502db5f8baf962c058d26679e
 DIST MiniSat.pdf 327416 BLAKE2B 77f77d763c9554680b4c5e1688801e8462102e8ddbcc3b53badccee17a98f935ef0e971a636abeb04021a2b3a3e9d6acfe4828b5dd20e6ef8733d71788cc31b0 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6
-DIST minisat-2.2.0_p20130925.tar.gz 49544 BLAKE2B 8c6893fb6c604140609c36cc912c02a73c1f2726d7f399595c50d674aff69c57f9c4914da6d95c37a46fefc218dd4b0550645bd7058d46640d08103e2a4ec333 SHA512 37fc35cc4f3104d7f0e8ee9f7123fc34e175df578658266799d809d71d6cf081e811919f304a02f6cb9c3827d308e59408149d63d1d1e7c6d0b495350f93b3d9
 DIST minisat-2.2.1.tar.gz 50485 BLAKE2B 58c292f0b90dd459fa29fadbf9e2b20106406c08df9ce98f40138b12a8f001b4ab72f661815d1254c6c90158c3d6e3df339c784552605a935ebc5e703b2d8768 SHA512 a69734e1a70fe056f9dfd479fe4e6e25bc418d3631c1c2d0dea1190ffe9f86b1fc5e9aabaf3772a752fe654551f1e84e47fcb8655f6fe25176efc8d8bc96c663
-EBUILD minisat-2.2.0_p20130925-r1.ebuild 1612 BLAKE2B 4198df59696fa88b779ab8ea9954a1f53db39b8e9dfaf1c80897f5a772d9436731579ec2adf59d292bb0d9aa6baab446057333188838ed2a6548efd6ef5990fa SHA512 2bcbf4aeadb12e0998bdc97065c527dbeb29b155e352feaf4b871b89028a1784025c71e8e2f9ee27a135056feeb4fd557967c5d0e130b0b88ef7cfdc396aa438
-EBUILD minisat-2.2.1.ebuild 700 BLAKE2B e911c31d9ed3f6847e80f832f657fe06cce9fcc1faa75ab97fdb819dee89eae24094089ef41148ad85a0ea41619a8db66c96a5a4508c293b15c647010d204e00 SHA512 68a4c1bfc7d8deeeb401b8d1d11a994cc75731fb5a0b14ce9d11063a4578bfad848db462efe146591134db2b653c3366a2d59bfdce51aec7ecd2cfcaffc98fa2
-MISC metadata.xml 1285 BLAKE2B ac5f5813e82419840d0a004e623b08d88967bbf9e4e617c2ec23bdd574c67cee349f83aefcf719aa4151b991eaa6e5ee5fe0a1fcc955bd56b6bc6cb84cda3235 SHA512 ee16bf934be05d0128e0d9bce30dc9fab70a6b8934e6d6047a8e9a11a9558cd0fbe824323b98573589f6bd6cc2eae925f591d9cd97193d5f63769d28074e5fd0
+EBUILD minisat-2.2.1-r1.ebuild 639 BLAKE2B 651b93daea22d747fb472004c0f48643490ee8c15f1e1de43aa73f4df848309b610b01c8e79530f64517a78e5720c6c22b94e95b87871ea63a600a67ee09a8e7 SHA512 5adda43272e97882dcff9df129e18720eeb6e2dd7ead21a86f3448af08300699ed2ba01e0d53951dfd27ac7d7e4031766fd3c0a9c5139a1b1d60882493556286
+MISC metadata.xml 1244 BLAKE2B 7ef490fc9e45d1f9af7e5b40028614d71557e055fea15289dffcf4afc16fe72ecfa48b4dc7508ee042f603bd7035ccdc529b3640f33d67e96b3b5ede433455c4 SHA512 e6dbcbc2433da6491c94eefbcdf78d5634ca17c4c2e6174a832b46b75a6771cb1b7d92a3fe14d739dc9215a78126e40fe8447b2b3a65c355f9addcf4084ffe3d
diff --git a/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch b/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
deleted file mode 100644
index 4b17c8fb44bb..000000000000
--- a/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
+++ /dev/null
@@ -1,527 +0,0 @@
---- a/Makefile
-+++ b/Makefile
-@@ -69,8 +89,8 @@
- VERB=
- endif
- 
--SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc)
--HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h)
-+SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) $(wildcard minisat/proof/*.cc)
-+HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h) $(wildcard minisat/proof/*.h)
- OBJS = $(filter-out %Main.o, $(SRCS:.cc=.o))
- 
- r:	$(BUILD_DIR)/release/bin/$(MINISAT)
-@@ -89,7 +109,7 @@
- lsh:	$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
- 
- ## Build-type Compile-flags:
--$(BUILD_DIR)/release/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM)
-+$(BUILD_DIR)/release/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM) $(MINISAT_FPIC)
- $(BUILD_DIR)/debug/%.o:				MINISAT_CXXFLAGS +=$(MINISAT_DEB) -g
- $(BUILD_DIR)/profile/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_PRF) -pg
- $(BUILD_DIR)/dynamic/%.o:			MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)
-@@ -195,7 +215,7 @@
- 	$(INSTALL) -d $(DESTDIR)$(bindir)
- 	$(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir)
- 
--clean:
-+origclean:
- 	rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
-           $(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
- 	  $(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \
-@@ -203,6 +223,7 @@
- 	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
- 	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
- 	  $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
-+	rm -f $(NUSMV_LIBNAME)
- 
- distclean:	clean
- 	rm -f config.mk
---- a/minisat/core/Solver.cc
-+++ b/minisat/core/Solver.cc
-@@ -101,7 +101,16 @@
-   , conflict_budget    (-1)
-   , propagation_budget (-1)
-   , asynch_interrupt   (false)
--{}
-+{
-+    // NuSMV: MOD BEGIN
-+    /* Disables "progress saving" which relies on last polarity
-+       assigned to a var when branching. Polarity for us is forced to
-+       be false. See http://reasoning.cs.ucla.edu/fetch.php?id=69&type=pdf
-+    */
-+    phase_saving = 0;
-+    default_polarity = l_Undef;
-+    // NuSMV: MOD END
-+}   
- 
- 
- Solver::~Solver()
-@@ -250,8 +259,19 @@
- {
-     Var next = var_Undef;
- 
-+    // NuSMV: PREF MOD
-+    // Selection from preferred list
-+    for (int i = 0; i < preferred.size(); i++) {
-+      if (value(preferred[i]) == l_Undef) {
-+        next = preferred[i];
-+        break;
-+      }
-+    }
-+    // NuSMV: PREF MOD END
-+
-     // Random decision:
--    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
-+    if (next == var_Undef && // NuSMV: PREF MOD
-+        drand(random_seed) < random_var_freq && !order_heap.empty()){
-         next = order_heap[irand(random_seed,order_heap.size())];
-         if (value(next) == l_Undef && decision[next])
-             rnd_decisions++; }
-@@ -269,6 +289,8 @@
-         return lit_Undef;
-     else if (user_pol[next] != l_Undef)
-         return mkLit(next, user_pol[next] == l_True);
-+    else if (default_polarity != l_Undef) // NuSMV
-+        return mkLit(next, default_polarity == l_True);
-     else if (rnd_pol)
-         return mkLit(next, drand(random_seed) < 0.5);
-     else
-@@ -620,6 +642,19 @@
- }
- 
- 
-+// NuSMV: PREF MOD
-+void Solver::addPreferred(Var v)
-+{
-+    preferred.push(v);
-+}
-+
-+void Solver::clearPreferred()
-+{
-+    preferred.clear(0);
-+}
-+// NuSMV: PREF MOD END
-+
-+
- void Solver::rebuildOrderHeap()
- {
-     vec<Var> vs;
---- a/minisat/core/Solver.h
-+++ b/minisat/core/Solver.h
-@@ -90,6 +90,19 @@
-     void    setPolarity    (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
-     void    setDecisionVar (Var v, bool b);  // Declare if a variable should be eligible for selection in the decision heuristic.
- 
-+    // NuSMV: PREF MOD
-+    /*
-+     * Add a variable at the end of the list of preferred variables
-+     * Does not remove the variable from the standard ordering.
-+     */
-+    void addPreferred(Var v);
-+    
-+    /*
-+     * Clear vector of preferred variables.
-+     */
-+    void clearPreferred();
-+    // NuSMV: PREF MOD END
-+    
-     // Read state:
-     //
-     lbool   value      (Var x) const;       // The current value of a variable.
-@@ -134,6 +147,8 @@
-     int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
-     int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
-     bool      rnd_pol;            // Use random polarities for branching heuristics.
-+    lbool     default_polarity; // NuSMV: default polarity for vars
-+    
-     bool      rnd_init_act;       // Initialize variable activities with a small random value.
-     double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
-     int       min_learnts_lim;    // Minimum number to set the learnts limit to.
-@@ -215,6 +230,10 @@
-     Var                 next_var;         // Next variable to be created.
-     ClauseAllocator     ca;
- 
-+    // NuSMV: PREF MOD
-+    vec<Var>            preferred;
-+    // NuSMV: PREF MOD END
-+
-     vec<Var>            released_vars;
-     vec<Var>            free_vars;
- 
---- a/minisat/core/SolverTypes.h
-+++ b/minisat/core/SolverTypes.h
-@@ -52,7 +52,7 @@
-     int     x;
- 
-     // Use this as a constructor:
--    friend Lit mkLit(Var var, bool sign = false);
-+    friend Lit mkLit(Var var, bool sign);
- 
-     bool operator == (Lit p) const { return x == p.x; }
-     bool operator != (Lit p) const { return x != p.x; }
-@@ -61,6 +61,7 @@
- 
- 
- inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
-+inline  Lit  mkLit     (Var var)            { return mkLit(var, false); }
- inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
- inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
- inline  bool sign      (Lit p)              { return p.x & 1; }
-@@ -120,6 +121,7 @@
- inline int   toInt  (lbool l) { return l.value; }
- inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
- 
-+#define MINISAT_CONSTANTS_AS_MACROS
- #if defined(MINISAT_CONSTANTS_AS_MACROS)
-   #define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
-   #define l_False (lbool((uint8_t)1))
---- a/minisat/simp/Solver_C.cc
-+++ b/minisat/simp/Solver_C.cc
-@@ -0,0 +1,246 @@
-+
-+/**************************************************************************************************
-+
-+Solver_C.C
-+
-+C-wrapper for Solver.C
-+
-+  This file is part of NuSMV version 2. 
-+  Copyright (C) 2007 by FBK-irst. 
-+  Author: Roberto Cavada <cavada@fbk.eu>
-+
-+  NuSMV version 2 is free software; you can redistribute it and/or 
-+  modify it under the terms of the GNU Lesser General Public 
-+  License as published by the Free Software Foundation; either 
-+  version 2 of the License, or (at your option) any later version.
-+
-+  NuSMV version 2 is distributed in the hope that it will be useful, 
-+  but WITHOUT ANY WARRANTY; without even the implied warranty of 
-+  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
-+  Lesser General Public License for more details.
-+
-+  You should have received a copy of the GNU Lesser General Public 
-+  License along with this library; if not, write to the Free Software 
-+  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
-+
-+  For more information on NuSMV see <http://nusmv.fbk.eu>
-+  or email to <nusmv-users@fbk.eu>.
-+  Please report bugs to <nusmv-users@fbk.eu>.
-+
-+  To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
-+
-+**************************************************************************************************/
-+
-+
-+#include "SimpSolver.h"
-+extern "C" {
-+#include "Solver_C.h"
-+}
-+
-+namespace {
-+using Minisat::lbool;
-+} // namespace
-+
-+extern "C" MiniSat_ptr MiniSat_Create()
-+{
-+  Minisat::SimpSolver *s = new Minisat::SimpSolver();
-+  s->default_polarity = l_True;
-+  return (MiniSat_ptr)s;
-+}
-+
-+extern "C" void MiniSat_Delete(MiniSat_ptr ms)
-+{
-+  delete (Minisat::SimpSolver *)ms;
-+}
-+
-+extern "C" int MiniSat_Nof_Variables(MiniSat_ptr ms)
-+{
-+  return ((Minisat::SimpSolver *)ms)->nVars();
-+}
-+
-+extern "C" int MiniSat_Nof_Clauses(MiniSat_ptr ms)
-+{
-+  return ((Minisat::SimpSolver *)ms)->nClauses();
-+}
-+
-+/* variables are in the range 1...N */
-+extern "C" int MiniSat_New_Variable(MiniSat_ptr ms)
-+{
-+  /* Actually, minisat used variable range 0 .. N-1,
-+     so in all function below there is a convertion between
-+     input variable (1..N) and internal variables (0..N-1)
-+  */	
-+  Minisat::Var var = ((Minisat::SimpSolver *)ms)->newVar();
-+  ((Minisat::SimpSolver *)ms)->setFrozen(var, true);
-+  return var+1;
-+}
-+
-+
-+/*
-+ * Here clauses are in dimacs form, variable indexing is 1...N
-+ */
-+extern "C" int MiniSat_Add_Clause(MiniSat_ptr ms,
-+                                  int *clause_lits, int num_lits)
-+{
-+  int i;
-+  Minisat::vec<Minisat::Lit> cl;
-+  for(i = 0; i < num_lits; ++i) {
-+    const int lit = clause_lits[i];
-+    assert(abs(lit) > 0);
-+    assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
-+    int var = abs(lit) - 1;
-+    cl.push((lit > 0) ? Minisat::mkLit(var) : ~ Minisat::mkLit(var));
-+  }
-+  ((Minisat::SimpSolver *)ms)->addClause(cl);
-+
-+  if(((Minisat::SimpSolver *)ms)->okay()) return 1;
-+  return 0;
-+}
-+
-+extern "C" int MiniSat_Solve(MiniSat_ptr ms)
-+{
-+  bool ret = ((Minisat::SimpSolver *)ms)->solve();
-+  if(ret) return 1;
-+  return 0;
-+}
-+
-+/*
-+ * Here the assumption is in "dimacs form", variable indexing is 1...N
-+ */
-+extern "C" int MiniSat_Solve_Assume(MiniSat_ptr ms,
-+				    int nof_assumed_lits,
-+				    int *assumed_lits)
-+{
-+  int i;
-+  Minisat::vec<Minisat::Lit> cl;
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
-+
-+  solver.simplify();
-+  if(solver.okay() == false) return 0;
-+
-+  assert(nof_assumed_lits >= 0);
-+  for(i = 0; i < nof_assumed_lits; ++i) {
-+    const int lit = assumed_lits[i];
-+    assert(abs(lit) > 0);
-+    assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
-+    int var = abs(lit) - 1;
-+    cl.push((lit > 0) ? Minisat::mkLit(var) : ~Minisat::mkLit(var));
-+  }
-+
-+  if (solver.solve(cl)) return 1;
-+  return 0;
-+}
-+
-+extern "C" int MiniSat_simplifyDB(MiniSat_ptr ms)
-+{
-+  ((Minisat::SimpSolver *)ms)->simplify();
-+  if(((Minisat::SimpSolver *)ms)->okay()) return 1;
-+  return 0;
-+}
-+
-+/*
-+ * Here variables are numbered 1...N
-+ */
-+extern "C" int MiniSat_Get_Value(MiniSat_ptr ms, int var_num)
-+{
-+  assert(var_num > 0);
-+  if(var_num > MiniSat_Nof_Variables(ms)) return -1;
-+  /* minisat assigns all variables. just check */
-+  assert(((Minisat::SimpSolver *)ms)->model[var_num-1] != l_Undef); 
-+  
-+  if(((Minisat::SimpSolver *)ms)->model[var_num-1] == l_True) return 1;
-+  return 0;
-+}
-+
-+extern "C" int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms)
-+{
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
-+
-+  return solver.conflict.size();
-+}
-+
-+extern "C" void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits)
-+{
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
-+
-+  Minisat::LSet& cf = solver.conflict;
-+
-+  for (int i = 0; i < cf.size(); ++i) {
-+    int v = Minisat::var(~cf[i]);
-+    int s = Minisat::sign(~cf[i]);
-+    assert(v != Minisat::var_Undef);
-+    conflict_lits[i] = (s == 0) ? (v+1) : -(v+1);
-+  }
-+}
-+
-+/** mode can be  polarity_user, polarity_rnd */
-+extern "C" void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode)
-+{
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  assert(__polarity_unsupported != mode); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);  
-+  if (polarity_rnd == mode) {
-+    solver.rnd_pol = true;
-+    solver.default_polarity = l_Undef;
-+  }
-+  else {
-+    // assert(polarity_user == mode);
-+    solver.rnd_pol = false;
-+    switch (mode) {
-+    case polarity_false:
-+      solver.default_polarity = l_True;
-+      break;
-+    case polarity_true:
-+      solver.default_polarity = l_False;
-+      break;
-+    default: // polarity_user
-+      solver.default_polarity = l_Undef;
-+      break;
-+    }
-+  }
-+}
-+
-+extern "C" int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms)
-+{
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);  
-+  //return solver.rnd_pol ? polarity_rnd : polarity_user;
-+  if (solver.rnd_pol) {
-+    return polarity_rnd;
-+  } else if (solver.default_polarity == l_True) {
-+    return polarity_false;
-+  } else if (solver.default_polarity == l_False) {
-+    return polarity_true;
-+  } else {
-+    return polarity_user;
-+  }
-+}
-+
-+extern "C" void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed)
-+{
-+  assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms)); 
-+  Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
-+  solver.random_seed = seed;
-+}
-+
-+
-+// NuSMV: PREF MOD
-+/* variables are in the range 1...N */
-+extern "C" void MiniSat_Set_Preferred_Variable(MiniSat_ptr ms, int x)
-+{
-+  /* Actually, minisat used variable range 0 .. N-1,
-+     so in all function below there is a convertion between
-+     input variable (1..N) and internal variables (0..N-1)
-+  */
-+  ((Minisat::SimpSolver *)ms)->addPreferred((Minisat::Var) x);
-+}
-+
-+extern "C" void MiniSat_Clear_Preferred_Variables(MiniSat_ptr ms)
-+{
-+
-+  ((Minisat::SimpSolver *)ms)->clearPreferred();
-+}
-+// NuSMV: PREF MOD END
---- a/minisat/simp/Solver_C.h
-+++ b/minisat/simp/Solver_C.h
-@@ -0,0 +1,72 @@
-+/**************************************************************************************************
-+
-+Solver_C.h
-+
-+C-wrapper for Solver.h
-+
-+  This file is part of NuSMV version 2. 
-+  Copyright (C) 2007 by FBK-irst. 
-+  Author: Roberto Cavada <cavada@fbk.eu>
-+
-+  NuSMV version 2 is free software; you can redistribute it and/or 
-+  modify it under the terms of the GNU Lesser General Public 
-+  License as published by the Free Software Foundation; either 
-+  version 2 of the License, or (at your option) any later version.
-+
-+  NuSMV version 2 is distributed in the hope that it will be useful, 
-+  but WITHOUT ANY WARRANTY; without even the implied warranty of 
-+  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
-+  Lesser General Public License for more details.
-+
-+  You should have received a copy of the GNU Lesser General Public 
-+  License along with this library; if not, write to the Free Software 
-+  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
-+
-+  For more information on NuSMV see <http://nusmv.fbk.eu>
-+  or email to <nusmv-users@fbk.eu>.
-+  Please report bugs to <nusmv-users@fbk.eu>.
-+
-+  To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
-+
-+**************************************************************************************************/
-+
-+#ifndef SOLVER_C_h
-+#define SOLVER_C_h
-+
-+//=================================================================================================
-+// Solver -- the main class:
-+
-+#define MiniSat_ptr void *
-+
-+enum {
-+  __polarity_unsupported = -1,
-+  polarity_true = 0, 
-+  polarity_false = 1, 
-+  polarity_user = 2,  
-+  polarity_rnd = 3,
-+};
-+
-+MiniSat_ptr MiniSat_Create();
-+void MiniSat_Delete(MiniSat_ptr);
-+int MiniSat_Nof_Variables(MiniSat_ptr);
-+int MiniSat_Nof_Clauses(MiniSat_ptr);
-+int MiniSat_New_Variable(MiniSat_ptr);
-+int MiniSat_Add_Clause(MiniSat_ptr, int *clause_lits, int num_lits);
-+int MiniSat_Solve(MiniSat_ptr);
-+int MiniSat_Solve_Assume(MiniSat_ptr, int nof_assumed_lits, int *assumed_lits);
-+int MiniSat_simplifyDB(MiniSat_ptr);
-+int MiniSat_Get_Value(MiniSat_ptr, int var_num);
-+int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms);
-+void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits);
-+
-+void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode);
-+int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms);
-+void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed);
-+
-+// NuSMV: PREF MOD
-+void MiniSat_Set_Preferred_Variable(MiniSat_ptr, int);
-+void MiniSat_Clear_Preferred_Variables(MiniSat_ptr);
-+// NuSMV: PREF MOD END
-+
-+//=================================================================================================
-+#endif
---- a/minisat/utils/System.cc
-+++ b/minisat/utils/System.cc
-@@ -77,7 +77,7 @@
-     struct rusage ru;
-     getrusage(RUSAGE_SELF, &ru);
-     return (double)ru.ru_maxrss / 1024; }
--double Minisat::memUsedPeak() { return memUsed(); }
-+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
- 
- 
- #elif defined(__APPLE__)
-@@ -87,11 +87,11 @@
-     malloc_statistics_t t;
-     malloc_zone_statistics(NULL, &t);
-     return (double)t.max_size_in_use / (1024*1024); }
--double Minisat::memUsedPeak() { return memUsed(); }
-+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
- 
- #else
- double Minisat::memUsed()     { return 0; }
--double Minisat::memUsedPeak() { return 0; }
-+double Minisat::memUsedPeak(bool strictlyPeak) { return 0; }
- #endif
- 
- 
diff --git a/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch b/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch
new file mode 100644
index 000000000000..1c875827f6ac
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch
@@ -0,0 +1,54 @@
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -2,6 +2,7 @@
+ 
+ project(minisat)
+ 
++include(GNUInstallDirs)
+ #--------------------------------------------------------------------------------------------------
+ # Configurable options:
+ 
+@@ -44,24 +45,16 @@
+     minisat/core/Solver.cc
+     minisat/simp/SimpSolver.cc)
+ 
+-add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES})
+ add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES})
+ 
+ target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY})
+-target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY})
+ 
+ add_executable(minisat_core minisat/core/Main.cc)
+ add_executable(minisat_simp minisat/simp/Main.cc)
+ 
+-if(STATIC_BINARIES)
+-  target_link_libraries(minisat_core minisat-lib-static)
+-  target_link_libraries(minisat_simp minisat-lib-static)
+-else()
+-  target_link_libraries(minisat_core minisat-lib-shared)
+-  target_link_libraries(minisat_simp minisat-lib-shared)
+-endif()
++target_link_libraries(minisat_core minisat-lib-shared)
++target_link_libraries(minisat_simp minisat-lib-shared)
+ 
+-set_target_properties(minisat-lib-static PROPERTIES OUTPUT_NAME "minisat")
+ set_target_properties(minisat-lib-shared
+   PROPERTIES
+     OUTPUT_NAME "minisat" 
+@@ -73,11 +66,11 @@
+ #--------------------------------------------------------------------------------------------------
+ # Installation targets:
+ 
+-install(TARGETS minisat-lib-static minisat-lib-shared minisat_core minisat_simp 
+-        RUNTIME DESTINATION bin
+-        LIBRARY DESTINATION lib
+-        ARCHIVE DESTINATION lib)
++install(TARGETS minisat-lib-shared minisat_core minisat_simp 
++        RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}
++        LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
++        ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
+ 
+ install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp
+-        DESTINATION include/minisat
++        DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/minisat
+         FILES_MATCHING PATTERN "*.h")
diff --git a/sci-mathematics/minisat/metadata.xml b/sci-mathematics/minisat/metadata.xml
index 812aa0c09202..68f253bc3c2d 100644
--- a/sci-mathematics/minisat/metadata.xml
+++ b/sci-mathematics/minisat/metadata.xml
@@ -1,28 +1,27 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
-
 <pkgmetadata>
-  <maintainer type="project">
-    <email>sci@gentoo.org</email>
-    <name>Gentoo Science Project</name>
-  </maintainer>
-  <longdescription>
-    MiniSat is a minimalistic, open-source SAT solver, developed to help
-    researchers and developers alike to get started on SAT. It is released
-    under the MIT licence, and is currently used in a number of projects.
-    MiniSat is small and well-documented, and possibly also well-designed,
-    making it an ideal starting point for adapting SAT based techniques to
-    domain specific problems.
-    Winning all the industrial categories of the SAT 2005 competition, MiniSat
-    is a good starting point both for future research in SAT, and for
-    applications using SAT.
-    MiniSat supports incremental SAT and has mechanisms for adding non-clausal
-    constraints. By virtue of being easy to modify, it is a good choice for
-    integrating as a backend to another tool, such as a model checker or a more
-    generic constraint solver.
-  </longdescription>
-  <upstream>
-    <remote-id type="github">niklasso/minisat</remote-id>
-    <remote-id type="github">stp/minisat</remote-id>
-  </upstream>
+	<maintainer type="project">
+		<email>sci@gentoo.org</email>
+		<name>Gentoo Science Project</name>
+	</maintainer>
+	<longdescription>
+		MiniSat is a minimalistic, open-source SAT solver, developed to help
+		researchers and developers alike to get started on SAT. It is released
+		under the MIT licence, and is currently used in a number of projects.
+		MiniSat is small and well-documented, and possibly also well-designed,
+		making it an ideal starting point for adapting SAT based techniques to
+		domain specific problems.
+		Winning all the industrial categories of the SAT 2005 competition, MiniSat
+		is a good starting point both for future research in SAT, and for
+		applications using SAT.
+		MiniSat supports incremental SAT and has mechanisms for adding non-clausal
+		constraints. By virtue of being easy to modify, it is a good choice for
+		integrating as a backend to another tool, such as a model checker or a more
+		generic constraint solver.
+	</longdescription>
+	<upstream>
+		<remote-id type="github">niklasso/minisat</remote-id>
+		<remote-id type="github">stp/minisat</remote-id>
+	</upstream>
 </pkgmetadata>
diff --git a/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild b/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild
deleted file mode 100644
index 39e62e229e7d..000000000000
--- a/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild
+++ /dev/null
@@ -1,57 +0,0 @@
-# Copyright 1999-2016 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=6
-
-inherit toolchain-funcs vcs-snapshot
-
-DESCRIPTION="Small yet efficient SAT solver with reference paper"
-HOMEPAGE="http://minisat.se/Main.html"
-COMMIT=37dc6c67e2af26379d88ce349eb9c4c6160e8543
-SRC_URI="https://github.com/niklasso/minisat/archive/${COMMIT}.tar.gz -> ${P}.tar.gz
-	doc? ( http://minisat.se/downloads/MiniSat.pdf )"
-
-SLOT="0"
-KEYWORDS="~amd64 ~x86 ~amd64-linux ~x86-linux"
-LICENSE="MIT"
-
-IUSE="debug doc"
-
-DEPEND="sys-libs/zlib"
-RDEPEND="${DEPEND}"
-DOCS=( README doc/ReleaseNotes-${PV%_*}.txt )
-PATCHES=( "${FILESDIR}"/${P}-nusmv.patch )
-
-src_prepare() {
-	default
-	# Remove makefile silencing and
-	# Remove static linking by default
-	sed -i -e "s/VERB=@/VERB=/" \
-		-e "s/--static //g" \
-		Makefile || die
-
-	sed -i -e "s:\$(exec_prefix)/lib:\$(exec_prefix)/$(get_libdir):" \
-		Makefile || die
-
-	# Fix headers ( #include "minisat/..." -> #include <...> )
-	while IFS="" read -d $'\0' -r file; do
-		einfo Correcting header "$file"
-		sed -i -e 's:#include "minisat/\([^"]*\)":#include <minisat/\1>:g' "${file}" || die
-	done < <(find minisat -name "*.h" -print0)
-}
-
-src_configure() {
-	local minisat_cflags="${CFLAGS} -D NDEBUG -I${S}/minisat"
-	emake config prefix="${EPREFIX}"/usr MINISAT_RELSYM="" MINISAT_REL="${minisat_cflags}" MINISAT_PRF="${minisat_cflags}" MINISAT_DEB="${CFLAGS} -D DEBUG -I${S}/minisat"
-}
-
-src_compile() {
-	emake all $(usex debug d "")
-}
-
-src_install() {
-	use doc && DOCS+=( "${DISTDIR}"/MiniSat.pdf )
-	default
-
-	dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
-}
diff --git a/sci-mathematics/minisat/minisat-2.2.1.ebuild b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
index 360c5a33082b..15d260429e0f 100644
--- a/sci-mathematics/minisat/minisat-2.2.1.ebuild
+++ b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -11,19 +11,17 @@ SRC_URI="https://github.com/stp/${PN}/archive/releases/${PV}.tar.gz -> ${P}.tar.
 	doc? ( http://minisat.se/downloads/MiniSat.pdf )"
 S="${WORKDIR}/${PN}-releases-${PV}"
 
+LICENSE="MIT"
 SLOT="0/${PV}"
 KEYWORDS="~amd64 ~x86"
-LICENSE="MIT"
 IUSE="doc"
 
 RDEPEND="sys-libs/zlib:="
 DEPEND="${RDEPEND}"
 
+PATCHES=( "${FILESDIR}"/${P}-cmake.patch )
+
 src_install() {
 	cmake_src_install
-
-	mv "${D}"/usr/lib "${D}"/usr/$(get_libdir) || die
-	dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
-
 	use doc && dodoc "${DISTDIR}"/MiniSat.pdf
 }