luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

SAT sweeping under constraints (bug fix).

This commit is contained in:
Alan Mishchenko 2013-05-07 18:11:29 -07:00
parent 51db560206
commit a735d95a5b
5 changed files with 16 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -891,7 +891,7 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );

7
src/aig/gia/giaEquiv.c
View File

@ -414,7 +414,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@ -445,7 +445,8 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
return NULL;
}
*/
Gia_ManSetPhase( p );
if ( !fSkipPhase )
Gia_ManSetPhase( p );
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
@ -637,7 +638,7 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
{
Gia_Man_t * pNew, * pFinal;
pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
if ( pNew == NULL )
return NULL;
if ( fMiterPairs )

2
src/aig/gia/giaSweep.c
View File

@ -288,7 +288,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
if ( p->pManTime == NULL )
{
Gia_ManFraigSweepPerform( p, pPars );
pNew = Gia_ManEquivReduce( p, 1, 0, 0 );
pNew = Gia_ManEquivReduce( p, 1, 0, 0, 0 );
if ( pNew == NULL )
return Gia_ManDup(p);
return pNew;

14
src/base/abci/abc.c
View File

@ -27365,7 +27365,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fSynthesis )
{
pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, fVerbose );
pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, fDualOut, 0, fVerbose );
if ( pTemp )
{
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
@ -27612,7 +27612,7 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fUseAll )
{
pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, fVerbose );
pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, 0, fVerbose );
pTemp = Gia_ManSeqStructSweep( pTemp2 = pTemp, 1, 1, 0 );
Gia_ManStop( pTemp2 );
}
@ -31601,7 +31601,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// Gia_Man_t * pTemp = NULL;
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
int fSwitch = 0;
// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
@ -31614,9 +31614,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Unr_ManTest( Gia_Man_t * pGia );
// extern void Mig_ManTest( Gia_Man_t * pGia );
// extern int Gia_ManVerify( Gia_Man_t * pGia );
// extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
// extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
// extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@ -31668,10 +31668,10 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Unr_ManTest( pAbc->pGia );
// Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia );
// pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
// pTemp = Gia_ManOptimizeRing( pAbc->pGia );
// Abc_FrameUpdateGia( pAbc, pTemp );
// Gia_ManCollectSeqTest( pAbc->pGia );
// pTemp = Gia_ManOptimizeRing( pAbc->pGia );
pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &test [-svh]\n" );

4
src/proof/ssc/sscCore.c
View File

@ -298,6 +298,7 @@ clk = clock();
{
p->nSatCallsUnsat++;
pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
Gia_ObjSetProved( pAig, i );
}
else if ( status == l_True )
{
@ -329,9 +330,10 @@ clk = clock();
p->timeSimSat += clock() - clk;
}
// Gia_ManEquivPrintClasses( pAig, 1, 0 );
// Gia_ManPrint( pAig );
// generate the resulting AIG
pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
if ( pResult == NULL )
{
printf( "There is no equivalences.\n" );