summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abclib.dsp4
-rw-r--r--src/aig/llb/llb3Nonlin.c69
-rw-r--r--src/misc/hash/hashGen.h3
-rw-r--r--src/misc/util/utilSignal.c12
4 files changed, 41 insertions, 47 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 3668cb51..dc59fcd6 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2365,6 +2365,10 @@ SOURCE=.\src\misc\util\utilMem.c
SOURCE=.\src\misc\util\utilMem.h
# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\utilSignal.c
+# End Source File
# End Group
# Begin Group "nm"
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index 18562f5f..88bee63e 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -80,74 +80,59 @@ extern int nSuppMax;
***********************************************************************/
int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
{
+ int fVerbose = 0;
Aig_Obj_t * pObj;
-// Vec_Int_t * vVars;
DdNode * bCof, * bVar, * bTemp;
- int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY;
+ int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
int Size, Size0, Size1;
int clk = clock();
-// vVars = Vec_IntStartNatural( Cudd_ReadSize(dd) );
- printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
- Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
-// Vec_IntForEachEntry( vVars, iVar, i )
-
+ Size = Cudd_DagSize(bFunc);
+// printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
+// Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = Aig_ObjId(pObj);
-/*
- printf( "Var =%3d : ", iVar );
- bVar = Cudd_bddIthVar(dd, iVar);
- bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
-// bCof = Cudd_bddAnd( dd, bTemp = bCof, Cudd_Not(bVar) ); Cudd_Ref( bCof );
-// Cudd_RecursiveDeref( dd, bTemp );
- printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
- printf( "Size0 =%6d ", Size0 = Cudd_DagSize(bCof) );
- Cudd_RecursiveDeref( dd, bCof );
-
- bCof = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof );
-// bCof = Cudd_bddAnd( dd, bTemp = bCof, bVar ); Cudd_Ref( bCof );
-// Cudd_RecursiveDeref( dd, bTemp );
- printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
- printf( "Size1 =%6d ", Size1 = Cudd_DagSize(bCof) );
- Cudd_RecursiveDeref( dd, bCof );
-
- printf( "D =%6d ", Size0 + Size1 - Size );
- printf( "B =%6d\n", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
-*/
-
-// printf( "Var =%3d : ", iVar );
+ if ( fVerbose )
+ printf( "Var =%3d : ", iVar );
bVar = Cudd_bddIthVar(dd, iVar);
bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
bCof = Cudd_bddAnd( dd, bTemp = bCof, Cudd_Not(bVar) ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bTemp );
Size0 = Cudd_DagSize(bCof);
-// printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
-// printf( "Size0 =%6d ", Size0 );
+ if ( fVerbose )
+ printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
+ if ( fVerbose )
+ printf( "Size0 =%6d ", Size0 );
Cudd_RecursiveDeref( dd, bCof );
bCof = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof );
bCof = Cudd_bddAnd( dd, bTemp = bCof, bVar ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bTemp );
Size1 = Cudd_DagSize(bCof);
-// printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
-// printf( "Size1 =%6d ", Size1 );
+ if ( fVerbose )
+ printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
+ if ( fVerbose )
+ printf( "Size1 =%6d ", Size1 );
Cudd_RecursiveDeref( dd, bCof );
iValue = ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) + Size0 + Size1 - Size;
-// printf( "D =%6d ", Size0 + Size1 - Size );
-// printf( "B =%6d ", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
-// printf( "S =%6d\n", iValue );
+ if ( fVerbose )
+ printf( "D =%6d ", Size0 + Size1 - Size );
+ if ( fVerbose )
+ printf( "B =%6d ", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
+ if ( fVerbose )
+ printf( "S =%6d\n", iValue );
if ( iValueBest > iValue )
{
iValueBest = iValue;
- iVarBest = i;
+ iVarBest = iVar;
+ Size0Best = Size0;
}
}
-// Vec_IntFree( vVars );
- printf( "Best var = %d. Best value = %d. ", iVarBest, iValueBest );
+ printf( "BestVar = %4d. Value =%6d. Orig =%6d. Size0 =%6d. ", iVarBest, iValueBest, Size, Size0Best );
Abc_PrintTime( 1, "Time", clock() - clk );
return iVarBest;
}
@@ -424,12 +409,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
{
int iVar;
DdNode * bVar;
+ int nDagSize;
// if ( !p->pPars->fSilent )
// printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
// p->pPars->iFrame = nIters - 1;
// return -1;
bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent );
+ nDagSize = Cudd_DagSize(bCurrent);
iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
bVar = Cudd_bddIthVar(p->dd, iVar);
@@ -438,6 +425,10 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
Cudd_RecursiveDeref( p->dd, bTemp );
bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
+
+// printf( "Before = %6d. After = %6d.\n", nDagSize, Cudd_DagSize(bCurrent) );
+
+ p->pPars->nBddMax = 3 * p->pPars->nBddMax / 2;
continue;
}
Cudd_Ref( bNext );
diff --git a/src/misc/hash/hashGen.h b/src/misc/hash/hashGen.h
index 33359e89..257b9dba 100644
--- a/src/misc/hash/hashGen.h
+++ b/src/misc/hash/hashGen.h
@@ -87,7 +87,7 @@ struct Hash_Gen_t_
***********************************************************************/
static int Hash_DefaultHashFuncStr( void * key, int nBins )
{
- char* p = (const char*)key;
+ const char* p = (const char*)key;
int h=0;
for( ; *p ; ++p )
@@ -151,7 +151,6 @@ static inline Hash_Gen_t * Hash_GenAlloc(
int fFreeKey)
{
Hash_Gen_t * p;
- int i;
assert(nBins > 0);
p = ABC_CALLOC( Hash_Gen_t, 1 );
p->nBins = nBins;
diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c
index 2b2d538c..6a793ce0 100644
--- a/src/misc/util/utilSignal.c
+++ b/src/misc/util/utilSignal.c
@@ -18,19 +18,19 @@
***********************************************************************/
-#ifndef _MSC_VER
-
#include <main.h>
#include <stdlib.h>
-#include <unistd.h>
#include <signal.h>
-#include <hashGen.h>
+#include "abc_global.h"
+#include "hashGen.h"
+
+#ifndef _MSC_VER
+
+#include <unistd.h>
#include <errno.h>
#include <sys/types.h>
#include <sys/wait.h>
-#include "abc_global.h"
-
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////