/**CFile****************************************************************
FileName [gia.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// combinational simulation manager
typedef struct Hcd_Man_t_ Hcd_Man_t;
struct Hcd_Man_t_
{
// parameters
Gia_Man_t * pGia; // the AIG to be used for simulation
int nBTLimit; // internal backtrack limit
int fVerbose; // internal verbose flag
// internal variables
unsigned * pSimInfo; // simulation info for each object
Vec_Ptr_t * vSimInfo; // pointers to the CI simulation info
Vec_Ptr_t * vSimPres; // pointers to the presense of simulation info
// temporaries
Vec_Int_t * vClassOld; // old class numbers
Vec_Int_t * vClassNew; // new class numbers
Vec_Int_t * vClassTemp; // temporary storage
Vec_Int_t * vRefinedC; // refined const reprs
};
static inline unsigned Hcd_ObjSim( Hcd_Man_t * p, int Id ) { return p->pSimInfo[Id]; }
static inline unsigned * Hcd_ObjSimP( Hcd_Man_t * p, int Id ) { return p->pSimInfo + Id; }
static inline unsigned Hcd_ObjSetSim( Hcd_Man_t * p, int Id, unsigned n ) { return p->pSimInfo[Id] = n; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hcd_Man_t * Gia_ManEquivStart( Gia_Man_t * pGia, int nBTLimit, int fVerbose )
{
Hcd_Man_t * p;
Gia_Obj_t * pObj;
int i;
p = ABC_CALLOC( Hcd_Man_t, 1 );
p->pGia = pGia;
p->nBTLimit = nBTLimit;
p->fVerbose = fVerbose;
p->pSimInfo = ABC_ALLOC( unsigned, Gia_ManObjNum(pGia) );
p->vClassOld = Vec_IntAlloc( 100 );
p->vClassNew = Vec_IntAlloc( 100 );
p->vClassTemp = Vec_IntAlloc( 100 );
p->vRefinedC = Vec_IntAlloc( 100 );
// collect simulation info
p->vSimInfo = Vec_PtrAlloc( 1000 );
Gia_ManForEachCi( pGia, pObj, i )
Vec_PtrPush( p->vSimInfo, Hcd_ObjSimP(p, Gia_ObjId(pGia,pObj)) );
p->vSimPres = Vec_PtrAllocSimInfo( Gia_ManCiNum(pGia), 1 );
return p;
}
/**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManEquivStop( Hcd_Man_t * p )
{
Vec_PtrFree( p->vSimInfo );
Vec_PtrFree( p->vSimPres );
Vec_IntFree( p->vClassOld );
Vec_IntFree( p->vClassNew );
Vec_IntFree( p->vClassTemp );
Vec_IntFree( p->vRefinedC );
ABC_FREE( p->pSimInfo );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Compared two simulation infos.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Hcd_ManCompareEqual( unsigned s0, unsigned s1 )
{
if ( (s0 & 1) == (s1 & 1) )
return s0 == s1;
else
return s0 ==~s1;
}
/**Function*************************************************************
Synopsis [Compares one simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Hcd_ManCompareConst( unsigned s )
{
if ( s & 1 )
return s ==~0;
else
return s == 0;
}
/**Function*************************************************************
Synopsis [Creates one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManClassCreate( Gia_Man_t * pGia, Vec_Int_t * vClass )
{
int Repr = -1, EntPrev = -1, Ent, i;
assert( Vec_IntSize(vClass) > 0 );
Vec_IntForEachEntry( vClass, Ent, i )
{
if ( i == 0 )
{
Repr = Ent;
Gia_ObjSetRepr( pGia, Ent, -1 );
EntPrev = Ent;
}
else
{
Gia_ObjSetRepr( pGia, Ent, Repr );
Gia_ObjSetNext( pGia, EntPrev, Ent );
EntPrev = Ent;
}
}
Gia_ObjSetNext( pGia, EntPrev, 0 );
}
/**Function*************************************************************
Synopsis [Refines one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ManClassClassRemoveOne( Hcd_Man_t * p, int i )
{
int iRepr, Ent;
if ( Gia_ObjIsConst(p->pGia, i) )
{
Gia_ObjSetRepr( p->pGia, i, GIA_VOID );
return 1;
}
if ( !Gia_ObjIsClass(p->pGia, i) )
return 0;
assert( Gia_ObjIsClass(p->pGia, i) );
iRepr = Gia_ObjRepr( p->pGia, i );
if ( iRepr == GIA_VOID )
iRepr = i;
// collect nodes
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Gia_ClassForEachObj( p->pGia, iRepr, Ent )
{
if ( Ent == i )
Vec_IntPush( p->vClassNew, Ent );
else
Vec_IntPush( p->vClassOld, Ent );
}
assert( Vec_IntSize( p->vClassNew ) == 1 );
Hcd_ManClassCreate( p->pGia, p->vClassOld );
Hcd_ManClassCreate( p->pGia, p->vClassNew );
assert( !Gia_ObjIsClass(p->pGia, i) );
return 1;
}
/**Function*************************************************************
Synopsis [Refines one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ManClassRefineOne( Hcd_Man_t * p, int i )
{
unsigned Sim0, Sim1;
int Ent;
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
Sim0 = Hcd_ObjSim(p, i);
Gia_ClassForEachObj1( p->pGia, i, Ent )
{
Sim1 = Hcd_ObjSim(p, Ent);
if ( Hcd_ManCompareEqual( Sim0, Sim1 ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
Hcd_ManClassCreate( p->pGia, p->vClassOld );
Hcd_ManClassCreate( p->pGia, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
return 1 + Hcd_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
/**Function*************************************************************
Synopsis [Computes hash key of the simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
{
static int s_Primes[16] = {
1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
unsigned uHash = 0;
int i;
if ( pSim[0] & 1 )
for ( i = 0; i < nWords; i++ )
uHash ^= ~pSim[i] * s_Primes[i & 0xf];
else
for ( i = 0; i < nWords; i++ )
uHash ^= pSim[i] * s_Primes[i & 0xf];
return (int)(uHash % nTableSize);
}
/**Function*************************************************************
Synopsis [Rehashes the refined classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined )
{
int * pTable, nTableSize, Key, i, k;
nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
assert( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) );
Key = Hcd_ManHashKey( Hcd_ObjSimP(p, i), 1, nTableSize );
if ( pTable[Key] == 0 )
Gia_ObjSetRepr( p->pGia, i, GIA_VOID );
else
{
Gia_ObjSetNext( p->pGia, pTable[Key], i );
Gia_ObjSetRepr( p->pGia, i, Gia_ObjRepr(p->pGia, pTable[Key]) );
if ( Gia_ObjRepr(p->pGia, i) == GIA_VOID )
Gia_ObjSetRepr( p->pGia, i, pTable[Key] );
}
pTable[Key] = i;
}
ABC_FREE( pTable );
// Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
// refine classes in the table
Vec_IntForEachEntry( vRefined, i, k )
{
if ( Gia_ObjIsHead( p->pGia, i ) )
Hcd_ManClassRefineOne( p, i );
}
Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
}
/**Function*************************************************************
Synopsis [Refines equivalence classes after simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManClassesRefine( Hcd_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
Vec_IntClear( p->vRefinedC );
Gia_ManForEachAnd( p->pGia, pObj, i )
{
if ( Gia_ObjIsTail(p->pGia, i) ) // add check for the class level
{
Hcd_ManClassRefineOne( p, Gia_ObjRepr(p->pGia, i) );
}
else if ( Gia_ObjIsConst(p->pGia, i) )
{
if ( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) )
Vec_IntPush( p->vRefinedC, i );
}
}
Hcd_ManClassesRehash( p, p->vRefinedC );
}
/**Function*************************************************************
Synopsis [Creates equivalence classes for the first time.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManClassesCreate( Hcd_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
assert( p->pGia->pReprs == NULL );
p->pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pGia) );
p->pGia->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pGia) );
Gia_ManForEachObj( p->pGia, pObj, i )
Gia_ObjSetRepr( p->pGia, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
}
/**Function*************************************************************
Synopsis [Initializes simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManSimulationInit( Hcd_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
Gia_ManForEachCi( p->pGia, pObj, i )
Hcd_ObjSetSim( p, i, (Gia_ManRandom(0) << 1) );
}
/**Function*************************************************************
Synopsis [Performs one round of simple combinational simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Hcd_ManSimulateSimple( Hcd_Man_t * p )
{
Gia_Obj_t * pObj;
unsigned Res0, Res1;
int i;
Gia_ManForEachAnd( p->pGia, pObj, i )
{
Res0 = Hcd_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
Res1 = Hcd_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
Hcd_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
(Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
}
}
/**Function*************************************************************
Synopsis [Resimulate and refine one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Gia_Resimulate_rec( Hcd_Man_t * p, int iObj )
{
Gia_Obj_t * pObj;
unsigned Res0, Res1;
if ( Gia_ObjIsTravIdCurrentId( p->pGia, iObj ) )
return Hcd_ObjSim( p, iObj );
Gia_ObjSetTravIdCurrentId( p->pGia, iObj );
pObj = Gia_ManObj(p->pGia, iObj);
if ( Gia_ObjIsCi(pObj) )
return Hcd_ObjSim( p, iObj );
assert( Gia_ObjIsAnd(pObj) );
Res0 = Gia_Resimulate_rec( p, Gia_ObjFaninId0(pObj, iObj) );
Res1 = Gia_Resimulate_rec( p, Gia_ObjFaninId1(pObj, iObj) );
return Hcd_ObjSetSim( p, iObj, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
(Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
}
/**Function*************************************************************
Synopsis [Resimulate and refine one equivalence class.]
Description [Assumes that the counter-example is assigned at the PIs.
The counter-example should have the first bit set to 0 at each PI.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ResimulateAndRefine( Hcd_Man_t * p, int i )
{
int RetValue, iObj;
Gia_ManIncrementTravId( p->pGia );
Gia_ClassForEachObj( p->pGia, i, iObj )
Gia_Resimulate_rec( p, iObj );
RetValue = Hcd_ManClassRefineOne( p, i );
if ( RetValue == 0 )
printf( "!!! no refinement !!!\n" );
// assert( RetValue );
}
/**Function*************************************************************
Synopsis [Returns temporary representative of the node.]
Description [The temp repr is the first node among the nodes in the class that
(a) precedes the given node, and (b) whose level is lower than the given node.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Gia_Obj_t * Gia_ObjTempRepr( Gia_Man_t * p, int i, int Level )
{
int iRepr, iMember;
iRepr = Gia_ObjRepr( p, i );
if ( !Gia_ObjProved(p, i) )
return NULL;
if ( Gia_ObjFailed(p, i) )
return NULL;
if ( iRepr == GIA_VOID )
return NULL;
if ( iRepr == 0 )
return Gia_ManConst0( p );
// if ( p->pLevels[iRepr] < Level )
// return Gia_ManObj( p, iRepr );
Gia_ClassForEachObj( p, iRepr, iMember )
{
if ( Gia_ObjFailed(p, iMember) )
continue;
if ( iMember >= i )
return NULL;
if ( Gia_ObjLevelId(p, iMember) < Level )
return Gia_ManObj( p, iMember );
}
assert( 0 );
return NULL;
}
/**Function*************************************************************
Synopsis [Generates reduced AIG for the given level.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvRoots )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj, * pRepr;
Vec_Ptr_t * vRoots;
int i;
vRoots = Vec_PtrAlloc( 100 );
// copy unmarked nodes
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_ManHashAlloc( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjLevelId(p, i) > Level )
continue;
if ( Gia_ObjLevelId(p, i) == Level )
Vec_PtrPush( vRoots, pObj );
if ( Gia_ObjLevelId(p, i) < Level && (pRepr = Gia_ObjTempRepr(p, i, Level)) )
{
// printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) );
assert( pRepr < pObj );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
continue;
}
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
*pvRoots = vRoots;
// required by SAT solving
Gia_ManCreateRefs( pNew );
Gia_ManFillValue( pNew );
Gia_ManIncrementTravId( pNew ); // needed for MiniSat to record cexes
// Gia_ManSetPhase( pNew ); // needed if MiniSat is using polarity -- should not be enabled for TAS because fPhase is used to label
return pNew;
}
/**Function*************************************************************
Synopsis [Collects relevant classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_CollectRelatedClasses( Gia_Man_t * pGia, Vec_Ptr_t * vRoots )
{
Vec_Ptr_t * vClasses;
Gia_Obj_t * pRoot, * pRepr;
int i;
vClasses = Vec_PtrAlloc( 100 );
Gia_ManConst0( pGia )->fMark0 = 1;
Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pRoot, i )
{
pRepr = Gia_ObjReprObj( pGia, Gia_ObjId(pGia, pRoot) );
if ( pRepr == NULL || pRepr->fMark0 )
continue;
pRepr->fMark0 = 1;
Vec_PtrPush( vClasses, pRepr );
}
Gia_ManConst0( pGia )->fMark0 = 0;
Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
pRepr->fMark0 = 0;
return vClasses;
}
/**Function*************************************************************
Synopsis [Collects class members.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Obj_t * Gia_CollectClassMembers( Gia_Man_t * p, Gia_Obj_t * pRepr, Vec_Ptr_t * vMembers, int Level )
{
Gia_Obj_t * pTempRepr = NULL;
int iRepr, iMember;
iRepr = Gia_ObjId( p, pRepr );
Vec_PtrClear( vMembers );
Gia_ClassForEachObj( p, iRepr, iMember )
{
if ( Gia_ObjLevelId(p, iMember) == Level )
Vec_PtrPush( vMembers, Gia_ManObj( p, iMember ) );
if ( pTempRepr == NULL && Gia_ObjLevelId(p, iMember) < Level )
pTempRepr = Gia_ManObj( p, iMember );
}
return pTempRepr;
}
/**Function*************************************************************
Synopsis [Packs patterns into array of simulation info.]
Description []
SideEffects []
SeeAlso []
*************************************`**********************************/
int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{
unsigned * pInfo, * pPres;
int i;
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
if ( Abc_InfoHasBit( pPres, iBit ) &&
Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
Abc_InfoSetBit( pPres, iBit );
if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
Abc_InfoXorBit( pInfo, iBit );
}
return 1;
}
/**Function*************************************************************
Synopsis [Procedure to test the new SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GiarfStorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex )
{
int k;
for ( k = 1; k < 32; k++ )
if ( Gia_GiarfStorePatternTry( vSimInfo, vPres, k, (int *)Vec_IntArray(vCex), Vec_IntSize(vCex) ) )
break;
return (int)(k < 32);
}
/**Function*************************************************************
Synopsis [Inserts pattern into simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k )
{
Gia_Obj_t * pObj;
unsigned * pInfo;
int Lit, i;
Vec_IntForEachEntry( vCex, Lit, i )
{
pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) );
pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) );
if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) )
Abc_InfoXorBit( pInfo, k );
}
}
/**Function*************************************************************
Synopsis [Inserts pattern into simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_GiarfPrintClasses( Gia_Man_t * pGia )
{
int nFails = 0;
int nProves = 0;
int nTotal = 0;
int nBoth = 0;
int i;
for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
{
nFails += Gia_ObjFailed(pGia, i);
nProves += Gia_ObjProved(pGia, i);
nTotal += Gia_ObjReprObj(pGia, i) != NULL;
nBoth += Gia_ObjFailed(pGia, i) && Gia_ObjProved(pGia, i);
}
printf( "nFails = %7d. nProves = %7d. nBoth = %7d. nTotal = %7d.\n",
nFails, nProves, nBoth, nTotal );
}
ABC_NAMESPACE_IMPL_END
#include "proof/cec/cecInt.h"
ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t * vOldRoots, int Level, int fUseMiniSat )
{
int fUse2Solver = 0;
Cec_ManSat_t * pSat;
Cec_ParSat_t Pars;
Tas_Man_t * pTas;
Vec_Int_t * vCex;
Vec_Ptr_t * vClasses, * vMembers, * vOldRootsNew;
Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr;
int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember;
int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0;
clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock();
if ( Vec_PtrSize(vOldRoots) == 0 )
return 0;
// start SAT solvers
Cec_ManSatSetDefaultParams( &Pars );
Pars.fPolarFlip = 0;
Pars.nBTLimit = p->nBTLimit;
pSat = Cec_ManSatCreate( pGiaLev, &Pars );
pTas = Tas_ManAlloc( pGiaLev, p->nBTLimit );
if ( fUseMiniSat )
vCex = Cec_ManSatReadCex( pSat );
else
vCex = Tas_ReadModel( pTas );
vMembers = Vec_PtrAlloc( 100 );
Vec_PtrCleanSimInfo( p->vSimPres, 0, 1 );
// resolve constants
Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
{
iRoot = Gia_ObjId( p->pGia, pRoot );
if ( !Gia_ObjIsConst( p->pGia, iRoot ) )
continue;
iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase );
assert( iRootNew != 1 );
if ( fUse2Solver )
{
nTsat++;
clk = clock();
status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
timeTsat += clock() - clk;
if ( status == -1 )
{
nMiniSat++;
clk = clock();
status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
timeMiniSat += clock() - clk;
if ( status == 0 )
{
Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
vCex = Cec_ManSatReadCex( pSat );
}
}
else if ( status == 0 )
vCex = Tas_ReadModel( pTas );
}
else if ( fUseMiniSat )
{
nMiniSat++;
clk = clock();
status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
timeMiniSat += clock() - clk;
if ( status == 0 )
Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
}
else
{
nTsat++;
clk = clock();
status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
timeTsat += clock() - clk;
}
if ( status == -1 ) // undec
{
// Gia_ObjSetFailed( p->pGia, iRoot );
nUndec++;
// Hcd_ManClassClassRemoveOne( p, iRoot );
Gia_ObjSetFailed( p->pGia, iRoot );
}
else if ( status == 1 ) // unsat
{
Gia_ObjSetProved( p->pGia, iRoot );
// printf( "proved constant %d\n", iRoot );
}
else // sat
{
// printf( "Disproved constant %d\n", iRoot );
Gia_ObjUnsetRepr( p->pGia, iRoot ); // do we need this?
nRecords++;
nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
}
}
vClasses = Vec_PtrAlloc( 100 );
vOldRootsNew = Vec_PtrAlloc( 100 );
for ( nIter = 0; Vec_PtrSize(vOldRoots) > 0; nIter++ )
{
// printf( "Iter = %d (Size = %d)\n", nIter, Vec_PtrSize(vOldRoots) );
// resolve equivalences
Vec_PtrClear( vClasses );
Vec_PtrClear( vOldRootsNew );
Gia_ManConst0( p->pGia )->fMark0 = 1;
Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
{
iRoot = Gia_ObjId( p->pGia, pRoot );
if ( Gia_ObjIsHead( p->pGia, iRoot ) )
pRepr = pRoot;
else if ( Gia_ObjIsClass( p->pGia, iRoot ) )
pRepr = Gia_ObjReprObj( p->pGia, iRoot );
else
continue;
if ( pRepr->fMark0 )
continue;
pRepr->fMark0 = 1;
Vec_PtrPush( vClasses, pRepr );
// iRepr = Gia_ObjId( p->pGia, pRepr );
// fTwoMember = Gia_ClassIsPair(p->pGia, iRepr)
// derive temp repr and members on this level
pTempRepr = Gia_CollectClassMembers( p->pGia, pRepr, vMembers, Level );
if ( pTempRepr )
Vec_PtrPush( vMembers, pTempRepr );
if ( Vec_PtrSize(vMembers) < 2 )
continue;
// try proving the members
fOneFailed = 0;
pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers );
Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
{
iMemberPrev = Abc_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase );
iMember = Abc_LitNotCond( pMember->Value, !pMember->fPhase );
assert( iMemberPrev != iMember );
if ( fUse2Solver )
{
nTsat++;
clk = clock();
status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
timeTsat += clock() - clk;
if ( status == -1 )
{
nMiniSat++;
clk = clock();
status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
timeMiniSat += clock() - clk;
if ( status == 0 )
{
Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
vCex = Cec_ManSatReadCex( pSat );
}
}
else if ( status == 0 )
vCex = Tas_ReadModel( pTas );
}
else if ( fUseMiniSat )
{
nMiniSat++;
clk = clock();
status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
timeMiniSat += clock() - clk;
if ( status == 0 )
Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
}
else
{
nTsat++;
clk = clock();
status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
timeTsat += clock() - clk;
}
if ( status == -1 ) // undec
{
// Gia_ObjSetFailed( p->pGia, iRoot );
nUndec++;
if ( Gia_ObjLevel(p->pGia, pMemberPrev) > Gia_ObjLevel(p->pGia, pMember) )
{
// Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMemberPrev) );
Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
}
else
{
// Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMember) );
Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
}
}
else if ( status == 1 ) // unsat
{
// Gia_ObjSetProved( p->pGia, iRoot );
}
else // sat
{
// iRepr = Gia_ObjId( p->pGia, pRepr );
// if ( Gia_ClassIsPair(p->pGia, iRepr) )
// Gia_ClassUndoPair(p->pGia, iRepr);
// else
{
fOneFailed = 1;
nRecords++;
nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
Gia_GiarfInsertPattern( p, vCex, (k % 31) + 1 );
}
}
pMemberPrev = pMember;
// if ( fOneFailed )
// k += Vec_PtrSize(vMembers) / 4;
}
// if fail, quit this class
if ( fOneFailed )
{
nClassRefs++;
Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
if ( pMember != pTempRepr && !Gia_ObjFailed(p->pGia, Gia_ObjId(p->pGia, pMember)) )
Vec_PtrPush( vOldRootsNew, pMember );
clk = clock();
Gia_ResimulateAndRefine( p, Gia_ObjId(p->pGia, pRepr) );
timeSim += clock() - clk;
}
else
{
Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
Gia_ObjSetProved( p->pGia, Gia_ObjId(p->pGia, pMember) );
/*
// }
// else
// {
printf( "Proved equivalent: " );
Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
printf( "%d(L=%d) ", Gia_ObjId(p->pGia, pMember), p->pGia->pLevels[Gia_ObjId(p->pGia, pMember)] );
printf( "\n" );
*/
}
}
Vec_PtrClear( vOldRoots );
Vec_PtrForEachEntry( Gia_Obj_t *, vOldRootsNew, pMember, i )
Vec_PtrPush( vOldRoots, pMember );
// clean up
Gia_ManConst0( p->pGia )->fMark0 = 0;
Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
pRepr->fMark0 = 0;
}
Vec_PtrFree( vClasses );
Vec_PtrFree( vOldRootsNew );
printf( "nSaved = %d nRecords = %d nUndec = %d nClassRefs = %d nMiniSat = %d nTas = %d\n",
nSaved, nRecords, nUndec, nClassRefs, nMiniSat, nTsat );
ABC_PRT( "Tas ", timeTsat );
ABC_PRT( "MiniSat", timeMiniSat );
ABC_PRT( "Sim ", timeSim );
ABC_PRT( "Total ", clock() - timeTotal );
// resimulate
// clk = clock();
Hcd_ManSimulateSimple( p );
Hcd_ManClassesRefine( p );
// ABC_PRT( "Simulate/refine", clock() - clk );
// verify the results
Vec_PtrFree( vMembers );
Tas_ManStop( pTas );
Cec_ManSatStop( pSat );
return nIter;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, int fVerbose )
{
Hcd_Man_t * p;
Vec_Ptr_t * vRoots;
Gia_Man_t * pGiaLev;
int i, Lev, nLevels, nIters;
clock_t clk;
Gia_ManRandom( 1 );
Gia_ManSetPhase( pGia );
nLevels = Gia_ManLevelNum( pGia );
Gia_ManIncrementTravId( pGia );
// start the manager
p = Gia_ManEquivStart( pGia, nBTLimit, fVerbose );
// create trivial classes
Hcd_ManClassesCreate( p );
// refine
for ( i = 0; i < 3; i++ )
{
clk = clock();
Hcd_ManSimulationInit( p );
Hcd_ManSimulateSimple( p );
ABC_PRT( "Sim", clock() - clk );
clk = clock();
Hcd_ManClassesRefine( p );
ABC_PRT( "Ref", clock() - clk );
}
// process in the levelized order
for ( Lev = 1; Lev < nLevels; Lev++ )
{
clk = clock();
printf( "LEVEL %3d (out of %3d) ", Lev, nLevels );
pGiaLev = Gia_GenerateReducedLevel( pGia, Lev, &vRoots );
nIters = Gia_ComputeEquivalencesLevel( p, pGiaLev, vRoots, Lev, fUseMiniSat );
Gia_ManStop( pGiaLev );
Vec_PtrFree( vRoots );
printf( "Iters = %3d " );
ABC_PRT( "Time", clock() - clk );
}
Gia_GiarfPrintClasses( pGia );
// clean up
Gia_ManEquivStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END