stp: 2014.01.07 -> 2.2.0

3 files changed, 26 insertions, 254 deletions

diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix
index 444bb06c4a00..8c0b82cc549c 100644
--- a/pkgs/applications/science/logic/stp/default.nix
+++ b/pkgs/applications/science/logic/stp/default.nix
@@ -1,23 +1,32 @@
-{stdenv, cmake, boost, bison, flex, fetchgit, perl, zlib}: 
+{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }:
+
 stdenv.mkDerivation rec {
-  version = "2014.01.07";
+  version = "2.2.0";
   name = "stp-${version}";
-  src = fetchgit {
-    url    = "git://github.com/stp/stp";
-    rev    = "3aa11620a823d617fc033d26aedae91853d18635";
-    sha256 = "832520787f57f63cf47364d080f30ad10d6d6e00f166790c19b125be3d6dd45c";
+
+  src = fetchFromGitHub {
+    owner = "stp";
+    repo = "stp";
+    rev    = "stp-${version}";
+    sha256 = "1jh23wjm62nnqfx447g2y53bbangq04hjrvqc35v9xxpcjgj3i49";
   };
-  buildInputs = [ cmake boost bison flex perl zlib ];
-  cmakeFlags = [ "-DBUILD_SHARED_LIBS=ON" ];
-  patchPhase = ''
-      sed -e 's,^export(PACKAGE.*,,' -i CMakeLists.txt
-      patch -p1 < ${./fixbuild.diff}
-      patch -p1 < ${./fixrefs.diff}
+
+  buildInputs = [ boost zlib minisatUnstable cryptominisat python3 ];
+  nativeBuildInputs = [ cmake bison flex perl ];
+  preConfigure = ''
+    python_install_dir=$out/${python3Packages.python.sitePackages}
+    mkdir -p $python_install_dir
+    cmakeFlagsArray=(
+      $cmakeFlagsArray
+      "-DBUILD_SHARED_LIBS=ON"
+      "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir"
+    )
   '';
-  meta = {
-    description = ''Simple Theorem Prover'';
-    maintainers = with stdenv.lib.maintainers; [mornfall];
-    platforms = with stdenv.lib.platforms; linux;
-    license = stdenv.lib.licenses.mit;
+
+  meta = with stdenv.lib; {
+    description = "Simple Theorem Prover";
+    maintainers = with maintainers; [ mornfall ];
+    platforms = platforms.linux;
+    license = licenses.mit;
   };
 }
diff --git a/pkgs/applications/science/logic/stp/fixbuild.diff b/pkgs/applications/science/logic/stp/fixbuild.diff
deleted file mode 100644
index 01782cb4f40b..000000000000
--- a/pkgs/applications/science/logic/stp/fixbuild.diff
+++ /dev/null
@@ -1,45 +0,0 @@
-diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt
-index 83bd03a..9c0304b 100644
---- a/src/libstp/CMakeLists.txt
-+++ b/src/libstp/CMakeLists.txt
-@@ -23,6 +23,15 @@ set(stp_lib_targets
-     printer
- )
- 
-+include_directories(${CMAKE_SOURCE_DIR}/src/AST/)
-+include_directories(${CMAKE_BINARY_DIR}/src/AST/)
-+
-+add_library(globalstp OBJECT
-+    ../main/Globals.cpp
-+    ${CMAKE_CURRENT_BINARY_DIR}/../main/GitSHA1.cpp
-+)
-+add_dependencies(globalstp ASTKind_header)
-+
- # Create list of objects and gather list of
- # associated public headers.
- set(stp_lib_objects "")
-@@ -31,6 +40,7 @@ foreach(target ${stp_lib_targets})
-     list(APPEND stp_lib_objects $<TARGET_OBJECTS:${target}>)
- 
-     get_target_property(TARGETS_PUBLIC_HEADERS ${target} PUBLIC_HEADER)
-+    set_target_properties(${target} PROPERTIES POSITION_INDEPENDENT_CODE ON)
-     if (EXISTS "${TARGETS_PUBLIC_HEADERS}")
-         list(APPEND stp_public_headers "${TARGETS_PUBLIC_HEADERS}")
-         message("Adding public header(s) ${TARGETS_PUBLIC_HEADERS} to target libstp")
-diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
-index 0735137..73039f5 100644
---- a/src/main/CMakeLists.txt
-+++ b/src/main/CMakeLists.txt
-@@ -3,12 +3,6 @@ include_directories(${CMAKE_BINARY_DIR}/src/AST/)
- 
- configure_file("${CMAKE_CURRENT_SOURCE_DIR}/GitSHA1.cpp.in" "${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp" @ONLY)
- 
--add_library(globalstp OBJECT
--    Globals.cpp
--    ${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp
--)
--add_dependencies(globalstp ASTKind_header)
--
- # -----------------------------------------------------------------------------
- # Create binary
- # -----------------------------------------------------------------------------
diff --git a/pkgs/applications/science/logic/stp/fixrefs.diff b/pkgs/applications/science/logic/stp/fixrefs.diff
deleted file mode 100644
index 60ad4949f076..000000000000
--- a/pkgs/applications/science/logic/stp/fixrefs.diff
+++ /dev/null
@@ -1,192 +0,0 @@
-commit 53b6043e25b2eba264faab845077fbf6736cf22f
-Author: Petr Rockai <me@mornfall.net>
-Date:   Tue Jan 7 13:30:07 2014 +0100
-
-    aig: Comment out unused functions with undefined references in them.
-
-diff --git a/src/extlib-abc/aig/aig/aigPart.c b/src/extlib-abc/aig/aig/aigPart.c
-index a4cc116..5bd5f08 100644
---- a/src/extlib-abc/aig/aig/aigPart.c
-+++ b/src/extlib-abc/aig/aig/aigPart.c
-@@ -869,6 +869,7 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )

- {

-     extern int Cmd_CommandExecute( void * pAbc, char * sCommand );

-@@ -981,6 +982,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
-     Aig_ManMarkValidChoices( pAig );

-     return pAig;

- }

-+#endif

- 

- 

- ////////////////////////////////////////////////////////////////////////

-diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c
-index ae8fa8b..f04eedc 100644
---- a/src/extlib-abc/aig/aig/aigShow.c
-+++ b/src/extlib-abc/aig/aig/aigShow.c
-@@ -326,6 +326,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )

- {

-     extern void Abc_ShowFile( char * FileNameDot );

-@@ -347,7 +348,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
-     // visualize the file 

-     Abc_ShowFile( FileNameDot );

- }

--

-+#endif

- 

- ////////////////////////////////////////////////////////////////////////

- ///                       END OF FILE                                ///

-diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c
-index d744b4f..23fc3d5 100644
---- a/src/extlib-abc/aig/dar/darRefact.c
-+++ b/src/extlib-abc/aig/dar/darRefact.c
-@@ -340,6 +340,7 @@ printf( "\n" );
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required )

- {

-     Vec_Ptr_t * vCut;

-@@ -428,6 +429,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
-     }

-     return p->GainBest;

- }

-+#endif

- 

- /**Function*************************************************************

- 

-@@ -461,6 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
-   SeeAlso     []

-  

- ***********************************************************************/

-+#if 0

- int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )

- {

- //    Bar_Progress_t * pProgress;

-@@ -583,6 +586,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
-     return 1;

- 

- }

-+#endif

- 

- ////////////////////////////////////////////////////////////////////////

- ///                       END OF FILE                                ///

-diff --git a/src/extlib-abc/aig/dar/darScript.c b/src/extlib-abc/aig/dar/darScript.c
-index e60df00..1b9c24f 100644
---- a/src/extlib-abc/aig/dar/darScript.c
-+++ b/src/extlib-abc/aig/dar/darScript.c
-@@ -64,6 +64,7 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )

- //alias rwsat       "st; rw -l; b -l; rw -l; rf -l"

- {

-@@ -108,7 +109,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
- 

-     return pAig;

- }

--

-+#endif

- 

- /**Function*************************************************************

- 

-@@ -121,6 +122,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

- //alias compress2   "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"

- {

-@@ -180,6 +182,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
- 

-     return pAig;

- }

-+#endif

- 

- /**Function*************************************************************

- 

-@@ -192,6 +195,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

- //alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"

- {

-@@ -285,6 +289,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
-     }

-     return pAig;

- }

-+#endif

- 

- /**Function*************************************************************

- 

-@@ -297,6 +302,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

- //alias resyn    "b; rw; rwz; b; rwz; b"

- //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"

-@@ -311,6 +317,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
-     Vec_PtrPush( vAigs, pAig );

-     return vAigs;

- }

-+#endif

- 

- /**Function*************************************************************

- 

-diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c
-index de301f2..7e5df0f 100644
---- a/src/extlib-abc/aig/kit/kitAig.c
-+++ b/src/extlib-abc/aig/kit/kitAig.c
-@@ -95,6 +95,7 @@ Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )

- {

-     Aig_Obj_t * pObj;

-@@ -113,6 +114,7 @@ Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * p
-     Kit_GraphFree( pGraph );

-     return pObj;

- }

-+#endif

- 

- ////////////////////////////////////////////////////////////////////////

- ///                       END OF FILE                                ///

-diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c
-index 39ef587..0485c66 100644
---- a/src/extlib-abc/aig/kit/kitGraph.c
-+++ b/src/extlib-abc/aig/kit/kitGraph.c
-@@ -349,6 +349,7 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph )
-   SeeAlso     []

- 

- ***********************************************************************/

-+#if 0

- Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )

- {

-     Kit_Graph_t * pGraph;

-@@ -365,6 +366,7 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
-     pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );

-     return pGraph;

- }

-+#endif

- 

- /**Function*************************************************************

-