reinit the tree, so we can have metadata

6 files changed, 834 insertions, 0 deletions

diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest
new file mode 100644
index 000000000000..ac7b99cb502e
--- /dev/null
+++ b/sci-mathematics/minisat/Manifest
@@ -0,0 +1,10 @@
+AUX minisat-2.2.0-header_fix.patch 3879 SHA256 edcfefe00d39997e5c553ad583aa432315425d321af9fb5a56c530862482a50e SHA512 1a8a00e1a049dfab2c7041043ebc47eb09cac38c634c9fc54725fd262d24ef1f49dd445f2330122623d6464effd2755c36e7d16b3d5681a31ca1da0fcf9491b0 WHIRLPOOL 08b5336d0e9032783f2f174c99697ea407efbc4ce7d2a31ebb35544441e02851ea395e32b01d3c10125764f57374c69ad49643ad8700218382b6882607bc87a7
+AUX minisat-2.2.0_p20130925-nusmv.patch 17540 SHA256 88615ec21bfba218959914ce04fb536b77ec459aa62150b380fd802288cbab7c SHA512 cfad7fb104f8630396f745144da7c052b1e6d5eb3ac9f3cc86a71c9d1353664ea9ece3cbd977f12a9d3a18efc245e33eb97bb949516c5620d3f6b76aa3c1586c WHIRLPOOL de43b31eafef9e3a3c4af4ed8b0c48c4d257790372c60636806f884cb91842bc98fecf7dba49e66653190cebce00065bdc5c638261c0b95970da5db62f1ba454
+DIST MiniSat.pdf 327416 SHA256 53197dbd783c924a2627d75e305706297988494265bd5e5ec873840e5d797ac4 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6 WHIRLPOOL a087d8929476fc33464d19432fc05a01797761f695b81c0aa6d35270731b00dabe2402ea2cfd705b49d5d6664a3cbd46bc60147d60934acdfc94a33066316185
+DIST minisat-2.2.0.tar.gz 43879 SHA256 92957d851cdc3baddfe07b5fc80ed5a0237c489d0c52ae72f62844b3b46d7808 SHA512 cf79b05d43ebdc8fd8081899a1f853370de051cafe6e5b143eaff9827efc542b58062782a3ce2a3d1a03561a9ffd780c9cdc645bb50036eb61e80fa729136e64 WHIRLPOOL a5117e7bc81aeecb6fa34d8e2dea70b379d9e3463957e7029c80957ff3bcdd3107a99fb0dabfe59b57bfdb16ed51a0a4781c8dbf8e3f6f225ebd5035c1a9ff79
+DIST minisat-2.2.0_p20130925.tar.gz 49544 SHA256 3db05b02f91c4b097b7962e523225aa5e6fa9a6c0d42704a170b01b069cdfcfe SHA512 37fc35cc4f3104d7f0e8ee9f7123fc34e175df578658266799d809d71d6cf081e811919f304a02f6cb9c3827d308e59408149d63d1d1e7c6d0b495350f93b3d9 WHIRLPOOL c976fabadb2149e15260025646e465d7422ffb9fd35e37263766002462de7b8d16db031aacb1458467acd9957eb370894d39ea3a7ddc5c98627f84b0a08b7820
+EBUILD minisat-2.2.0-r4.ebuild 1353 SHA256 a5e06a513d7aac1c7b1f90d59950989e04550bdda8637fb01bdaa032e3c85251 SHA512 d763d57490d349f400f62c5516d99f14df57cf1aa03ec14d0d1035f5e0042ab17a3007637f336bec520295b388e960c0f67d5a6e81a13c90f984d13a43784f9c WHIRLPOOL 2b9ff15bf280a0841780246c3a562b3824ffdd3449357a9555306c20cdc487529a16b2d80773e23b9eba8bd91afbfe39e2386d4fc81d43170d4deb15a1850ad5
+EBUILD minisat-2.2.0_p20130925.ebuild 1604 SHA256 bcc133ffef459fa77716d527c479c83916ce004ad23be2f2bdac8e844fbbbebc SHA512 5214b3ea329966412499728ca437ad49540476284200e634fbfcc36346615e58c07fb1990c679edec7283a7fd2a3c71f2bc2ff7c1e8dadd5c0ea2466f42ce820 WHIRLPOOL 9969adc8a7c7ff8b437dc927dc390974a4c05ebb43c00daa7842777918afe99e32682ba2d33eded2e40a3f12fe4e8496e882d5dc6dbfa1624713e47702321d73
+MISC ChangeLog 3820 SHA256 ec7ce24bae115c4a63beeb290aee9d2c731969c9079f71bfa476153f68c1c251 SHA512 f3e98aea2cbb17e4d52837cf39432cb848039401c95ba5bfa04f25ae62f6ce54d69d6f2998e0c5bcec2ce9836c90a2b457a077718f756254a3b2e08b93b23b85 WHIRLPOOL cf9b2cab0fd01b1b80145f8399bbb2bcd2ce86edbb84132c5d627347936e59d4d4dc28afec6d665c28646f44393674cae4d86d2959429795ec2a123142ef9c66
+MISC ChangeLog-2015 2048 SHA256 755dba04a91cf19ee74cc317b16de162abd38df5887969688b8201a3964b0bd1 SHA512 3c781eb23c4310a6b58b1ad28fca3ae384825f728876853358cf1b83dd04b8710d35a9b69e9fce24b51988c016d1bc758ea14885dbd030cccdeb7ae815180b6c WHIRLPOOL ecae4fb62b9b3f35405a10056660c8871d84e0339e6d8f4dc63e239291a1877355955cde1d612b461327c8125f17c60a64a20d1a75dbee2362c208d9e2f0b903
+MISC metadata.xml 451 SHA256 30cde76f469ab7b407fd6c028f089c7502ac73b571c8c38203f7932b2cab0a35 SHA512 366989ee424c843bf3239bb16f0afa46393dd7fdf2c131a8de6d7bf6ab29fc5db71b3cf47f6acf5923bb4bbcf8244eb655ce465555ea8e17203048be536020e2 WHIRLPOOL 028d60cc31e492bb1ff7a1df0582acc89071337a6bccea40909a83fd1a0fbcebe5393737c14ec0165f021175a70110af813c2762ad7ec2d805c21682616f9819
diff --git a/sci-mathematics/minisat/files/minisat-2.2.0-header_fix.patch b/sci-mathematics/minisat/files/minisat-2.2.0-header_fix.patch
new file mode 100644
index 000000000000..486c012fe2a4
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.0-header_fix.patch
@@ -0,0 +1,160 @@
+--- ./utils/System.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./utils/System.h	2011-04-12 18:33:41.000000000 -0700
+@@ -25,7 +25,7 @@
+ #include <fpu_control.h>
+ #endif
+ 
+-#include "mtl/IntTypes.h"
++#include <mtl/IntTypes.h>
+ 
+ //-------------------------------------------------------------------------------------------------
+ 
+--- ./utils/Options.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./utils/Options.h	2011-04-12 18:34:38.000000000 -0700
+@@ -25,9 +25,9 @@
+ #include <math.h>
+ #include <string.h>
+ 
+-#include "mtl/IntTypes.h"
+-#include "mtl/Vec.h"
+-#include "utils/ParseUtils.h"
++#include <mtl/IntTypes.h>
++#include <mtl/Vec.h>
++#include "ParseUtils.h"
+ 
+ namespace Minisat {
+ 
+--- ./core/SolverTypes.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./core/SolverTypes.h	2011-04-12 18:27:58.000000000 -0700
+@@ -24,11 +24,11 @@
+ 
+ #include <assert.h>
+ 
+-#include "mtl/IntTypes.h"
+-#include "mtl/Alg.h"
+-#include "mtl/Vec.h"
+-#include "mtl/Map.h"
+-#include "mtl/Alloc.h"
++#include <mtl/IntTypes.h>
++#include <mtl/Alg.h>
++#include <mtl/Vec.h>
++#include <mtl/Map.h>
++#include <mtl/Alloc.h>
+ 
+ namespace Minisat {
+ 
+--- ./core/Solver.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./core/Solver.h	2011-04-12 18:26:56.000000000 -0700
+@@ -21,11 +21,11 @@
+ #ifndef Minisat_Solver_h
+ #define Minisat_Solver_h
+ 
+-#include "mtl/Vec.h"
+-#include "mtl/Heap.h"
+-#include "mtl/Alg.h"
+-#include "utils/Options.h"
+-#include "core/SolverTypes.h"
++#include <mtl/Vec.h>
++#include <mtl/Heap.h>
++#include <mtl/Alg.h>
++#include <utils/Options.h>
++#include "SolverTypes.h"
+ 
+ 
+ namespace Minisat {
+--- ./mtl/Vec.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Vec.h	2011-04-12 18:30:50.000000000 -0700
+@@ -24,8 +24,8 @@
+ #include <assert.h>
+ #include <new>
+ 
+-#include "mtl/IntTypes.h"
+-#include "mtl/XAlloc.h"
++#include "IntTypes.h"
++#include "XAlloc.h"
+ 
+ namespace Minisat {
+ 
+--- ./mtl/Sort.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Sort.h	2011-04-12 18:31:05.000000000 -0700
+@@ -21,7 +21,7 @@
+ #ifndef Minisat_Sort_h
+ #define Minisat_Sort_h
+ 
+-#include "mtl/Vec.h"
++#include "Vec.h"
+ 
+ //=================================================================================================
+ // Some sorting algorithms for vec's
+--- ./mtl/Alg.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Alg.h	2011-04-12 18:32:26.000000000 -0700
+@@ -21,7 +21,7 @@
+ #ifndef Minisat_Alg_h
+ #define Minisat_Alg_h
+ 
+-#include "mtl/Vec.h"
++#include "Vec.h"
+ 
+ namespace Minisat {
+ 
+--- ./mtl/Alloc.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Alloc.h	2011-04-12 18:32:18.000000000 -0700
+@@ -21,8 +21,8 @@
+ #ifndef Minisat_Alloc_h
+ #define Minisat_Alloc_h
+ 
+-#include "mtl/XAlloc.h"
+-#include "mtl/Vec.h"
++#include "XAlloc.h"
++#include "Vec.h"
+ 
+ namespace Minisat {
+ 
+--- ./mtl/Heap.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Heap.h	2011-04-12 18:32:05.000000000 -0700
+@@ -21,7 +21,7 @@
+ #ifndef Minisat_Heap_h
+ #define Minisat_Heap_h
+ 
+-#include "mtl/Vec.h"
++#include "Vec.h"
+ 
+ namespace Minisat {
+ 
+--- ./mtl/Map.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Map.h	2011-04-12 18:31:36.000000000 -0700
+@@ -20,8 +20,8 @@
+ #ifndef Minisat_Map_h
+ #define Minisat_Map_h
+ 
+-#include "mtl/IntTypes.h"
+-#include "mtl/Vec.h"
++#include "IntTypes.h"
++#include "Vec.h"
+ 
+ namespace Minisat {
+ 
+--- ./mtl/Queue.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./mtl/Queue.h	2011-04-12 18:31:18.000000000 -0700
+@@ -21,7 +21,7 @@
+ #ifndef Minisat_Queue_h
+ #define Minisat_Queue_h
+ 
+-#include "mtl/Vec.h"
++#include "Vec.h"
+ 
+ namespace Minisat {
+ 
+--- ./simp/SimpSolver.h.orig	2010-07-10 09:07:36.000000000 -0700
++++ ./simp/SimpSolver.h	2011-04-12 18:35:20.000000000 -0700
+@@ -21,8 +21,8 @@
+ #ifndef Minisat_SimpSolver_h
+ #define Minisat_SimpSolver_h
+ 
+-#include "mtl/Queue.h"
+-#include "core/Solver.h"
++#include <mtl/Queue.h>
++#include <core/Solver.h>
+ 
+ 
+ namespace Minisat {
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
new file mode 100644
index 000000000000..4b17c8fb44bb
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
@@ -0,0 +1,527 @@
+--- 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/metadata.xml b/sci-mathematics/minisat/metadata.xml
new file mode 100644
index 000000000000..1d99050d0a59
--- /dev/null
+++ b/sci-mathematics/minisat/metadata.xml
@@ -0,0 +1,15 @@
+<?xml version='1.0' encoding='UTF-8'?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+	<maintainer type="project">
+		<email>sci@gentoo.org</email>
+		<name>Gentoo Science Project</name>
+	</maintainer>
+	<use>
+		<flag name="extended-solver">Build extended version of SAT solver with
+ additional features.</flag>
+	</use>
+	<upstream>
+		<remote-id type="github">niklasso/minisat</remote-id>
+	</upstream>
+</pkgmetadata>
diff --git a/sci-mathematics/minisat/minisat-2.2.0-r4.ebuild b/sci-mathematics/minisat/minisat-2.2.0-r4.ebuild
new file mode 100644
index 000000000000..2bbc706d240a
--- /dev/null
+++ b/sci-mathematics/minisat/minisat-2.2.0-r4.ebuild
@@ -0,0 +1,65 @@
+# Copyright 1999-2016 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=6
+
+inherit toolchain-funcs
+
+DESCRIPTION="Small yet efficient SAT solver with reference paper"
+HOMEPAGE="http://minisat.se/Main.html"
+SRC_URI="http://minisat.se/downloads/${P}.tar.gz
+	doc? ( http://minisat.se/downloads/MiniSat.pdf )"
+
+SLOT="0"
+KEYWORDS="~amd64 ~x86 ~amd64-linux ~x86-linux"
+LICENSE="MIT"
+
+IUSE="debug doc extended-solver"
+
+DEPEND="sys-libs/zlib"
+RDEPEND="${DEPEND}"
+
+DOCS=( README doc/ReleaseNotes-2.2.0.txt )
+PATCHES=( "${FILESDIR}"/${P}-header_fix.patch )
+
+S=${WORKDIR}/${PN}
+
+src_prepare() {
+	default
+	# Remove makefile silencing
+	sed -i -e 's:@\(\$\|ln\|rm\|for\):\1:g'	mtl/template.mk || die
+}
+
+src_configure() {
+	myconf=$(usex debug d r)
+	myext=$(usex debug debug release)
+	mydir=$(usex extended-solver simp core)
+
+	tc-export CXX
+}
+
+src_compile() {
+	export MROOT="$S"
+	emake -C $mydir $myconf
+	LIB="${PN}" emake -C $mydir lib$myconf
+}
+
+src_install() {
+	insinto /usr/include/${PN}2/mtl
+	doins mtl/*.h
+
+	insinto /usr/include/${PN}2/core
+	doins core/Solver*.h
+
+	insinto /usr/include/${PN}2/simp
+	doins simp/Simp*.h
+
+	insinto /usr/include/${PN}2/utils
+	doins utils/*.h
+
+	newbin ${mydir}/${PN}_${myext} ${PN}
+	newlib.a ${mydir}/lib${PN}_${myext}.a lib${PN}.a
+
+	use doc && DOCS+=( "${DISTDIR}"/MiniSat.pdf )
+	einstalldocs
+}
diff --git a/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild b/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild
new file mode 100644
index 000000000000..308bc18e8afd
--- /dev/null
+++ b/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild
@@ -0,0 +1,57 @@
+# 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 <\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
+}