/**CFile****************************************************************
FileName [dchSimSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Choice computation for tech-mapping.]
Synopsis [Performs resimulation using counter-examples.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dchInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collects internal nodes in the reverse DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanout, * pRepr;
int iFanout = -1, i;
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
// traverse the fanouts
Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
Dch_ManCollectTfoCands_rec( p, pFanout );
// check if the given node has a representative
pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
if ( pRepr == NULL )
return;
// pRepr is the constant 1 node
if ( pRepr == Aig_ManConst1(p->pAigTotal) )
{
Vec_PtrPush( p->vSimRoots, pObj );
return;
}
// pRepr is the representative of an equivalence class
if ( pRepr->fMarkA )
return;
pRepr->fMarkA = 1;
Vec_PtrPush( p->vSimClasses, pRepr );
}
/**Function*************************************************************
Synopsis [Collect equivalence classes and const1 cands in the TFO.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
Aig_Obj_t * pObj;
int i;
Vec_PtrClear( p->vSimRoots );
Vec_PtrClear( p->vSimClasses );
Aig_ManIncrementTravId( p->pAigTotal );
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManCollectTfoCands_rec( p, pObj1 );
Dch_ManCollectTfoCands_rec( p, pObj2 );
Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
pObj->fMarkA = 0;
}
/**Function*************************************************************
Synopsis [Resimulates the cone of influence of the solved nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
if ( Aig_ObjIsPi(pObj) )
{
Aig_Obj_t * pObjFraig;
int nVarNum;
pObjFraig = Dch_ObjFraig( pObj );
assert( !Aig_IsComplement(pObjFraig) );
nVarNum = Dch_ObjSatNum( p, pObjFraig );
// get the value from the SAT solver
// (account for the fact that some vars may be minimized away)
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
return;
}
Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
// count the cone size
if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
p->nConeThis++;
}
/**Function*************************************************************
Synopsis [Resimulates the cone of influence of the other nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
{
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
if ( Aig_ObjIsPi(pObj) )
{
// set random value
pObj->fMarkB = Aig_ManRandom(0) & 1;
return;
}
Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pRoot, ** ppClass;
int i, k, nSize, RetValue1, RetValue2, clk = clock();
// get the equivalence classes
Dch_ManCollectTfoCands( p, pObj, pRepr );
// resimulate the cone of influence of the solved nodes
p->nConeThis = 0;
Aig_ManIncrementTravId( p->pAigTotal );
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );
// refine these nodes
RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
// resimulate the cone of influence of the cand classes
RetValue2 = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
{
ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
for ( k = 0; k < nSize; k++ )
Dch_ManResimulateOther_rec( p, ppClass[k] );
// refine this class
RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
}
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
assert( RetValue1 );
else
assert( RetValue2 );
p->timeSimSat += clock() - clk;
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pRoot;
int i, RetValue, clk = clock();
// get the equivalence class
if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
else
Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
// resimulate the cone of influence of the solved nodes
p->nConeThis = 0;
Aig_ManIncrementTravId( p->pAigTotal );
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );
// refine this class
if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
else
RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
assert( RetValue );
p->timeSimSat += clock() - clk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END