summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/kit/kitTruth.c19
-rw-r--r--src/base/abci/abc.c25
-rw-r--r--src/base/abci/abcRec.c18
-rw-r--r--src/base/abci/module.make1
4 files changed, 31 insertions, 32 deletions
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 56f10ac0..5b467c00 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -1658,20 +1658,20 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
{
// short pStore2[32];
unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
-// int nWords = Kit_TruthWordNum( nVars );
- int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
unsigned uCanonPhase;
// canonicize output
uCanonPhase = 0;
-/*
+
nOnes = Kit_TruthCountOnes(pIn, nVars);
if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
{
uCanonPhase |= (1 << nVars);
Kit_TruthNot( pIn, pIn, nVars );
}
-*/
+
// collect the minterm counts
Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
/*
@@ -1698,7 +1698,6 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
// permute
Counter = 0;
-
do {
fChange = 0;
for ( i = 0; i < nVars-1; i++ )
@@ -1721,11 +1720,11 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
pStore[2*(i+1)+1] = Temp;
// if the polarity of variables is different, swap them
-// if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
-// {
-// uCanonPhase ^= (1 << i);
-// uCanonPhase ^= (1 << (i+1));
-// }
+ if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << (i+1));
+ }
Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
pTemp = pIn; pIn = pOut; pOut = pTemp;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ac0f26dd..daf92b1b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -206,11 +206,11 @@ static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, cha
//static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecAdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecAdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -662,11 +662,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Choicing", "haig_stop", Abc_CommandHaigStop, 0 );
// Cmd_CommandAdd( pAbc, "Choicing", "haig_use", Abc_CommandHaigUse, 1 );
-// Cmd_CommandAdd( pAbc, "Choicing", "rec_start", Abc_CommandRecStart, 0 );
-// Cmd_CommandAdd( pAbc, "Choicing", "rec_stop", Abc_CommandRecStop, 0 );
-// Cmd_CommandAdd( pAbc, "Choicing", "rec_add", Abc_CommandRecAdd, 0 );
-// Cmd_CommandAdd( pAbc, "Choicing", "rec_ps", Abc_CommandRecPs, 0 );
-// Cmd_CommandAdd( pAbc, "Choicing", "rec_use", Abc_CommandRecUse, 1 );
+ Cmd_CommandAdd( pAbc, "Choicing", "rec_start", Abc_CommandRecStart, 0 );
+ Cmd_CommandAdd( pAbc, "Choicing", "rec_stop", Abc_CommandRecStop, 0 );
+ Cmd_CommandAdd( pAbc, "Choicing", "rec_add", Abc_CommandRecAdd, 0 );
+ Cmd_CommandAdd( pAbc, "Choicing", "rec_ps", Abc_CommandRecPs, 0 );
+ Cmd_CommandAdd( pAbc, "Choicing", "rec_use", Abc_CommandRecUse, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "amap", Abc_CommandAmap, 1 );
@@ -11887,6 +11887,7 @@ usage:
return 1;
}
+#endif
/**Function*************************************************************
@@ -11909,7 +11910,7 @@ int Abc_CommandRecStart( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
- nVars = 4;
+ nVars = 6;
nCuts = 8;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCh" ) ) != EOF )
@@ -12155,8 +12156,6 @@ usage:
return 1;
}
-#endif
-
/**Function*************************************************************
Synopsis []
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 47380da1..33fd9e82 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -237,7 +237,7 @@ p->timeTruth += clock() - clk;
// add the resulting truth table to the hash table
ppSpot = Abc_NtkRecTableLookup( p, pTruth, p->nVars );
- assert( pObj->pEquiv == NULL );
+ assert( pObj->pData == NULL );
assert( pObj->pCopy == NULL );
if ( *ppSpot == NULL )
{
@@ -246,8 +246,8 @@ p->timeTruth += clock() - clk;
}
else
{
- pObj->pEquiv = (*ppSpot)->pEquiv;
- (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+ pObj->pData = (*ppSpot)->pData;
+ (*ppSpot)->pData = (Hop_Obj_t *)pObj;
if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
printf( "Loop!\n" );
}
@@ -362,7 +362,7 @@ void Abc_NtkRecPs()
{
Counters[ Abc_ObjGetMax(pEntry) ]++;
Counter++;
- for ( pTemp = pEntry; pTemp; pTemp = (Abc_Obj_t *)pTemp->pEquiv )
+ for ( pTemp = pEntry; pTemp; pTemp = (Abc_Obj_t *)pTemp->pData )
{
assert( Abc_ObjGetMax(pTemp) == Abc_ObjGetMax(pEntry) );
CountersS[ Abc_ObjGetMax(pTemp) ]++;
@@ -935,7 +935,7 @@ s_pMan->timeCanon += clock() - clk;
// add the resulting truth table to the hash table
ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
- assert( pObj->pEquiv == NULL );
+ assert( pObj->pData == NULL );
assert( pObj->pCopy == NULL );
if ( *ppSpot == NULL )
{
@@ -944,8 +944,8 @@ s_pMan->timeCanon += clock() - clk;
}
else
{
- pObj->pEquiv = (*ppSpot)->pEquiv;
- (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+ pObj->pData = (*ppSpot)->pData;
+ (*ppSpot)->pData = pObj;
if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
printf( "Loop!\n" );
}
@@ -1104,7 +1104,7 @@ int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTru
}
// go through the candidates - and recursively label them
- for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+ for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pData )
Abc_NtkRecStrashNodeLabel_rec( pNtkNew, pCand, 0, s_pMan->vLabels );
@@ -1120,7 +1120,7 @@ int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTru
// find the best subgraph
CostMin = ABC_INFINITY;
pCandMin = NULL;
- for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+ for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pData )
{
// label the leaves
Abc_NtkIncrementTravId( pAig );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b0223330..965e0258 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -42,6 +42,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcProve.c \
src/base/abci/abcQbf.c \
src/base/abci/abcQuant.c \
+ src/base/abci/abcRec.c \
src/base/abci/abcReconv.c \
src/base/abci/abcReach.c \
src/base/abci/abcRefactor.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 06:14:24 +0000