mirror of https://github.com/YosysHQ/abc.git
Profiling quantification and other changes.
This commit is contained in:
Alan Mishchenko
parent
94a575a5b3
commit
716969190a
|
|
@ -1091,6 +1091,10 @@ SOURCE=.\src\base\acb\acbSets.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\acb\acbSets.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\acb\acbUtil.c
|
||||
# End Source File
|
||||
# End Group
|
||||
|
|
|
|||
|
|
@ -198,6 +198,7 @@ struct Gia_Man_t_
|
|||
int MappedArea; // area after mapping
|
||||
int MappedDelay; // delay after mapping
|
||||
// bit-parallel simulation
|
||||
int fBuiltInSim;
|
||||
int iPatsPi;
|
||||
int nSimWords;
|
||||
Vec_Wrd_t * vSims;
|
||||
|
|
@ -673,6 +674,11 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
|
|||
if ( pFan1->fMark0 ) pFan1->fMark1 = 1; else pFan1->fMark0 = 1;
|
||||
pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
|
||||
}
|
||||
if ( p->fBuiltInSim )
|
||||
{
|
||||
extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj );
|
||||
Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) );
|
||||
}
|
||||
return Gia_ObjId( p, pObj ) << 1;
|
||||
}
|
||||
static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
|
||||
|
|
@ -1469,6 +1475,10 @@ extern unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i );
|
|||
extern void Gia_ManSimInfoInit( Gia_ManSim_t * p );
|
||||
extern void Gia_ManSimInfoTransfer( Gia_ManSim_t * p );
|
||||
extern void Gia_ManSimulateRound( Gia_ManSim_t * p );
|
||||
extern void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs );
|
||||
extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj );
|
||||
extern int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 );
|
||||
extern int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs );
|
||||
/*=== giaSpeedup.c ============================================================*/
|
||||
extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
|
||||
extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
|
||||
|
|
@ -1612,6 +1622,7 @@ extern void Gia_ManSwapPos( Gia_Man_t * p, int i );
|
|||
extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p );
|
||||
extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
|
||||
extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p );
|
||||
extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 );
|
||||
|
||||
/*=== giaCTas.c ===========================================================*/
|
||||
typedef struct Tas_Man_t_ Tas_Man_t;
|
||||
|
|
|
|||
|
|
@ -1909,7 +1909,7 @@ Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds )
|
|||
Gia_Man_t * pNew; int i, iLit0;
|
||||
Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) );
|
||||
Vec_Int_t * vObjs = Vec_IntAlloc( 1000 );
|
||||
assert( Gia_ObjIsAnd(pRoot) );
|
||||
//assert( Gia_ObjIsAnd(pRoot) );
|
||||
if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
|
||||
Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
|
||||
pNew = Gia_ManStart( Gia_ManObjNum(p) );
|
||||
|
|
|
|||
|
|
@ -748,6 +748,154 @@ void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut )
|
|||
Vec_IntFree( vPatOut );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Bit-parallel simulation during AIG construction.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj )
|
||||
{
|
||||
return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
|
||||
}
|
||||
void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs )
|
||||
{
|
||||
int i, k;
|
||||
assert( !p->fBuiltInSim );
|
||||
assert( Gia_ManAndNum(p) == 0 );
|
||||
p->fBuiltInSim = 1;
|
||||
p->nSimWords = nWords;
|
||||
p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
|
||||
Vec_WrdFill( p->vSims, p->nSimWords, 0 );
|
||||
Gia_ManRandomW( 1 );
|
||||
for ( i = 0; i < Gia_ManCiNum(p); i++ )
|
||||
for ( k = 0; k < p->nSimWords; k++ )
|
||||
Vec_WrdPush( p->vSims, Gia_ManRandomW(0) );
|
||||
}
|
||||
void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj )
|
||||
{
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
|
||||
word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
|
||||
word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); int w;
|
||||
assert( p->fBuiltInSim );
|
||||
if ( Gia_ObjFaninC0(pObj) )
|
||||
{
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
Vec_WrdPush( p->vSims, ~(pInfo0[w] | pInfo1[w]) );
|
||||
else
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
Vec_WrdPush( p->vSims, ~pInfo0[w] & pInfo1[w] );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
Vec_WrdPush( p->vSims, pInfo0[w] & ~pInfo1[w] );
|
||||
else
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
Vec_WrdPush( p->vSims, pInfo0[w] & pInfo1[w] );
|
||||
}
|
||||
assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords );
|
||||
}
|
||||
int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 )
|
||||
{
|
||||
word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
|
||||
word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
|
||||
assert( p->fBuiltInSim );
|
||||
|
||||
// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
|
||||
// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
|
||||
// Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
|
||||
// printf( "\n" );
|
||||
|
||||
if ( Abc_LitIsCompl(iLit0) )
|
||||
{
|
||||
if ( Abc_LitIsCompl(iLit1) )
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
if ( ~pInfo0[w] & ~pInfo1[w] )
|
||||
return 1;
|
||||
else
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
if ( ~pInfo0[w] & pInfo1[w] )
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( Abc_LitIsCompl(iLit1) )
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
if ( pInfo0[w] & ~pInfo1[w] )
|
||||
return 1;
|
||||
else
|
||||
for ( w = 0; w < p->nSimWords; w++ )
|
||||
if ( pInfo0[w] & pInfo1[w] )
|
||||
return 1;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Finds a satisfying assignment.]
|
||||
|
||||
Description [Returns 1 if a sat assignment is found; 0 otherwise.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManObjCheckSat_rec( Gia_Man_t * p, int iLit, Vec_Int_t * vObjs )
|
||||
{
|
||||
int iObj = Abc_Lit2Var(iLit);
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
|
||||
if ( pObj->fMark0 )
|
||||
return pObj->fMark1 == (unsigned)Abc_LitIsCompl(iLit);
|
||||
pObj->fMark0 = 1;
|
||||
pObj->fMark1 = Abc_LitIsCompl(iLit);
|
||||
Vec_IntPush( vObjs, iObj );
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
if ( pObj->fMark1 == 0 ) // node value is 1
|
||||
{
|
||||
if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit0(pObj, iObj), vObjs ) ) return 0;
|
||||
if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit1(pObj, iObj), vObjs ) ) return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( !Gia_ManObjCheckSat_rec( p, Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj)), vObjs ) ) return 0;
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
int Gia_ManObjCheckOverlap1( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, Res0, Res1 = 0;
|
||||
// Gia_ManForEachObj( p, pObj, i )
|
||||
// assert( pObj->fMark0 == 0 && pObj->fMark1 == 0 );
|
||||
Vec_IntClear( vObjs );
|
||||
Res0 = Gia_ManObjCheckSat_rec( p, iLit0, vObjs );
|
||||
if ( Res0 )
|
||||
Res1 = Gia_ManObjCheckSat_rec( p, iLit1, vObjs );
|
||||
Gia_ManForEachObjVec( vObjs, p, pObj, i )
|
||||
pObj->fMark0 = pObj->fMark1 = 0;
|
||||
return Res0 && Res1;
|
||||
}
|
||||
int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
|
||||
{
|
||||
if ( Gia_ManObjCheckOverlap1( p, iLit0, iLit1, vObjs ) )
|
||||
return 1;
|
||||
return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -2075,6 +2075,58 @@ void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName )
|
|||
fclose( pTable );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Check if two logic cones have overlap.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManCheckSuppMark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj->fMark0 )
|
||||
return;
|
||||
pObj->fMark0 = 1;
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
return;
|
||||
Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin0(pObj) );
|
||||
Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin1(pObj) );
|
||||
}
|
||||
void Gia_ManCheckSuppUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( !pObj->fMark0 )
|
||||
return;
|
||||
pObj->fMark0 = 0;
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
return;
|
||||
Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin0(pObj) );
|
||||
Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin1(pObj) );
|
||||
}
|
||||
int Gia_ManCheckSupp_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj->fMark0 )
|
||||
return 1;
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
return 0;
|
||||
if ( Gia_ManCheckSupp_rec( p, Gia_ObjFanin0(pObj) ) )
|
||||
return 1;
|
||||
return Gia_ManCheckSupp_rec( p, Gia_ObjFanin1(pObj) );
|
||||
}
|
||||
int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 )
|
||||
{
|
||||
int Result;
|
||||
if ( iNode1 == 0 || iNode2 == 0 )
|
||||
return 0;
|
||||
Gia_ManCheckSuppMark_rec( p, Gia_ManObj(p, iNode1) );
|
||||
Result = Gia_ManCheckSupp_rec( p, Gia_ManObj(p, iNode2) );
|
||||
Gia_ManCheckSuppUnmark_rec( p, Gia_ManObj(p, iNode1) );
|
||||
return Result;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -0,0 +1,61 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [acbSets.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Hierarchical word-level netlist.]
|
||||
|
||||
Synopsis [Reading data from file.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - July 21, 2015.]
|
||||
|
||||
Revision [$Id: acbSets.h,v 1.00 2017/04/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__base__acb__acbSets_h
|
||||
#define ABC__base__acb__acbSets_h
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// ITERATORS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -745,16 +745,16 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSatVars, Vec_Int_t * vVar2Index )
|
||||
Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSatVars, Vec_Int_t * vVar2Index, int CubeLimit )
|
||||
{
|
||||
int fCreatePrime = 1;
|
||||
int nSupp = Vec_IntSize(vCiSatVars);
|
||||
int nCubes, nSupp = Vec_IntSize(vCiSatVars);
|
||||
Vec_Str_t * vSop = Vec_StrAlloc( 1000 );
|
||||
Vec_Int_t * vLits = Vec_IntAlloc( nSupp );
|
||||
Vec_Str_t * vCube = Vec_StrAlloc( nSupp + 4 );
|
||||
Vec_StrFill( vCube, nSupp, '-' );
|
||||
Vec_StrPrintF( vCube, " 1\n\0" );
|
||||
while ( 1 )
|
||||
for ( nCubes = 0; !CubeLimit || nCubes < CubeLimit; nCubes++ )
|
||||
{
|
||||
int * pFinal, nFinal, iVar, i, k = 0;
|
||||
// generate onset minterm
|
||||
|
|
@ -803,7 +803,7 @@ Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSat
|
|||
Vec_StrPush( vSop, '\0' );
|
||||
return vSop;
|
||||
}
|
||||
Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p )
|
||||
Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit )
|
||||
{
|
||||
bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() };
|
||||
|
||||
|
|
@ -838,7 +838,7 @@ Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p )
|
|||
Vec_IntWriteEntry( vVarMap, iFirstVar+i, i );
|
||||
}
|
||||
|
||||
Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap );
|
||||
Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap, CubeLimit );
|
||||
Vec_IntFree( vVarMap );
|
||||
Vec_IntFree( vVars );
|
||||
|
||||
|
|
@ -846,13 +846,53 @@ Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p )
|
|||
bmcg_sat_solver_stop( pSat[1] );
|
||||
return vSop;
|
||||
}
|
||||
void Glucose_GenerateSopTest( Gia_Man_t * p )
|
||||
void bmcg_sat_solver_sopTest( Gia_Man_t * p )
|
||||
{
|
||||
Vec_Str_t * vSop = Glucose_GenerateSop( p );
|
||||
Vec_Str_t * vSop = bmcg_sat_solver_sop( p, 0 );
|
||||
printf( "%s", Vec_StrArray(vSop) );
|
||||
Vec_StrFree( vSop );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computing d-literals.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
#define Gia_CubeForEachVar( pCube, Value, i ) \
|
||||
for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
|
||||
#define Gia_SopForEachCube( pSop, nFanins, pCube ) \
|
||||
for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
|
||||
|
||||
void bmcg_sat_generate_dvars( Vec_Int_t * vCiVars, Vec_Str_t * vSop, Vec_Int_t * vDLits )
|
||||
{
|
||||
int i, Lit, Counter, nCubes = 0;
|
||||
char Value, * pCube, * pSop = Vec_StrArray( vSop );
|
||||
Vec_Int_t * vCounts = Vec_IntStart( 2*Vec_IntSize(vCiVars) );
|
||||
Vec_IntClear( vDLits );
|
||||
Gia_SopForEachCube( pSop, Vec_IntSize(vCiVars), pCube )
|
||||
{
|
||||
nCubes++;
|
||||
Gia_CubeForEachVar( pCube, Value, i )
|
||||
{
|
||||
if ( Value == '1' )
|
||||
Vec_IntAddToEntry( vCounts, 2*i, 1 );
|
||||
else if ( Value == '0' )
|
||||
Vec_IntAddToEntry( vCounts, 2*i+1, 1 );
|
||||
}
|
||||
}
|
||||
Vec_IntForEachEntry( vCounts, Counter, Lit )
|
||||
if ( Counter == nCubes )
|
||||
Vec_IntPush( vDLits, Abc_Var2Lit(Vec_IntEntry(vCiVars, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)) );
|
||||
Vec_IntSort( vDLits, 0 );
|
||||
Vec_IntFree( vCounts );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs SAT-based quantification.]
|
||||
|
|
@ -864,20 +904,29 @@ void Glucose_GenerateSopTest( Gia_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData )
|
||||
|
||||
abctime clkQuaSetup = 0;
|
||||
abctime clkQuaSolve = 0;
|
||||
abctime clkQuaSynth = 0;
|
||||
|
||||
int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
|
||||
{
|
||||
abctime clk = Abc_Clock(), clkAll = Abc_Clock();
|
||||
extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
|
||||
Gia_Man_t * pMan, * pNew, * pTemp; Vec_Str_t * vSop;
|
||||
int i, CiId, ObjId, Res, Count = 0, iNode = Abc_Lit2Var(iLit);
|
||||
int i, CiId, ObjId, Res, nCubes, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit);
|
||||
Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 );
|
||||
Gia_ManCollectCis( p, &iNode, 1, vCisUsed );
|
||||
Vec_IntSort( vCisUsed, 0 );
|
||||
if ( vDLits ) Vec_IntClear( vDLits );
|
||||
if ( iLit < 2 )
|
||||
return iLit;
|
||||
// remap into CI Ids
|
||||
Vec_IntForEachEntry( vCisUsed, ObjId, i )
|
||||
Vec_IntWriteEntry( vCisUsed, i, Gia_ManIdToCioId(p, ObjId) );
|
||||
// duplicate cone
|
||||
pNew = Gia_ManDupConeSupp( p, iLit, vCisUsed );
|
||||
assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCisUsed) );
|
||||
//Gia_AigerWrite( pNew, "test1.aig", 0, 0 );
|
||||
|
||||
// perform quantification one CI at a time
|
||||
assert( pFuncCiToKeep );
|
||||
|
|
@ -889,7 +938,7 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
|
|||
Gia_ManStop( pTemp );
|
||||
Count++;
|
||||
}
|
||||
//Gia_AigerWrite( pNew, "test2.aig", 0, 0 );
|
||||
clkQuaSetup += Abc_Clock() - clk;
|
||||
if ( Gia_ManPoIsConst(pNew, 0) )
|
||||
{
|
||||
int RetValue = Gia_ManPoIsConst1(pNew, 0);
|
||||
|
|
@ -898,13 +947,25 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
|
|||
return RetValue;
|
||||
}
|
||||
|
||||
vSop = Glucose_GenerateSop( pNew );
|
||||
clk = Abc_Clock();
|
||||
vSop = bmcg_sat_solver_sop( pNew, 0 );
|
||||
nNodes = Gia_ManAndNum(pNew);
|
||||
Gia_ManStop( pNew );
|
||||
clkQuaSolve += Abc_Clock() - clk;
|
||||
|
||||
printf( "Computed # with %d keep-vars and %d quant-vars with %d cubes.\n",
|
||||
Vec_IntSize(vCisUsed) - Count, Count, Vec_StrCountEntry(vSop, '\n') );
|
||||
|
||||
pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 0 );
|
||||
clk = Abc_Clock();
|
||||
pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 );
|
||||
clkQuaSynth += Abc_Clock() - clk;
|
||||
nCubes = Vec_StrCountEntry(vSop, '\n');
|
||||
if ( vDLits )
|
||||
{
|
||||
// convert into object IDs
|
||||
Vec_Int_t * vCisObjs = Vec_IntAlloc( Vec_IntSize(vCisUsed) );
|
||||
Vec_IntForEachEntry( vCisUsed, CiId, i )
|
||||
Vec_IntPush( vCisObjs, CiId + 1 );
|
||||
bmcg_sat_generate_dvars( vCisObjs, vSop, vDLits );
|
||||
Vec_IntFree( vCisObjs );
|
||||
}
|
||||
Vec_StrFree( vSop );
|
||||
if ( Gia_ManPoIsConst(pMan, 0) )
|
||||
{
|
||||
|
|
@ -915,13 +976,18 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT
|
|||
}
|
||||
|
||||
Res = Gia_ManDupConeBack( p, pMan, vCisUsed );
|
||||
|
||||
// report the result
|
||||
printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ",
|
||||
nNodes, Vec_IntSize(vCisUsed) - Count, Count, nCubes, Gia_ManAndNum(pMan) );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll );
|
||||
|
||||
Vec_IntFree( vCisUsed );
|
||||
Gia_ManStop( pMan );
|
||||
return Res;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs SAT-based quantification.]
|
||||
|
|
@ -1001,16 +1067,20 @@ int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, in
|
|||
Gia_ManStop( pMan );
|
||||
return Result;
|
||||
}
|
||||
int bmcg_sat_solver_quantify3( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData )
|
||||
int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
|
||||
{
|
||||
return bmcg_sat_solver_quantify2( p, iLit, fHash, pFuncCiToKeep, pData );
|
||||
return bmcg_sat_solver_quantify2( p, iLit, fHash, pFuncCiToKeep, pData, vDLits );
|
||||
}
|
||||
int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData )
|
||||
int bmcg_sat_solver_quantify3( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
|
||||
{
|
||||
abctime clk, clkAll = Abc_Clock();
|
||||
Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); // GIA objs
|
||||
Vec_Int_t * vCiVars = Vec_IntAlloc( 100 ); // CI SAT vars
|
||||
Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL;
|
||||
int i, iVar, iVarLast, Lit, RetValue, Count = 0, Result = -1;
|
||||
if ( vDLits ) Vec_IntClear( vDLits );
|
||||
if ( iLit < 2 )
|
||||
return iLit;
|
||||
if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
|
||||
Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
|
||||
// assign variable number 0 to const0 node
|
||||
|
|
@ -1018,10 +1088,15 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
|
|||
Vec_IntPush( vObjsUsed, 0 );
|
||||
Gia_ObjSetCopyArray( p, 0, iVar );
|
||||
assert( iVar == 0 );
|
||||
|
||||
// collect other variables
|
||||
clk = Abc_Clock();
|
||||
iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCiVars );
|
||||
Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
|
||||
clkQuaSetup += Abc_Clock() - clk;
|
||||
|
||||
// check constants
|
||||
clk = Abc_Clock();
|
||||
Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) );
|
||||
RetValue = bmcg_sat_solver_addclause( pSats[0], &Lit, 1 ); // offset
|
||||
if ( !RetValue || bmcg_sat_solver_solve(pSats[0], NULL, 0) == GLUCOSE_UNSAT )
|
||||
|
|
@ -1036,6 +1111,26 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
|
|||
Result = 0;
|
||||
goto cleanup;
|
||||
}
|
||||
/*
|
||||
// reorder CI SAT variables to have keep-vars first
|
||||
Vec_Int_t * vCiVars2 = Vec_IntAlloc( 100 ); // CI SAT vars
|
||||
Vec_IntForEachEntry( vCiVars, iVar, i )
|
||||
{
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
|
||||
assert( Gia_ObjIsCi(pObj) );
|
||||
if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
|
||||
Vec_IntPush( vCiVars2, iVar );
|
||||
}
|
||||
Vec_IntForEachEntry( vCiVars, iVar, i )
|
||||
{
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
|
||||
assert( Gia_ObjIsCi(pObj) );
|
||||
if ( !pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
|
||||
Vec_IntPush( vCiVars2, iVar );
|
||||
}
|
||||
ABC_SWAP( Vec_Int_t *, vCiVars2, vCiVars );
|
||||
Vec_IntFree( vCiVars2 );
|
||||
*/
|
||||
// map CI SAT variables into their indexes used in the cubes
|
||||
vVarMap = Vec_IntStartFull( Vec_IntSize(vObjsUsed) );
|
||||
Vec_IntForEachEntry( vCiVars, iVar, i )
|
||||
|
|
@ -1045,16 +1140,32 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit
|
|||
if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
|
||||
Vec_IntWriteEntry( vVarMap, iVar, i ), Count++;
|
||||
}
|
||||
if ( Count == 0 || Count == Vec_IntSize(vCiVars) )
|
||||
{
|
||||
Result = Count == 0 ? 1 : iLit;
|
||||
goto cleanup;
|
||||
}
|
||||
// generate cubes
|
||||
vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap );
|
||||
vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap, 0 );
|
||||
clkQuaSolve += Abc_Clock() - clk;
|
||||
//printf( "%s", Vec_StrArray(vSop) );
|
||||
printf( "Computed # with %d keep-vars and %d quant-vars with %d cubes.\n",
|
||||
Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n') );
|
||||
// convert into object IDs
|
||||
Vec_IntForEachEntry( vCiVars, iVar, i )
|
||||
Vec_IntWriteEntry( vCiVars, i, Vec_IntEntry(vObjsUsed, iVar) );
|
||||
// generate unate variables
|
||||
if ( vDLits )
|
||||
bmcg_sat_generate_dvars( vCiVars, vSop, vDLits );
|
||||
// convert into an AIG
|
||||
clk = Abc_Clock();
|
||||
RetValue = Gia_ManAndNum(p);
|
||||
Result = Gia_ManFactorSop( p, vCiVars, vSop, fHash );
|
||||
clkQuaSynth += Abc_Clock() - clk;
|
||||
|
||||
// report the result
|
||||
printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ",
|
||||
Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll );
|
||||
|
||||
cleanup:
|
||||
Vec_IntForEachEntry( vObjsUsed, iVar, i )
|
||||
Gia_ObjSetCopyArray( p, iVar, -1 );
|
||||
|
|
@ -1074,11 +1185,11 @@ void Glucose_QuantifyAigTest( Gia_Man_t * p )
|
|||
bmcg_sat_solver * pSats[3] = { bmcg_sat_solver_start(), bmcg_sat_solver_start(), bmcg_sat_solver_start() };
|
||||
|
||||
abctime clk1 = Abc_Clock();
|
||||
int iRes1 = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL );
|
||||
int iRes1 = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL, NULL );
|
||||
abctime clk1d = Abc_Clock()-clk1;
|
||||
|
||||
abctime clk2 = Abc_Clock();
|
||||
int iRes2 = bmcg_sat_solver_quantify2( p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL );
|
||||
int iRes2 = bmcg_sat_solver_quantify2( p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL, NULL );
|
||||
abctime clk2d = Abc_Clock()-clk2;
|
||||
|
||||
Abc_PrintTime( 1, "Time1", clk1d );
|
||||
|
|
@ -1108,8 +1219,12 @@ void Glucose_QuantifyAigTest( Gia_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
abctime clkTrav = 0;
|
||||
abctime clkSatRun = 0;
|
||||
|
||||
int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv )
|
||||
{
|
||||
abctime clk;
|
||||
bmcg_sat_solver * pSats[2] = { pSat, NULL };
|
||||
Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 );
|
||||
int i, iVar, iSatVar[2], iSatLit[2], Lits[2], status;
|
||||
|
|
@ -1122,14 +1237,25 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
|
|||
Gia_ObjSetCopyArray( p, 0, iVar );
|
||||
assert( iVar == 0 );
|
||||
|
||||
//printf( "%d ", iLit0 );
|
||||
//printf( "%d ", iLit1 );
|
||||
//printf( " -> " );
|
||||
clk = Abc_Clock();
|
||||
iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL );
|
||||
//printf( "%d ", Vec_IntSize(vObjsUsed) );
|
||||
iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL );
|
||||
clkTrav += Abc_Clock() - clk;
|
||||
//printf( "%d ", Vec_IntSize(vObjsUsed) );
|
||||
//printf( "\n" );
|
||||
|
||||
iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) );
|
||||
iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) );
|
||||
Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
|
||||
Vec_IntForEachEntry( vObjsUsed, iVar, i )
|
||||
Gia_ObjSetCopyArray( p, iVar, -1 );
|
||||
Vec_IntFree( vObjsUsed );
|
||||
|
||||
clk = Abc_Clock();
|
||||
if ( fEquiv )
|
||||
{
|
||||
Lits[0] = iSatLit[0];
|
||||
|
|
@ -1141,6 +1267,7 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
|
|||
Lits[1] = iSatLit[1];
|
||||
status = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
|
||||
}
|
||||
clkSatRun += Abc_Clock() - clk;
|
||||
return status == GLUCOSE_UNSAT;
|
||||
}
|
||||
else
|
||||
|
|
@ -1148,6 +1275,7 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
|
|||
Lits[0] = iSatLit[0];
|
||||
Lits[1] = iSatLit[1];
|
||||
status = bmcg_sat_solver_solve( pSats[0], Lits, 2 );
|
||||
clkSatRun += Abc_Clock() - clk;
|
||||
return status == GLUCOSE_SAT;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -93,8 +93,9 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
|
|||
extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
|
||||
extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot );
|
||||
extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
|
||||
extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData );
|
||||
extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
|
||||
extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
|
||||
extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
|
||||
|
||||
extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
|
||||
extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
|
||||
|
|
|
|||
Loading…
Reference in New Issue