summaryrefslogtreecommitdiffstats
path: root/src/opt/sim
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/sim')
-rw-r--r--src/opt/sim/sim.h35
-rw-r--r--src/opt/sim/simMan.c51
-rw-r--r--src/opt/sim/simSupp.c78
-rw-r--r--src/opt/sim/simSwitch.c2
-rw-r--r--src/opt/sim/simSym.c82
-rw-r--r--src/opt/sim/simSymSat.c249
-rw-r--r--src/opt/sim/simSymSim.c48
-rw-r--r--src/opt/sim/simSymStr.c15
-rw-r--r--src/opt/sim/simUtils.c80
9 files changed, 403 insertions, 237 deletions
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 9b4d9699..afed7190 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -21,6 +21,12 @@
#ifndef __SIM_H__
#define __SIM_H__
+/*
+ The ideas realized in this package are described in the paper:
+ "Detecting Symmetries in Boolean Functions using Circuit Representation,
+ Simulation, and Satisfiability".
+*/
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -45,7 +51,8 @@ struct Sym_Man_t_
int nSimWords; // the number of bits in simulation info
Vec_Ptr_t * vSim; // simulation info
// support information
- Vec_Ptr_t * vSuppFun; // functional supports
+ Vec_Ptr_t * vSuppFun; // bit representation
+ Vec_Vec_t * vSupports; // integer representation
// symmetry info for each output
Vec_Ptr_t * vMatrSymms; // symmetric pairs
Vec_Ptr_t * vMatrNonSymms; // non-symmetric pairs
@@ -56,6 +63,14 @@ struct Sym_Man_t_
unsigned * uPatRand;
unsigned * uPatCol;
unsigned * uPatRow;
+ // temporary
+ Vec_Int_t * vVarsU;
+ Vec_Int_t * vVarsV;
+ int iOutput;
+ int iVar1;
+ int iVar2;
+ int iVar1Old;
+ int iVar2Old;
// internal data structures
int nSatRuns;
int nSatRunsSat;
@@ -64,8 +79,12 @@ struct Sym_Man_t_
int nPairsSymm;
int nPairsSymmStr;
int nPairsNonSymm;
+ int nPairsRem;
int nPairsTotal;
// runtime statistics
+ int timeStruct;
+ int timeCount;
+ int timeMatr;
int timeSim;
int timeFraig;
int timeSat;
@@ -91,6 +110,7 @@ struct Sim_Man_t_
Vec_Ptr_t * vSuppFun; // functional supports
// simulation targets
Vec_Vec_t * vSuppTargs; // support targets
+ int iInput; // the input current processed
// internal data structures
Extra_MmFixed_t * pMmPat;
Vec_Ptr_t * vFifo;
@@ -148,7 +168,7 @@ struct Sim_Pat_t_
////////////////////////////////////////////////////////////////////////
/*=== simMan.c ==========================================================*/
-extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk );
+extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
extern void Sym_ManStop( Sym_Man_t * p );
extern void Sym_ManPrintStats( Sym_Man_t * p );
extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk );
@@ -158,11 +178,13 @@ extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p );
extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
/*=== simSupp.c ==========================================================*/
extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
/*=== simSym.c ==========================================================*/
-extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
+extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== simSymSat.c ==========================================================*/
+extern int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
/*=== simSymStr.c ==========================================================*/
-extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs );
+extern void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
/*=== simSymSim.c ==========================================================*/
extern void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
/*=== simUtil.c ==========================================================*/
@@ -180,7 +202,8 @@ extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords );
extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
-extern int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters );
+extern void Sim_UtilCountPairsAll( Sym_Man_t * p );
+extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index 02d59343..780ecfd8 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -40,10 +40,10 @@
SeeAlso []
***********************************************************************/
-Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
+Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
{
Sym_Man_t * p;
- int i;
+ int i, v;
// start the manager
p = ALLOC( Sym_Man_t, 1 );
memset( p, 0, sizeof(Sym_Man_t) );
@@ -69,8 +69,15 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
p->uPatRand = ALLOC( unsigned, p->nSimWords );
p->uPatCol = ALLOC( unsigned, p->nSimWords );
p->uPatRow = ALLOC( unsigned, p->nSimWords );
+ p->vVarsU = Vec_IntStart( 100 );
+ p->vVarsV = Vec_IntStart( 100 );
// compute supports
- p->vSuppFun = Sim_ComputeFunSupp( pNtk );
+ p->vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose );
+ p->vSupports = Vec_VecStart( p->nOutputs );
+ for ( i = 0; i < p->nOutputs; i++ )
+ for ( v = 0; v < p->nInputs; v++ )
+ if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
+ Vec_VecPush( p->vSupports, i, (void *)v );
return p;
}
@@ -92,11 +99,14 @@ void Sym_ManStop( Sym_Man_t * p )
if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun );
if ( p->vSim ) Sim_UtilInfoFree( p->vSim );
if ( p->vNodes ) Vec_PtrFree( p->vNodes );
+ if ( p->vSupports ) Vec_VecFree( p->vSupports );
for ( i = 0; i < p->nOutputs; i++ )
{
Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
}
+ Vec_IntFree( p->vVarsU );
+ Vec_IntFree( p->vVarsV );
Vec_PtrFree( p->vMatrSymms );
Vec_PtrFree( p->vMatrNonSymms );
Vec_IntFree( p->vPairsTotal );
@@ -121,17 +131,18 @@ void Sym_ManStop( Sym_Man_t * p )
***********************************************************************/
void Sym_ManPrintStats( Sym_Man_t * p )
{
- printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n",
- Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
-/*
- printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
- printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
- printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
- printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
-*/
- printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat );
- printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat );
+// printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n",
+// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+ printf( "Total symm = %8d.\n", p->nPairsSymm );
+ printf( "Structural symm = %8d.\n", p->nPairsSymmStr );
+ printf( "Total non-sym = %8d.\n", p->nPairsNonSymm );
+ printf( "Total var pairs = %8d.\n", p->nPairsTotal );
+ printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat );
+ printf( "Sat runs UNSAT = %8d.\n", p->nSatRunsUnsat );
+ PRT( "Structural ", p->timeStruct );
PRT( "Simulation ", p->timeSim );
+ PRT( "Matrix ", p->timeMatr );
+ PRT( "Counting ", p->timeCount );
PRT( "Fraiging ", p->timeFraig );
PRT( "SAT ", p->timeSat );
PRT( "TOTAL ", p->timeTotal );
@@ -217,14 +228,12 @@ void Sim_ManStop( Sim_Man_t * p )
***********************************************************************/
void Sim_ManPrintStats( Sim_Man_t * p )
{
- printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n",
- Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
- printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
- printf( "Total func supps = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
- printf( "Total targets = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
- printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
- printf( "Sat runs SAT = %6d.\n", p->nSatRunsSat );
- printf( "Sat runs UNSAT = %6d.\n", p->nSatRunsUnsat );
+// printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n",
+// Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+ printf( "Total func supps = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
+ printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
+ printf( "Sat runs SAT = %8d.\n", p->nSatRunsSat );
+ printf( "Sat runs UNSAT = %8d.\n", p->nSatRunsUnsat );
PRT( "Simulation ", p->timeSim );
PRT( "Traversal ", p->timeTrav );
PRT( "Fraiging ", p->timeFraig );
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 2f380866..576e19cc 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -99,13 +99,12 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
{
Sim_Man_t * p;
Vec_Ptr_t * vResult;
int nSolved, i, clk = clock();
-// srand( time(NULL) );
srand( 0xABC );
// start the simulation manager
@@ -117,35 +116,40 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
// set the support targets
Sim_ComputeSuppSetTargets( p );
-printf( "Initial targets = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+if ( fVerbose )
+ printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
goto exit;
for ( i = 0; i < 1; i++ )
{
- // compute patterns using one round of random simulation
- Sim_UtilAssignRandom( p );
- nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
- if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
- goto exit;
- }
+ // compute patterns using one round of random simulation
+ Sim_UtilAssignRandom( p );
+ nSolved = Sim_ComputeSuppRound( p, 1 );
+ if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
+ goto exit;
+if ( fVerbose )
+ printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n",
+ Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
+ }
- // simulate until saturation
+ // try to solve the support targets
while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
{
- // solve randomly a given number of targets
+ // solve targets until the first disproved one (which gives counter-example)
Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
// compute additional functional support
-// Sim_UtilAssignRandom( p );
Sim_UtilAssignFromFifo( p );
nSolved = Sim_ComputeSuppRound( p, 1 );
-printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n",
+
+if ( fVerbose )
+ printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n",
Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
}
exit:
+p->timeTotal = clock() - clk;
vResult = p->vSuppFun;
// p->vSuppFun = NULL;
Sim_ManStop( p );
@@ -166,7 +170,6 @@ exit:
int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
{
Vec_Int_t * vTargets;
- Abc_Obj_t * pNode;
int i, Counter = 0;
int clk;
// perform one round of random simulation
@@ -174,7 +177,7 @@ clk = clock();
Sim_UtilSimulate( p, 0 );
p->timeSim += clock() - clk;
// iterate through the CIs and detect COs that depend on them
- Abc_NtkForEachCi( p->pNtk, pNode, i )
+ for ( i = p->iInput; i < p->nInputs; i++ )
{
vTargets = p->vSuppTargs->pArray[i];
if ( fUseTargets && vTargets->nSize == 0 )
@@ -207,7 +210,8 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
int fFirst = 1;
int clk;
// collect nodes by level in the TFO of the CI
- // (this procedure increments TravId of the collected nodes)
+ // this proceduredoes not collect the CIs and COs
+ // but it increments TravId of the collected nodes and CIs/COs
clk = clock();
pNodeCi = Abc_NtkCi( p->pNtk, iNumCi );
vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
@@ -232,13 +236,10 @@ p->timeSim += clock() - clk;
// get the target output
Output = vTargets->pArray[i];
// get the target node
- pNode = Abc_NtkCo( p->pNtk, Output );
+ pNode = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
// the output should be in the cone
assert( Abc_NodeIsTravIdCurrent(pNode) );
- // simulate the node
- Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
-
// skip if the simulation info is equal
if ( Sim_UtilInfoCompare( p, pNode ) )
continue;
@@ -283,12 +284,13 @@ printf( "\n" );
{
if ( !Abc_NodeIsTravIdCurrent( pNode ) )
continue;
- Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
- if ( !Sim_UtilInfoCompare( p, pNode ) )
+ if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
{
if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
+ {
Counter++;
- Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+ Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+ }
}
}
}
@@ -365,7 +367,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
Abc_Obj_t * pNode;
Sim_Pat_t * pPat;
unsigned * pSimInfo;
- int iWord, iWordLim, i, w;
+ int nWordsNew, iWord, iWordLim, i, w;
int iBeg, iEnd;
int Counter = 0;
// go through the patterns and fill in the dist-1 minterms for each
@@ -379,7 +381,7 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
// get the first word of the next series
iWordLim = iWord + 1;
// set the pattern for all PIs from iBit to iWord + p->nInputs
- iBeg = ABC_MAX( 0, pPat->Input - 16 );
+ iBeg = p->iInput;
iEnd = ABC_MIN( iBeg + 32, p->nInputs );
// for ( i = iBeg; i < iEnd; i++ )
Abc_NtkForEachCi( p->pNtk, pNode, i )
@@ -397,9 +399,12 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
}
else
{
+ // get the number of words for the remaining inputs
+ nWordsNew = p->nSuppWords;
+// nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
// get the first word of the next series
- iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords;
- // set the pattern for all PIs from iBit to iWord + p->nInputs
+ iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords;
+ // set the pattern for all CIs from iWord to iWord + nWordsNew
Abc_NtkForEachCi( p->pNtk, pNode, i )
{
pSimInfo = p->vSim0->pArray[pNode->Id];
@@ -413,8 +418,10 @@ void Sim_UtilAssignFromFifo( Sim_Man_t * p )
for ( w = iWord; w < iWordLim; w++ )
pSimInfo[w] = 0;
}
- // flip one bit
Sim_XorBit( pSimInfo + iWord, i );
+ // flip one bit
+// if ( i >= p->iInput )
+// Sim_XorBit( pSimInfo + iWord, i-p->iInput );
}
}
Sim_ManPatFree( p, pPat );
@@ -456,10 +463,11 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
{
p->nSatRuns++;
Output = (int)pEntry;
+
// set up the miter for the two cofactors of this output w.r.t. this input
pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
- // transform the target into a fraig
+ // transform the miter into a fraig
Fraig_ParamsSetDefault( &Params );
Params.fInternal = 1;
clk = clock();
@@ -502,23 +510,23 @@ p->timeSat += clock() - clk;
Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
if ( pModel[v] )
Sim_SetBit( pPat->pData, v );
- Sim_XorBit( pPat->pData, Input ); // flip the given bit
+ Sim_XorBit( pPat->pData, Input ); // add this bit in the opposite polarity
Vec_PtrPush( p->vFifo, pPat );
*/
Counter++;
}
// delete the fraig manager
Fraig_ManFree( pMan );
- // delete the target
+ // delete the miter
Abc_NtkDelete( pMiter );
+ // makr the input, which we are processing
+ p->iInput = Input;
+
// stop when we found enough patterns
// if ( Counter == Limit )
if ( Counter == 1 )
return;
- // switch to the next input if we found one model
- if ( pModel )
- break;
}
}
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index 06b730fc..b43597f3 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -72,8 +72,8 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
vNodes = Abc_AigDfs( pNtk, 1, 0 );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
- Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+ Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
}
Vec_PtrFree( vNodes );
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index 706b13dc..c452bb1b 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -40,52 +40,100 @@
SeeAlso []
***********************************************************************/
-int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk )
+int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
{
Sym_Man_t * p;
Vec_Ptr_t * vResult;
int Result;
- int i, clk = clock();
+ int i, clk, clkTotal = clock();
-// srand( time(NULL) );
srand( 0xABC );
// start the simulation manager
- p = Sym_ManStart( pNtk );
- p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+ p = Sym_ManStart( pNtk, fVerbose );
+ p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
// detect symmetries using circuit structure
- Sim_SymmsStructCompute( pNtk, p->vMatrSymms );
- p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym );
+clk = clock();
+ Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
+p->timeStruct = clock() - clk;
-printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n",
- p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+ Sim_UtilCountPairsAll( p );
+ p->nPairsSymmStr = p->nPairsSymm;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
// detect symmetries using simulation
for ( i = 1; i <= 1000; i++ )
{
- // generate random pattern
- Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
// simulate this pattern
+ Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
- if ( i % 100 != 0 )
+ if ( i % 50 != 0 )
continue;
+ // check disjointness
+ assert( Sim_UtilMatrsAreDisjoint( p ) );
// count the number of pairs
- p->nPairsSymm = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym );
- p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym );
+ Sim_UtilCountPairsAll( p );
+ if ( i % 500 != 0 )
+ continue;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+ }
-printf( "Total = %6d. Sym = %6d. NonSym = %6d. Remaining = %6d.\n",
- p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+ // detect symmetries using SAT
+ for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
+ {
+ // simulate this pattern in four polarities
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1 );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2 );
+/*
+ // try the previuos pair
+ Sim_XorBit( p->uPatRand, p->iVar1Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar2Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+ Sim_XorBit( p->uPatRand, p->iVar1Old );
+ Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+*/
+ if ( i % 10 != 0 )
+ continue;
+ // check disjointness
+ assert( Sim_UtilMatrsAreDisjoint( p ) );
+ // count the number of pairs
+ Sim_UtilCountPairsAll( p );
+ if ( i % 50 != 0 )
+ continue;
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
}
+ // count the number of pairs
+ Sim_UtilCountPairsAll( p );
+ if ( fVerbose )
+ printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n",
+ p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
+
Result = p->nPairsSymm;
vResult = p->vMatrSymms;
+p->timeTotal = clock() - clkTotal;
// p->vMatrSymms = NULL;
Sym_ManStop( p );
return Result;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index 88e33161..db9917b3 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -20,13 +20,14 @@
#include "abc.h"
#include "sim.h"
+#include "fraig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 );
-static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat );
+extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -34,95 +35,88 @@ static int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
/**Function*************************************************************
- Synopsis [Performs the SAT based check.]
+ Synopsis [Tries to prove the remaining pairs using SAT.]
- Description [Given two bit matrices, with symm info and non-symm info,
- checks the remaining pairs.]
+ Description [Continues to prove as long as it encounters symmetric pairs.
+ Returns 1 if a non-symmetric pair is found (which gives a counter-example).
+ Returns 0 if it finishes considering all pairs for all outputs.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym )
+int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
{
- int VarsU[512], VarsV[512];
- int nVarsU, nVarsV;
- int v, u, i, k;
- int Counter = 0;
- int satCalled = 0;
- int satProved = 0;
- double Density;
- int clk = clock();
-
- extern int symsSat;
- extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
-
-
- // count undecided pairs
- for ( v = 0; v < p->vInputs->nSize; v++ )
- for ( u = v+1; u < p->vInputs->nSize; u++ )
- {
- if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
- continue;
- Counter++;
- }
- // compute the density of 1's in the input space of the functions
- Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32;
-
- printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ",
- p->vInputs->nSize, Counter, Density );
+ Vec_Int_t * vSupport;
+ Extra_BitMat_t * pMatSym, * pMatNonSym;
+ int Index1, Index2, Index3, IndexU, IndexV;
+ int v, u, i, k, b, out;
-
- // go through the remaining variable pairs
- for ( v = 0; v < p->vInputs->nSize; v++ )
- for ( u = v+1; u < p->vInputs->nSize; u++ )
+ // iterate through outputs
+ for ( out = p->iOutput; out < p->nOutputs; out++ )
{
- if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
- continue;
- symsSat++;
- satCalled++;
-
- // collect the variables that are symmetric with each
- nVarsU = nVarsV = 0;
- for ( i = 0; i < p->vInputs->nSize; i++ )
+ pMatSym = Vec_PtrEntry( p->vMatrSymms, out );
+ pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );
+
+ // go through the remaining variable pairs
+ vSupport = Vec_VecEntry( p->vSupports, out );
+ Vec_IntForEachEntry( vSupport, v, Index1 )
+ Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
{
- if ( Extra_BitMatrixLookup1( pMatSym, u, i ) )
- VarsU[nVarsU++] = i;
- if ( Extra_BitMatrixLookup1( pMatSym, v, i ) )
- VarsV[nVarsV++] = i;
- }
+ if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+ continue;
+ p->nSatRuns++;
- if ( Fraig_SymmsSatProveOne( p, v, u ) )
- { // update the symmetric variable info
-//printf( "%d sym %d\n", v, u );
- for ( i = 0; i < nVarsU; i++ )
- for ( k = 0; k < nVarsV; k++ )
+ // collect the support variables that are symmetric with u and v
+ Vec_IntClear( p->vVarsU );
+ Vec_IntClear( p->vVarsV );
+ Vec_IntForEachEntry( vSupport, b, Index3 )
{
- Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1
- Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] ); // Theorem 1
- Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 2
+ if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
+ Vec_IntPush( p->vVarsU, b );
+ if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
+ Vec_IntPush( p->vVarsV, b );
}
- satProved++;
- }
- else
- { // update the assymmetric variable info
-//printf( "%d non-sym %d\n", v, u );
- for ( i = 0; i < nVarsU; i++ )
- for ( k = 0; k < nVarsV; k++ )
- {
- Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3
- Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] ); // Theorem 3
+
+ if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
+ { // update the symmetric variable info
+ p->nSatRunsUnsat++;
+ Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+ Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+ {
+ Extra_BitMatrixInsert1( pMatSym, i, k ); // Theorem 1
+ Extra_BitMatrixInsert2( pMatSym, i, k ); // Theorem 1
+ Extra_BitMatrixOrTwo( pMatNonSym, i, k ); // Theorem 2
+ }
+ }
+ else
+ { // update the assymmetric variable info
+ p->nSatRunsSat++;
+ Vec_IntForEachEntry( p->vVarsU, i, IndexU )
+ Vec_IntForEachEntry( p->vVarsV, k, IndexV )
+ {
+ Extra_BitMatrixInsert1( pMatNonSym, i, k ); // Theorem 3
+ Extra_BitMatrixInsert2( pMatNonSym, i, k ); // Theorem 3
+ }
+
+ // remember the out
+ p->iOutput = out;
+ p->iVar1Old = p->iVar1;
+ p->iVar2Old = p->iVar2;
+ p->iVar1 = v;
+ p->iVar2 = u;
+ return 1;
+
}
}
-//Extra_BitMatrixPrint( pMatSym );
-//Extra_BitMatrixPrint( pMatNonSym );
+ // make sure that the symmetry matrix contains only cliques
+ assert( Extra_BitMatrixIsClique( pMatSym ) );
}
-printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved );
-PRT( "Time", clock() - clk );
- // make sure that the symmetry matrix contains only cliques
- assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) );
+ // mark that we finished all outputs
+ p->iOutput = p->nOutputs;
+ return 0;
}
/**Function*************************************************************
@@ -136,65 +130,68 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 )
-{
- Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2;
- int RetValue;
- int nSatRuns = p->nSatCalls;
- int nSatProof = p->nSatProof;
-
- p->nBTLimit = 10; // set the backtrack limit
-
- pVar1 = p->vInputs->pArray[Var1];
- pVar2 = p->vInputs->pArray[Var2];
- pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) );
- pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 );
-
-//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof );
-
-// RetValue = (pCof01 == pCof10);
-// RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 );
- RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [A sanity check procedure.]
-
- Description [Makes sure that the symmetry information in the matrix
- is closed w.r.t. the relationship of transitivity (that is the symmetry
- graph is composed of cliques).]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
+int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
{
- int v, u, i;
- for ( v = 0; v < p->vInputs->nSize; v++ )
- for ( u = v+1; u < p->vInputs->nSize; u++ )
+ Fraig_Params_t Params;
+ Fraig_Man_t * pMan;
+ Abc_Ntk_t * pMiter;
+ int RetValue, i, clk;
+ int * pModel;
+
+ // get the miter for this problem
+ pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
+ // transform the miter into a fraig
+ Fraig_ParamsSetDefault( &Params );
+ Params.fInternal = 1;
+ Params.nPatsRand = 512;
+ Params.nPatsDyna = 512;
+
+clk = clock();
+ pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
+p->timeFraig += clock() - clk;
+clk = clock();
+ Fraig_ManProveMiter( pMan );
+p->timeSat += clock() - clk;
+
+ // analyze the result
+ RetValue = Fraig_ManCheckMiter( pMan );
+// assert( RetValue >= 0 );
+ // save the pattern
+ if ( RetValue == 0 )
{
- if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
- continue;
- // v and u are symmetric
- for ( i = 0; i < p->vInputs->nSize; i++ )
- {
- if ( i == v || i == u )
- continue;
- // i is neither v nor u
- // the symmetry status of i is the same w.r.t. to v and u
- if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
- return 0;
- }
+ // get the pattern
+ pModel = Fraig_ManReadModel( pMan );
+ assert( pModel != NULL );
+//printf( "Disproved by SAT: out = %d pair = (%d, %d)\n", Out, Var1, Var2 );
+ // transfer the model into the pattern
+ for ( i = 0; i < p->nSimWords; i++ )
+ pPattern[i] = 0;
+ for ( i = 0; i < p->nInputs; i++ )
+ if ( pModel[i] )
+ Sim_SetBit( pPattern, i );
+ // make sure these variables have the same value (1)
+ Sim_SetBit( pPattern, Var1 );
+ Sim_SetBit( pPattern, Var2 );
}
- return 1;
+ else if ( RetValue == -1 )
+ {
+ // this should never happen; if it happens, such is life
+ // we are conservative and assume that there is no symmetry
+//printf( "STRANGE THING: out = %d %s pair = (%d %s, %d %s)\n",
+// Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)),
+// Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)),
+// Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
+ memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
+ RetValue = 0;
+ }
+ // delete the fraig manager
+ Fraig_ManFree( pMan );
+ // delete the miter
+ Abc_NtkDelete( pMiter );
+ return RetValue;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index 53fc4ac2..94028c47 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -26,7 +26,7 @@
////////////////////////////////////////////////////////////////////////
static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
-static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output );
+static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -46,26 +46,36 @@ static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNo
void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym )
{
Abc_Obj_t * pNode;
- int i;
+ int i, nPairsTotal, nPairsSym, nPairsNonSym;
+ int clk;
+
// create the simulation matrix
Sim_SymmsCreateSquare( p, pPat );
// simulate each node in the DFS order
+clk = clock();
Vec_PtrForEachEntry( p->vNodes, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
continue;
Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords );
}
+p->timeSim += clock() - clk;
// collect info into the CO matrices
+clk = clock();
Abc_NtkForEachCo( p->pNtk, pNode, i )
{
pNode = Abc_ObjFanin0(pNode);
if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) )
continue;
- if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) )
+ nPairsTotal = Vec_IntEntry(p->vPairsTotal, i);
+ nPairsSym = Vec_IntEntry(p->vPairsSym, i);
+ nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ if ( nPairsTotal == nPairsSym + nPairsNonSym )
continue;
- Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i );
+ Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
}
+p->timeMatr += clock() - clk;
}
/**Function*************************************************************
@@ -114,40 +124,44 @@ void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat )
SeeAlso []
***********************************************************************/
-void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output )
+void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output )
{
- unsigned * pSuppInfo;
+ Extra_BitMat_t * pMat;
+ Vec_Int_t * vSupport;
+ unsigned * pSupport;
unsigned * pSimInfo;
- int i, w;
- // get the simuation info for the node
+ int i, w, Index;
+ // get the matrix, the support, and the simulation info
+ pMat = Vec_PtrEntry( vMatrsNonSym, Output );
+ vSupport = Vec_VecEntry( p->vSupports, Output );
+ pSupport = Vec_PtrEntry( p->vSuppFun, Output );
pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
- pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output );
// generate vectors A1 and A2
for ( w = 0; w < p->nSimWords; w++ )
{
- p->uPatCol[w] = pSuppInfo[w] & pPat[w] & pSimInfo[w];
- p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w];
+ p->uPatCol[w] = pSupport[w] & pPat[w] & pSimInfo[w];
+ p->uPatRow[w] = pSupport[w] & pPat[w] & ~pSimInfo[w];
}
// add two dimensions
- for ( i = 0; i < p->nInputs; i++ )
+ Vec_IntForEachEntry( vSupport, i, Index )
if ( Sim_HasBit( p->uPatCol, i ) )
Extra_BitMatrixOr( pMat, i, p->uPatRow );
// add two dimensions
- for ( i = 0; i < p->nInputs; i++ )
+ Vec_IntForEachEntry( vSupport, i, Index )
if ( Sim_HasBit( p->uPatRow, i ) )
Extra_BitMatrixOr( pMat, i, p->uPatCol );
// generate vectors B1 and B2
for ( w = 0; w < p->nSimWords; w++ )
{
- p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] & pSimInfo[w];
- p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w];
+ p->uPatCol[w] = pSupport[w] & ~pPat[w] & pSimInfo[w];
+ p->uPatRow[w] = pSupport[w] & ~pPat[w] & ~pSimInfo[w];
}
// add two dimensions
- for ( i = 0; i < p->nInputs; i++ )
+ Vec_IntForEachEntry( vSupport, i, Index )
if ( Sim_HasBit( p->uPatCol, i ) )
Extra_BitMatrixOr( pMat, i, p->uPatRow );
// add two dimensions
- for ( i = 0; i < p->nInputs; i++ )
+ Vec_IntForEachEntry( vSupport, i, Index )
if ( Sim_HasBit( p->uPatRow, i ) )
Extra_BitMatrixOr( pMat, i, p->uPatCol );
}
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
index c3059d84..ed7e93bf 100644
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@@ -37,7 +37,7 @@ static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, V
static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
static void Sim_SymmsPrint( Vec_Int_t * vSymms );
static void Sim_SymmsTrans( Vec_Int_t * vSymms );
-static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms );
+static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
@@ -55,7 +55,7 @@ static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
SeeAlso []
***********************************************************************/
-void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
+void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pTemp;
@@ -84,7 +84,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
pTemp = Abc_ObjFanin0(pTemp);
if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
continue;
- Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) );
+ Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
}
// clean the intermediate results
Sim_UtilInfoFree( pNtk->vSupps );
@@ -92,7 +92,8 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
Abc_NtkForEachCi( pNtk, pTemp, i )
Vec_IntFree( SIM_READ_SYMMS(pTemp) );
Vec_PtrForEachEntry( vNodes, pTemp, i )
- Vec_IntFree( SIM_READ_SYMMS(pTemp) );
+ if ( !Abc_NodeIsConst(pTemp) )
+ Vec_IntFree( SIM_READ_SYMMS(pTemp) );
Vec_PtrFree( vNodes );
free( pMap );
}
@@ -429,7 +430,7 @@ void Sim_SymmsTrans( Vec_Int_t * vSymms )
SeeAlso []
***********************************************************************/
-void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
+void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
{
int i, Ind1, Ind2, nInputs;
unsigned uSymm;
@@ -443,6 +444,10 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
uSymm = (unsigned)vSymms->pArray[i];
Ind1 = (uSymm & 0xffff);
Ind2 = (uSymm >> 16);
+ // skip variables that are not in the true support
+ assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
+ if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
+ continue;
Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
}
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 5a57ca2d..4b89c650 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -436,18 +436,80 @@ int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCou
SeeAlso []
***********************************************************************/
-int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters )
+int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
{
- Extra_BitMat_t * vMat;
- int Counter, nPairs, i;
- Counter = 0;
- Vec_PtrForEachEntry( vMatrs, vMat, i )
+ int i, k, Index1, Index2;
+ int Counter = 0;
+// int Counter2;
+ Vec_IntForEachEntry( vSupport, i, Index1 )
+ Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
+ Counter += Extra_BitMatrixLookup1( pMat, i, k );
+// Counter2 = Extra_BitMatrixCountOnesUpper(pMat);
+// assert( Counter == Counter2 );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of entries in the array of matrices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sim_UtilCountPairsAll( Sym_Man_t * p )
+{
+ int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
+clk = clock();
+ p->nPairsSymm = 0;
+ p->nPairsNonSymm = 0;
+ for ( i = 0; i < p->nOutputs; i++ )
{
- nPairs = Extra_BitMatrixCountOnesUpper( vMat );
- Vec_IntWriteEntry( vCounters, i, nPairs );
- Counter += nPairs;
+ nPairsTotal = Vec_IntEntry(p->vPairsTotal, i);
+ nPairsSym = Vec_IntEntry(p->vPairsSym, i);
+ nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ if ( nPairsTotal == nPairsSym + nPairsNonSym )
+ {
+ p->nPairsSymm += nPairsSym;
+ p->nPairsNonSymm += nPairsNonSym;
+ continue;
+ }
+ nPairsSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
+ nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) );
+ assert( nPairsTotal >= nPairsSym + nPairsNonSym );
+ Vec_IntWriteEntry( p->vPairsSym, i, nPairsSym );
+ Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
+ p->nPairsSymm += nPairsSym;
+ p->nPairsNonSymm += nPairsNonSym;
+// printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
}
- return Counter;
+//printf( "\n" );
+ p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
+p->timeCount += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nOutputs; i++ )
+ if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) )
+ return 0;
+ return 1;
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 02:57:09 +0000