philipp/nixpkgs
1
0
Fork 0
Code Issues Pull requests Projects Releases Activity
nixpkgs/pkgs/applications/science/logic/stp/fixrefs.diff

193 lines
7.1 KiB
Diff
Raw Normal View History

STP: Simple Theorem Prover (a SMT solver for bitvectors & arrays).
2014-01-12 13:22:58 +01:00
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*************************************************************
Reference in a new issue Copy permalink