diff options
author | Petr Rockai <me@mornfall.net> | 2014-01-12 13:22:58 +0100 |
---|---|---|
committer | Petr Rockai <me@mornfall.net> | 2014-01-25 16:33:12 +0100 |
commit | ed5bd26574c43246920fdf814e997b86c7b50fff (patch) | |
tree | 2587cd67c5e3bc17b0f08d0f5c15bee554aa651b /pkgs/applications/science/logic/stp | |
parent | e3fae16a298f3a7741c41df142245a75e6249365 (diff) | |
download | nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar.gz nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar.bz2 nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar.lz nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar.xz nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.tar.zst nixpkgs-ed5bd26574c43246920fdf814e997b86c7b50fff.zip |
STP: Simple Theorem Prover (a SMT solver for bitvectors & arrays).
Diffstat (limited to 'pkgs/applications/science/logic/stp')
-rw-r--r-- | pkgs/applications/science/logic/stp/default.nix | 23 | ||||
-rw-r--r-- | pkgs/applications/science/logic/stp/fixbuild.diff | 45 | ||||
-rw-r--r-- | pkgs/applications/science/logic/stp/fixrefs.diff | 192 |
3 files changed, 260 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix new file mode 100644 index 00000000000..cfe96bc6983 --- /dev/null +++ b/pkgs/applications/science/logic/stp/default.nix @@ -0,0 +1,23 @@ +{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; + }; +} diff --git a/pkgs/applications/science/logic/stp/fixbuild.diff b/pkgs/applications/science/logic/stp/fixbuild.diff new file mode 100644 index 00000000000..01782cb4f40 --- /dev/null +++ b/pkgs/applications/science/logic/stp/fixbuild.diff @@ -0,0 +1,45 @@ +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 new file mode 100644 index 00000000000..60ad4949f07 --- /dev/null +++ b/pkgs/applications/science/logic/stp/fixrefs.diff @@ -0,0 +1,192 @@ +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************************************************************* + |