Skip to content

A
abc
Commit 31f88974 by Alan Mishchenko
Options

Various changes.

parent eb44a80b
Showing with 62 additions and 38 deletions
src/aig/gia/gia.h
......@@ -548,6 +548,7 @@ static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) {
static inline int Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; }
static inline int Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; }
static inline int Gia_ManCoDriverId( Gia_Man_t * p, int iCoIndex ) { return Gia_ObjFaninId0p(p, Gia_ManCo(p, iCoIndex)); }
static inline int Gia_ManPoIsConst( Gia_Man_t * p, int iPoIndex ) { return Gia_ObjFaninId0p(p, Gia_ManPo(p, iPoIndex)) == 0; }
static inline int Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
static inline int Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
......
src/misc/vec/vecStr.h
......@@ -561,6 +561,11 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
}
p->pArray[p->nSize++] = Entry;
}
static inline void Vec_StrPushTwo( Vec_Str_t * p, char Entry1, char Entry2 )
{
Vec_StrPush( p, Entry1 );
Vec_StrPush( p, Entry2 );
}
static inline void Vec_StrPushBuffer( Vec_Str_t * p, char * pBuffer, int nSize )
{
if ( p->nSize + nSize > p->nCap )
......
src/proof/cec/cec.h
......@@ -101,6 +101,7 @@ struct Cec_ParFra_t_
int nRounds; // the number of simulation rounds
int nItersMax; // the maximum number of iterations of SAT sweeping
int nBTLimit; // conflict limit at a node
int nBTLimitPo; // conflict limit at an output
int TimeLimit; // the runtime limit in seconds
int nLevelMax; // restriction on the level nodes to be swept
int nDepthMax; // the depth in terms of steps of speculative reduction
......
src/proof/cec/cecSatG2.c
......@@ -98,13 +98,12 @@ struct Cec4_Man_t_
Vec_Int_t * vCands;
Vec_Int_t * vVisit;
Vec_Int_t * vPat;
Vec_Int_t * vPats;
Vec_Int_t * vDisprPairs;
Vec_Bit_t * vFails;
Vec_Bit_t * vCoDrivers;
int iPosRead; // candidate reading position
int iPosWrite; // candidate writing position
int iLastConst; // last const node proved
int nPatsAll;
// refinement
Vec_Int_t * vRefClasses;
Vec_Int_t * vRefNodes;
......@@ -162,25 +161,16 @@ Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWo
{
//Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords );
Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords );
int i, k, iPat = 0;
for ( i = 0; i < Vec_IntSize(vPats); )
{
int Size = Vec_IntEntry(vPats, i);
assert( Size > 0 );
for ( k = 1; k <= Size; k++ )
{
int iLit = Vec_IntEntry( vPats, i+k );
word * pSim;
if ( iLit == 0 )
continue;
assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
Abc_InfoXorBit( (unsigned*)pSim, iPat );
}
iPat++;
i += Size + 1;
}
int i, k, iLit, iPat = 0; word * pSim;
for ( i = 0; i < Vec_IntSize(vPats); i += Vec_IntEntry(vPats, i), iPat++ )
for ( k = 1; k < Vec_IntEntry(vPats, i)-1; k++ )
if ( (iLit = Vec_IntEntry(vPats, i+k)) )
{
assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
Abc_InfoXorBit( (unsigned*)pSim, iPat );
}
assert( iPat == nPats );
return vSimsPi;
}
......@@ -224,6 +214,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars )
pPars->nRounds = 10; // simulation rounds
pPars->nItersMax = 2000; // this is a miter
pPars->nBTLimit = 1000000; // use logic cones
pPars->nBTLimitPo = 0; // use logic outputs
pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver
pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver
pPars->nGenIters = 100; // pattern generation iterations
......@@ -257,10 +248,18 @@ 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 );
p->vPats = Vec_IntAlloc( 10000 );
p->vDisprPairs = Vec_IntAlloc( 100 );
p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) );
//pAig->pData = p->pSat; // point AIG manager to the solver
//Vec_IntFreeP( &p->pAig->vPats );
//p->pAig->vPats = Vec_IntAlloc( 1000 );
if ( pPars->nBTLimitPo )
{
int i, Driver;
p->vCoDrivers = Vec_BitStart( Gia_ManObjNum(pAig) );
Gia_ManForEachCoDriverId( pAig, Driver, i )
Vec_BitWriteEntry( p->vCoDrivers, Driver, 1 );
}
return p;
}
void Cec4_ManDestroy( Cec4_Man_t * p )
......@@ -287,11 +286,9 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
fflush( stdout );
}
//printf( "Recorded %d patterns with %d literals (average %.2f).\n",
// p->nPatsAll, Vec_IntSize(p->vPats) - p->nPatsAll, 1.0*Vec_IntSize(p->vPats)/Abc_MaxInt(1, p->nPatsAll)-1 );
//Cec4_EvalPatterns( p->pAig, p->vPats, p->nPatsAll );
//Vec_IntFreeP( &p->vPats );
Vec_IntFreeP( &p->pAig->vPats );
p->pAig->vPats = p->vPats;
// p->pAig->nBitPats, Vec_IntSize(p->pAig->vPats) - 2*p->pAig->nBitPats, 1.0*Vec_IntSize(p->pAig->vPats)/Abc_MaxInt(1, p->pAig->nBitPats)-2 );
//Cec4_EvalPatterns( p->pAig, p->pAig->vPats, p->pAig->nBitPats );
//Vec_IntFreeP( &p->pAig->vPats );
Vec_WrdFreeP( &p->pAig->vSims );
Vec_WrdFreeP( &p->pAig->vSimsPi );
Gia_ManCleanMark01( p->pAig );
......@@ -307,6 +304,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
Vec_IntFreeP( &p->vPat );
Vec_IntFreeP( &p->vDisprPairs );
Vec_BitFreeP( &p->vFails );
Vec_BitFreeP( &p->vCoDrivers );
Vec_IntFreeP( &p->vRefClasses );
Vec_IntFreeP( &p->vRefNodes );
Vec_IntFreeP( &p->vRefBins );
......@@ -1458,9 +1456,12 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
if ( Res )
{
int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 );
Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
Vec_IntAppend( p->vPats, p->vPat );
p->nPatsAll++;
if ( p->pAig->vPats )
{
Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
Vec_IntAppend( p->pAig->vPats, p->vPat );
Vec_IntPush( p->pAig->vPats, -1 );
}
//Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand );
Packs += Ret;
if ( Ret == 64 * p->pAig->nSimWords )
......@@ -1506,12 +1507,13 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
Vec_IntClear( &p->pNew->vCopiesTwo ); // pairs (CiAigId, SatId)
Vec_IntClear( &p->pNew->vVarMap ); // mapping of SatId into AigId
}
int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose, int fEffort )
{
abctime clk;
int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
int nBTLimit = fEffort ? p->pPars->nBTLimitPo : (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
int UnsatConflicts[3] = {0};
//printf( "%d ", nBTLimit );
if ( iObj1 < iObj0 )
iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
assert( iObj0 < iObj1 );
......@@ -1567,8 +1569,6 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
*pfEasy = nConfEnd == nConfBeg;
}
}
else
return status;
}
if ( status == GLUCOSE_UNSAT && iObj0 > 0 )
{
......@@ -1601,6 +1601,8 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
}
}
}
//if ( status == GLUCOSE_UNDEC )
// printf( "* " );
return status;
}
int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
......@@ -1610,7 +1612,8 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
int fEffort = p->vCoDrivers ? Vec_BitEntry(p->vCoDrivers, iObj) || Vec_BitEntry(p->vCoDrivers, iRepr) : 0;
status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose, fEffort );
if ( status == GLUCOSE_SAT )
{
int iLit;
......@@ -1635,9 +1638,12 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
p->pAig->iPatsPi++;
Vec_IntForEachEntry( p->vPat, iLit, i )
Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
Vec_IntAppend( p->vPats, p->vPat );
p->nPatsAll++;
if ( p->pAig->vPats )
{
Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
Vec_IntAppend( p->pAig->vPats, p->vPat );
Vec_IntPush( p->pAig->vPats, -1 );
}
//Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 );
//assert( iPatsOld + 1 == p->pAig->iPatsPi );
if ( fEasy )
......@@ -1887,6 +1893,17 @@ Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose )
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
return pNew;
}
Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose )
{
Gia_Man_t * pNew = NULL;
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec4_ManSetParams( pPars );
pPars->fVerbose = fVerbose;
pPars->nBTLimit = nBTLimit;
pPars->nBTLimitPo = nBTLimitPo;
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
return pNew;
}
int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose )
{
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
......
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