Skip to content

A
abc
Commit 83519c32 by Alan Mishchenko
Options

Experiments with SAT sweeping.

parent c0bb4bb0
Showing with 161 additions and 30 deletions
src/aig/gia/giaEquiv.c
......@@ -269,6 +269,7 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
pTails[i] = i;
for ( i = 0; i < Gia_ManObjNum(p); i++ )
{
//if ( p->pReprs[i].iRepr == GIA_VOID )
if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
continue;
pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
......@@ -2589,6 +2590,123 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
}
/**Function*************************************************************
Synopsis [Changing node order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManChangeOrder_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
if ( Gia_ObjIsCi(pObj) )
return pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
if ( Gia_ObjIsCo(pObj) )
return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin1(pObj) );
return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_Man_t * Gia_ManChangeOrder( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, k;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachClass( p, i )
Gia_ClassForEachObj( p, i, k )
Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
Gia_ManForEachConst( p, k )
Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) );
return pNew;
}
void Gia_ManTransferEquivs( Gia_Man_t * p, Gia_Man_t * pNew )
{
Vec_Int_t * vClass;
int i, k, iNode, iRepr;
assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
assert( p->pReprs != NULL );
assert( p->pNexts != NULL );
assert( pNew->pReprs == NULL );
assert( pNew->pNexts == NULL );
// start representatives
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
// iterate over constant candidates
Gia_ManForEachConst( p, i )
Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
// iterate over class candidates
vClass = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, i )
{
Vec_IntClear( vClass );
Gia_ClassForEachObj( p, i, k )
Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
assert( Vec_IntSize( vClass ) > 1 );
Vec_IntSort( vClass, 0 );
iRepr = Vec_IntEntry( vClass, 0 );
Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
Gia_ObjSetRepr( pNew, iNode, iRepr );
}
Vec_IntFree( vClass );
pNew->pNexts = Gia_ManDeriveNexts( pNew );
}
void Gia_ManTransferTest( Gia_Man_t * p )
{
Gia_Obj_t * pObj; int i;
Gia_Rpr_t * pReprs = p->pReprs; // representatives (for CIs and ANDs)
int * pNexts = p->pNexts; // next nodes in the equivalence classes
Gia_Man_t * pNew = Gia_ManChangeOrder(p);
//Gia_ManEquivPrintClasses( p, 1, 0 );
assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
Gia_ManTransferEquivs( p, pNew );
p->pReprs = NULL;
p->pNexts = NULL;
// make new point to old
Gia_ManForEachObj( p, pObj, i )
{
assert( !Abc_LitIsCompl(pObj->Value) );
Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
}
Gia_ManTransferEquivs( pNew, p );
//Gia_ManEquivPrintClasses( p, 1, 0 );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
pReprs[i].fProved = 0;
//printf( "%5d : %5d %5d %5d %5d\n", i, *(int*)&p->pReprs[i], *(int*)&pReprs[i], (int)p->pNexts[i], (int)pNexts[i] );
if ( memcmp(p->pReprs, pReprs, sizeof(int)*Gia_ManObjNum(p)) )
printf( "Verification of reprs failed.\n" );
else
printf( "Verification of reprs succeeded.\n" );
if ( memcmp(p->pNexts, pNexts, sizeof(int)*Gia_ManObjNum(p)) )
printf( "Verification of nexts failed.\n" );
else
printf( "Verification of nexts succeeded.\n" );
ABC_FREE( pNew->pReprs );
ABC_FREE( pNew->pNexts );
ABC_FREE( pReprs );
ABC_FREE( pNexts );
Gia_ManStop( pNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/proof/cec/cecSatG2.c
......@@ -79,6 +79,7 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
......@@ -92,24 +93,11 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
***********************************************************************/
Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
{
Cec4_Man_t * p;
Gia_Obj_t * pObj; int i;
//assert( Gia_ManRegNum(pAig) == 0 );
p = ABC_CALLOC( Cec4_Man_t, 1 );
Cec4_Man_t * p = ABC_CALLOC( Cec4_Man_t, 1 );
memset( p, 0, sizeof(Cec4_Man_t) );
p->timeStart = Abc_Clock();
p->pPars = pPars;
p->pAig = pAig;
pAig->pData = p->pSat; // point AIG manager to the solver
// create new manager
p->pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
Gia_ManFillValue( pAig );
Gia_ManConst0(pAig)->Value = 0;
Gia_ManForEachCi( pAig, pObj, i )
pObj->Value = Gia_ManAppendCi( p->pNew );
Gia_ManHashAlloc( p->pNew );
Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
// SAT solving
p->timeStart = Abc_Clock();
p->pPars = pPars;
p->pAig = pAig;
p->pSat = bmcg_sat_solver_start();
p->vFrontier = Vec_PtrAlloc( 1000 );
p->vFanins = Vec_PtrAlloc( 100 );
......@@ -119,6 +107,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->vCands = Vec_IntAlloc( 100 );
p->vVisit = Vec_IntAlloc( 100 );
p->vPat = Vec_IntAlloc( 100 );
//pAig->pData = p->pSat; // point AIG manager to the solver
return p;
}
void Cec4_ManDestroy( Cec4_Man_t * p )
......@@ -158,6 +147,21 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
Vec_IntFreeP( &p->vPat );
ABC_FREE( p );
}
Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
{
Gia_Obj_t * pObj; int i;
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
pNew->pName = Abc_UtilStrsav( pAig->pName );
pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
Gia_ManFillValue( pAig );
Gia_ManConst0(pAig)->Value = 0;
Gia_ManForEachCi( pAig, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManHashAlloc( pNew );
Vec_IntFill( &pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(pAig) );
return pNew;
}
/**Function*************************************************************
......@@ -933,16 +937,24 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p )
{
abctime clk = Abc_Clock();
int i, k, iLit, nPats = 64 * p->pAig->nSimWords;
Gia_Obj_t * pObj;
// collect candidate nodes
Vec_IntClear( p->vCands );
Gia_ManForEachObj( p->pAig, pObj, i )
if ( p->pPars->nGenIters )
{
pObj->fMark0 = pObj->fMark1 = 0;
if ( !Gia_ObjIsHead(p->pAig, i) )
continue;
Gia_ClassForEachObj1( p->pAig, i, k )
Vec_IntPush( p->vCands, k );
if ( Vec_IntSize(p->vCands) == 0 )
{
for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
if ( Gia_ObjRepr(p->pAig, i) != GIA_VOID )
Vec_IntPush( p->vCands, i );
}
else
{
int iObj, k = 0;
Vec_IntForEachEntry( p->vCands, iObj, i )
if ( Gia_ObjRepr(p->pAig, iObj) != GIA_VOID )
Vec_IntWriteEntry( p->vCands, k++, iObj );
Vec_IntShrink( p->vCands, k );
assert( Vec_IntSize(p->vCands) > 0 );
}
}
// generate the given number of patterns
for ( i = 0, p->pAig->iPatsPi = 1; i < p->pPars->nGenIters * nPats && p->pAig->iPatsPi < nPats; p->pAig->iPatsPi++, i++ )
......@@ -969,6 +981,7 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p )
p->timeGenPats += Abc_Clock() - clk;
}
/**Function*************************************************************
Synopsis [Internal simulation APIs.]
......@@ -1106,7 +1119,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
p->timeSatSat += Abc_Clock() - clk;
RetValue = 0;
// this is not needed, but we keep it here anyway, because it takes very little time
Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
//Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
// resimulated once in a while
if ( p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1 )
{
......@@ -1186,7 +1199,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
// check if any output trivially fails under all-0 pattern
Gia_ManRandomW( 1 );
Gia_ManSetPhase( p );
Gia_ManStaticFanoutStart( p );
//Gia_ManStaticFanoutStart( p );
if ( pPars->fCheckMiter )
{
Gia_ManForEachCo( p, pObj, i )
......@@ -1219,7 +1232,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
Cec4_ManPrintStats( p, pPars, pMan );
}
p->iPatsPi = 0;
pMan->pNew = Cec4_ManStartNew( p );
Gia_ManForEachAnd( p, pObj, i )
{
//Gia_Obj_t * pObjNew;
......@@ -1263,8 +1278,6 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
*ppNew = Gia_ManCleanup( pMan->pNew );
(*ppNew)->pName = Abc_UtilStrsav( p->pName );
(*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec );
}
finalize:
if ( pPars->fVerbose )
......@@ -1275,7 +1288,7 @@ finalize:
pMan->nSatUndec,
pMan->nSimulates, pMan->nRecycles );
Cec4_ManDestroy( pMan );
Gia_ManStaticFanoutStop( p );
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );
return p->pCexSeq ? 0 : 1;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment