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

Experiments with the SAT sweeper.

This commit is contained in:
Alan Mishchenko 2023-09-04 19:58:31 +07:00
parent a13dae7a4a
commit 301469432d
2 changed files with 76 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/aig/gia/giaDup.c
View File

@ -1604,6 +1604,47 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates while adding self-loops to the registers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs )
{
Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit0, iLit1;
pNew = Gia_ManStart( Gia_ManObjNum(p) + 3 * Vec_IntSize(vPairs) );
pNew->pName = Abc_UtilStrsav( "miter" );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntForEachEntryDouble( vPairs, iLit0, iLit1, i )
{
int Lit0 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit0))->Value, Abc_LitIsCompl(iLit0) );
int Lit1 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit1))->Value, Abc_LitIsCompl(iLit1) );
Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Lit0, Lit1) );
}
Vec_IntForEachEntry( vTemp, iLit0, i )
Gia_ManAppendCo( pNew, iLit0 );
Vec_IntFree( vTemp );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]

41
src/proof/cec/cecSatG2.c
View File

@ -101,6 +101,7 @@ struct Cec4_Man_t_
Vec_Int_t * vDisprPairs;
Vec_Bit_t * vFails;
Vec_Bit_t * vCoDrivers;
Vec_Int_t * vPairs;
int iPosRead; // candidate reading position
int iPosWrite; // candidate writing position
int iLastConst; // last const node proved
@ -250,6 +251,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->vPat = Vec_IntAlloc( 100 );
p->vDisprPairs = Vec_IntAlloc( 100 );
p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) );
p->vPairs = pPars->fUseCones ? Vec_IntAlloc( 100 ) : NULL;
//pAig->pData = p->pSat; // point AIG manager to the solver
//Vec_IntFreeP( &p->pAig->vPats );
//p->pAig->vPats = Vec_IntAlloc( 1000 );
@ -304,6 +306,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
Vec_IntFreeP( &p->vPat );
Vec_IntFreeP( &p->vDisprPairs );
Vec_BitFreeP( &p->vFails );
Vec_IntFreeP( &p->vPairs );
Vec_BitFreeP( &p->vCoDrivers );
Vec_IntFreeP( &p->vRefClasses );
Vec_IntFreeP( &p->vRefNodes );
@ -1686,12 +1689,26 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
{
p->nSatUndec++;
assert( status == GLUCOSE_UNDEC );
Gia_ObjSetFailed( p->pAig, iObj );
Vec_BitWriteEntry( p->vFails, iObj, 1 );
//if ( iRepr )
//Vec_BitWriteEntry( p->vFails, iRepr, 1 );
p->timeSatUndec += Abc_Clock() - clk;
RetValue = 2;
if ( p->vPairs ) // speculate
{
Vec_IntPushTwo( p->vPairs, Abc_Var2Lit(iRepr, 0), Abc_Var2Lit(iObj, fCompl) );
p->timeSatUndec += Abc_Clock() - clk;
// mark as proved
pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
Gia_ObjSetProved( p->pAig, iObj );
if ( iRepr == 0 )
p->iLastConst = iObj;
RetValue = 1;
}
else
{
Gia_ObjSetFailed( p->pAig, iObj );
Vec_BitWriteEntry( p->vFails, iObj, 1 );
//if ( iRepr )
//Vec_BitWriteEntry( p->vFails, iRepr, 1 );
p->timeSatUndec += Abc_Clock() - clk;
RetValue = 2;
}
}
return RetValue;
}
@ -1896,6 +1913,18 @@ finalize:
pMan->nSatSat, pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],
pMan->nSatUndec,
pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
if ( pMan->vPairs && Vec_IntSize(pMan->vPairs) )
{
extern char * Extra_FileNameGeneric( char * FileName );
char pFileName[1000], * pBase = Extra_FileNameGeneric(p->pName);
extern Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs );
Gia_Man_t * pM = Gia_ManDupMiterCones( p, pMan->vPairs );
sprintf( pFileName, "%s_miter.aig", pBase );
Gia_AigerWrite( pM, pFileName, 0, 0, 0 );
Gia_ManStop( pM );
ABC_FREE( pBase );
printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs) : -1 );
}
Cec4_ManDestroy( pMan );
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );