STP: Simple Theorem Prover (a SMT solver for bitvectors & arrays).

pkgs/applications/science/logic/stp/default.nix

···
+{stdenv, cmake, boost, bison, flex, fetchgit, perl, zlib}: 
+stdenv.mkDerivation rec {
+  version = "2014.01.07";
+  name = "stp-${version}";
+  src = fetchgit {
+    url    = "git://github.com/stp/stp";
+    rev    = "3aa11620a823d617fc033d26aedae91853d18635";
+    sha256 = "832520787f57f63cf47364d080f30ad10d6d6e00f166790c19b125be3d6dd45c";
+  };
+  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}
+  '';
+  meta = {
+    description = ''Simple Theorem Prover'';
+    maintainers = with stdenv.lib.maintainers; [mornfall];
+    platforms = with stdenv.lib.platforms; linux;
+    license = with stdenv.lib.licenses; mit;
+  };
+}

pkgs/applications/science/logic/stp/fixbuild.diff

···
+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
+ # -----------------------------------------------------------------------------

pkgs/applications/science/logic/stp/fixrefs.diff

···
+commit 53b6043e25b2eba264faab845077fbf6736cf22f
+Author: Petr Rockai <[e-mail]>
+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*************************************************************
+ 

pkgs/top-level/all-packages.nix

···
 
   stalonetray = callPackage ../applications/window-managers/stalonetray {};
 
+  stp = callPackage ../applications/science/logic/stp {};
+
   stumpwm = lispPackages.stumpwm;
 
   sublime = callPackage ../applications/editors/sublime { };