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.

This commit is contained in:
Alan Mishchenko 2013-05-06 00:44:21 -07:00
parent 05f7cd9ed2
commit f321b27bb7
5 changed files with 201 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/giaUtil.c
View File

@ -370,6 +370,7 @@ void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues )
{
Gia_Obj_t * pObj;
int i;
assert( Gia_ManCiNum(p) == Vec_IntSize(vCiValues) );
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjIsCi(pObj) )
pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) );

61
src/proof/ssc/sscClass.c
View File

@ -107,6 +107,12 @@ static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
}
return 1;
}
static inline int Ssc_GiaSimAreEqualBit( Gia_Man_t * p, int iObj0, int iObj1 )
{
Gia_Obj_t * pObj0 = Gia_ManObj( p, iObj0 );
Gia_Obj_t * pObj1 = Gia_ManObj( p, iObj1 );
return (pObj0->fPhase ^ pObj0->fMark0) == (pObj1->fPhase ^ pObj1->fMark0);
}
/**Function*************************************************************
@ -141,10 +147,58 @@ void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
}
Gia_ObjSetNext( p, EntPrev, 0 );
}
/**Function*************************************************************
Synopsis [Refines one equivalence class using individual bit-pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i )
{
Gia_Obj_t * pObj;
int Ent;
assert( Gia_ObjIsHead( p, i ) );
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
pObj = Gia_ManObj(p, i);
Gia_ClassForEachObj1( p, i, Ent )
{
if ( Ssc_GiaSimAreEqualBit( p, i, Ent ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
Ssc_GiaSimClassCreate( p, p->vClassOld );
Ssc_GiaSimClassCreate( p, p->vClassNew );
return 1;
}
/**Function*************************************************************
Synopsis [Refines one class using simulation patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
{
Gia_Obj_t * pObj;
int Ent;
assert( Gia_ObjIsHead( p, i ) );
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
@ -226,17 +280,18 @@ int Ssc_GiaClassesRefine( Gia_Man_t * p )
{
Vec_Int_t * vRefinedC;
Gia_Obj_t * pObj;
int i;
int i, Counter = 0;
if ( p->pReprs != NULL );
vRefinedC = Vec_IntAlloc( 100 );
Gia_ManForEachCand( p, pObj, i )
if ( Gia_ObjIsTail(p, i) )
Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
Counter += Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
Vec_IntPush( vRefinedC, i );
Ssc_GiaSimProcessRefined( p, vRefinedC );
Counter += Vec_IntSize( vRefinedC );
Vec_IntFree( vRefinedC );
return 0;
return Counter;
}

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

@ -119,6 +119,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
p->vFanins = Vec_IntAlloc( 100 );
p->vFront = Vec_IntAlloc( 100 );
Ssc_GiaClassesInit( pAig );
// now it is ready for refinement using simulation
return p;
}
void Ssc_ManPrintStats( Ssc_Man_t * p )
@ -142,6 +143,65 @@ void Ssc_ManPrintStats( Ssc_Man_t * p )
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
/**Function*************************************************************
Synopsis [Refine one class by resimulating one pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj )
{
Gia_Obj_t * pObj;
int Res0, Res1;
if ( Ssc_ObjSatVar(p, iFraigObj) )
return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) );
pObj = Gia_ManObj( p->pFraig, iFraigObj );
assert( Gia_ObjIsAnd(pObj) );
Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) );
Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) );
pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
return pObj->fMark0;
}
int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj )
{
int Res0, Res1;
if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
return pObj->fMark0;
Gia_ObjSetTravIdCurrent(p->pAig, pObj);
if ( ~pObj->Value ) // mapping into FRAIG exists - simulate FRAIG
{
Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) );
pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value);
}
else // mapping into FRAIG does not exist - simulate AIG
{
Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) );
Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) );
pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
}
return pObj->fMark0;
}
int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
{
int Ent, RetValue;
assert( iRepr == Gia_ObjRepr(p->pAig, iObj) );
assert( Gia_ObjIsHead( p->pAig, iRepr ) );
// set bit-values at the nodes according to the counter-example
Gia_ManIncrementTravId( p->pAig );
Gia_ClassForEachObj( p->pAig, iRepr, Ent )
Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) );
// refine one class using these bit-values
RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr );
// check that the candidate equivalence is indeed refined
assert( iRepr != Gia_ObjRepr(p->pAig, iObj) );
return RetValue;
}
/**Function*************************************************************
Synopsis []
@ -159,7 +219,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
Gia_Man_t * pResult;
Gia_Obj_t * pObj, * pRepr;
clock_t clk, clkTotal = clock();
int i, fCompl, status;
int i, fCompl, nRefined, status;
clk = clock();
assert( Gia_ManRegNum(pCare) == 0 );
assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
@ -172,18 +232,23 @@ clk = clock();
if ( p == NULL )
return Gia_ManDup( pAig );
if ( p->pPars->fVerbose )
printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 10), 640 );
printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );
// perform simulation
if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
while ( 1 )
{
for ( i = 0; i < 16; i++ )
{
Ssc_GiaRandomPiPattern( pAig, 10, NULL );
Ssc_GiaSimRound( pAig );
if ( pPars->fVerbose )
Ssc_GiaClassesRefine( pAig );
// simulate care set
Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL );
Ssc_GiaSimRound( p->pFraig );
// transfer care patterns to user's AIG
if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) )
break;
// simulate the main AIG
Ssc_GiaSimRound( pAig );
nRefined = Ssc_GiaClassesRefine( pAig );
if ( pPars->fVerbose )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
break;
}
p->timeSimInit += clock() - clk;
@ -242,6 +307,8 @@ clk = clock();
Vec_IntPush( p->vDisPairs, i );
// printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
// Vec_IntPrint( p->vPattern );
if ( Gia_ObjRepr(p->pAig, i) > 0 )
Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i );
}
else if ( status == l_Undef )
p->nSatCallsUndec++;

2
src/proof/ssc/sscInt.h
View File

@ -102,6 +102,7 @@ static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj
extern void Ssc_GiaClassesInit( Gia_Man_t * p );
extern int Ssc_GiaClassesRefine( Gia_Man_t * p );
extern void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
extern int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i );
/*=== sscCnf.c ===================================================*/
extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
/*=== sscCore.c ==================================================*/
@ -113,6 +114,7 @@ extern int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj
/*=== sscSim.c ===================================================*/
extern void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
extern int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot );
extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
extern void Ssc_GiaSimRound( Gia_Man_t * p );
extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p );

72
src/proof/ssc/sscSim.c
View File

@ -175,6 +175,56 @@ void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
// Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
}
}
void Ssc_GiaPrintPiPatterns( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
word * pSimAig;
int i, nWords = Gia_ObjSimWords( p );
Gia_ManForEachCi( p, pObj, i )
{
pSimAig = Gia_ObjSimObj( p, pObj );
// Extra_PrintBinary( stdout, pSimAig, 64 * nWords );
}
}
/**Function*************************************************************
Synopsis [Transfer the simulation pattern from pCare to pAig.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot )
{
extern word * Ssc_GiaGetCareMask( Gia_Man_t * p );
Gia_Obj_t * pObj;
int i, w, nWords = Gia_ObjSimWords( pCare );
word * pCareMask = Ssc_GiaGetCareMask( pCare );
int Count = Ssc_SimCountBits( pCareMask, nWords );
word * pSimPiCare, * pSimPiAig;
if ( Count == 0 )
{
ABC_FREE( pCareMask );
return 0;
}
Ssc_GiaResetPiPattern( pAig, nWords );
Gia_ManForEachCi( pCare, pObj, i )
{
pSimPiAig = Gia_ObjSimPi( pAig, i );
pSimPiCare = Gia_ObjSimObj( pCare, pObj );
for ( w = 0; w < nWords; w++ )
if ( Vec_IntEntry(vPivot, i) )
pSimPiAig[w] = pSimPiCare[w] | ~pCareMask[w];
else
pSimPiAig[w] = pSimPiCare[w] & pCareMask[w];
}
ABC_FREE( pCareMask );
return Count;
}
/**Function*************************************************************
@ -246,14 +296,21 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
word * Ssc_GiaGetCareMask( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, nWords = Gia_ObjSimWords( p );
word * pRes = ABC_FALLOC( word, nWords );
Gia_ManForEachPo( p, pObj, i )
Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
return pRes;
}
Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
{
Vec_Int_t * vInit;
Gia_Obj_t * pObj;
int i, iBit, nWords = Gia_ObjSimWords( p );
word * pRes = ABC_FALLOC( word, nWords );
Gia_ManForEachPo( p, pObj, i )
Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
word * pRes = Ssc_GiaGetCareMask( p );
iBit = Ssc_SimFindBit( pRes, nWords );
ABC_FREE( pRes );
if ( iBit == -1 )
@ -285,12 +342,9 @@ Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
***********************************************************************/
int Ssc_GiaCountCaresSim( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Count, nWords = Gia_ObjSimWords( p );
word * pRes = ABC_FALLOC( word, nWords );
Gia_ManForEachPo( p, pObj, i )
Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
Count = Ssc_SimCountBits( pRes, nWords );
word * pRes = Ssc_GiaGetCareMask( p );
int nWords = Gia_ObjSimWords( p );
int Count = Ssc_SimCountBits( pRes, nWords );
ABC_FREE( pRes );
return Count;
}