Skip to content

A
abc
Commit 486eacc5 by Alan Mishchenko
Options

SAT sweeping under constraints.

parent 005f0e39
Showing with 1461 additions and 173 deletions
Makefile
...@@ -23,7 +23,7 @@ MODULES := \ ...@@ -23,7 +23,7 @@ MODULES := \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \ src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/proof/abs \ src/proof/abs src/proof/ssc \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/aig/miniaig \ src/aig/miniaig \
src/python src/python
......
abcexe.dsp
...@@ -89,6 +89,10 @@ LINK32=link.exe ...@@ -89,6 +89,10 @@ LINK32=link.exe
SOURCE=.\src\base\main\main.c SOURCE=.\src\base\main\main.c
# End Source File # End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satSolver.c
# End Source File
# End Group # End Group
# Begin Group "Header Files" # Begin Group "Header Files"
......
abclib.dsp
...@@ -4522,6 +4522,38 @@ SOURCE=.\src\proof\abs\absUtil.c ...@@ -4522,6 +4522,38 @@ SOURCE=.\src\proof\abs\absUtil.c
SOURCE=.\src\proof\abs\absVta.c SOURCE=.\src\proof\abs\absVta.c
# End Source File # End Source File
# End Group # End Group
# Begin Group "ssc"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\proof\ssc\ssc.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscClass.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscCore.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscInt.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscSat.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscSim.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\ssc\sscUtil.c
# End Source File
# End Group
# End Group # End Group
# End Group # End Group
# Begin Group "Header Files" # Begin Group "Header Files"
......
src/aig/gia/gia.h
...@@ -167,6 +167,12 @@ struct Gia_Man_t_ ...@@ -167,6 +167,12 @@ struct Gia_Man_t_
int iData2; // various user data int iData2; // various user data
int nAnd2Delay; // AND2 delay scaled to match delay numbers used int nAnd2Delay; // AND2 delay scaled to match delay numbers used
int fVerbose; // verbose reports int fVerbose; // verbose reports
// bit-parallel simulation
int iPatsPi;
Vec_Wrd_t * vSims;
Vec_Wrd_t * vSimsPi;
Vec_Int_t * vClassOld;
Vec_Int_t * vClassNew;
// truth table computation for small functions // truth table computation for small functions
int nTtVars; // truth table variables int nTtVars; // truth table variables
int nTtWords; // truth table words int nTtWords; // truth table words
...@@ -379,7 +385,7 @@ static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * ...@@ -379,7 +385,7 @@ static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t *
static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); }
static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); }
static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); }
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); }
...@@ -423,6 +429,11 @@ static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * ...@@ -423,6 +429,11 @@ static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t *
static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); }
static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); }
static inline int Gia_ObjSimWords( Gia_Man_t * p ) { return Vec_WrdSize( p->vSimsPi ) / Gia_ManPiNum( p ); }
static inline word * Gia_ObjSimPi( Gia_Man_t * p, int PiId ) { return Vec_WrdEntryP( p->vSimsPi, PiId * Gia_ObjSimWords(p) ); }
static inline word * Gia_ObjSim( Gia_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vSims, Id * Gia_ObjSimWords(p) ); }
static inline word * Gia_ObjSimObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjSim( p, Gia_ObjId(p, pObj) ); }
// AIG construction // AIG construction
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p ) static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
...@@ -755,6 +766,8 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re ...@@ -755,6 +766,8 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
#define Gia_ManForEachAnd( p, pObj, i ) \ #define Gia_ManForEachAnd( p, pObj, i ) \
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachCand( p, pObj, i ) \
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsCand(pObj) ) {} else
#define Gia_ManForEachAndReverse( p, pObj, i ) \ #define Gia_ManForEachAndReverse( p, pObj, i ) \
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachCi( p, pObj, i ) \ #define Gia_ManForEachCi( p, pObj, i ) \
...@@ -837,6 +850,7 @@ extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames ); ...@@ -837,6 +850,7 @@ extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo );
extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo );
extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo );
extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
...@@ -859,6 +873,7 @@ extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); ...@@ -859,6 +873,7 @@ extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p );
/*=== giaEnable.c ==========================================================*/ /*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
...@@ -921,6 +936,7 @@ extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit ...@@ -921,6 +936,7 @@ extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit
extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ); extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
extern void Gia_ManHashProfile( Gia_Man_t * p ); extern void Gia_ManHashProfile( Gia_Man_t * p );
extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
/*=== giaIf.c ===========================================================*/ /*=== giaIf.c ===========================================================*/
extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); extern void Gia_ManPrintMappingStats( Gia_Man_t * p );
extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p );
...@@ -1015,7 +1031,7 @@ extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, i ...@@ -1015,7 +1031,7 @@ extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, i
extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ); extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames );
extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime ); extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime );
extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc ); extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc );
extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ); extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose );
/*=== giaSwitch.c ============================================================*/ /*=== giaSwitch.c ============================================================*/
extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
...@@ -1075,6 +1091,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); ...@@ -1075,6 +1091,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrint( Gia_Man_t * p ); extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern void Gia_ManInvertPos( Gia_Man_t * pAig );
extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 ); extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p ); extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
......
src/aig/gia/giaDup.c
...@@ -577,7 +577,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) ...@@ -577,7 +577,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
if ( pNew->nRegs > 0 ) if ( pNew->nRegs > 0 )
pNew->nRegs = 0; pNew->nRegs = 0;
if ( pNew->pHTable == NULL ) if ( pNew->pHTable == NULL )
Gia_ManHashAlloc( pNew ); Gia_ManHashStart( pNew );
Gia_ManConst0(pTwo)->Value = 0; Gia_ManConst0(pTwo)->Value = 0;
Gia_ManForEachObj1( pTwo, pObj, i ) Gia_ManForEachObj1( pTwo, pObj, i )
{ {
...@@ -589,19 +589,24 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) ...@@ -589,19 +589,24 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
} }
} }
void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
{
/**Function************************************************************* Gia_Obj_t * pObj;
int i;
Synopsis [Append second AIG on top of the first with the permutation.] assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) );
if ( pNew->pHTable == NULL )
Description [] Gia_ManHashStart( pNew );
Gia_ManConst0(pTwo)->Value = 0;
SideEffects [] Gia_ManForEachObj1( pTwo, pObj, i )
{
SeeAlso [] if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
***********************************************************************/ else if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) );
else if ( Gia_ObjIsCo(pObj) )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
}
Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
{ {
Gia_Man_t * pNew; Gia_Man_t * pNew;
...@@ -2185,6 +2190,58 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) ...@@ -2185,6 +2190,58 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis )
} }
/**Function*************************************************************
Synopsis [Generates AIG representing 1-hot condition for N inputs.]
Description [The condition is true of all POs are 0.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManOneHot( int nSkips, int nVars )
{
Gia_Man_t * p;
int i, b, Shift, iGiaLit, nLogVars = Abc_Base2Log( nVars );
int * pTemp = ABC_CALLOC( int, (1 << nLogVars) );
p = Gia_ManStart( nSkips + 4 * nVars + 1 );
p->pName = Abc_UtilStrsav( "onehot" );
for ( i = 0; i < nSkips; i++ )
Gia_ManAppendCi( p );
for ( i = 0; i < nVars; i++ )
pTemp[i] = Gia_ManAppendCi( p );
Gia_ManHashStart( p );
for ( b = 0; b < nLogVars; b++ )
for ( i = 0, Shift = (1<<b); i < (1 << nLogVars); i += 2*Shift )
{
iGiaLit = Gia_ManHashAnd( p, pTemp[i], pTemp[i + Shift] );
if ( iGiaLit )
Gia_ManAppendCo( p, iGiaLit );
pTemp[i] = Gia_ManHashOr( p, pTemp[i], pTemp[i + Shift] );
}
Gia_ManHashStop( p );
Gia_ManAppendCo( p, Abc_LitNot(pTemp[0]) );
ABC_FREE( pTemp );
assert( Gia_ManObjNum(p) <= nSkips + 4 * nVars + 1 );
return p;
}
Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p )
{
Gia_Man_t * pOneHot, * pNew = Gia_ManDup( p );
if ( Gia_ManRegNum(pNew) == 0 )
{
Abc_Print( 0, "Appending 1-hotness constraints to the PIs.\n" );
pOneHot = Gia_ManOneHot( 0, Gia_ManCiNum(pNew) );
}
else
pOneHot = Gia_ManOneHot( Gia_ManPiNum(pNew), Gia_ManRegNum(pNew) );
Gia_ManDupAppendShare( pNew, pOneHot );
pNew->nConstrs += Gia_ManPoNum(pOneHot);
Gia_ManStop( pOneHot );
return pNew;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/aig/gia/giaHash.c
...@@ -625,6 +625,37 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) ...@@ -625,6 +625,37 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
} }
/**Function*************************************************************
Synopsis [Creates well-balanced AND gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits )
{
if ( Vec_IntSize(vLits) == 0 )
return 0;
while ( Vec_IntSize(vLits) > 1 )
{
int i, k = 0, Lit1, Lit2, LitRes;
Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i )
{
LitRes = Gia_ManHashAnd( p, Lit1, Lit2 );
Vec_IntWriteEntry( vLits, k++, LitRes );
}
if ( Vec_IntSize(vLits) & 1 )
Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) );
Vec_IntShrink( vLits, k );
}
assert( Vec_IntSize(vLits) == 1 );
return Vec_IntEntry(vLits, 0);
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaMan.c
...@@ -77,6 +77,10 @@ void Gia_ManStop( Gia_Man_t * p ) ...@@ -77,6 +77,10 @@ void Gia_ManStop( Gia_Man_t * p )
assert( p->pManTime == NULL ); assert( p->pManTime == NULL );
Vec_PtrFreeFree( p->vNamesIn ); Vec_PtrFreeFree( p->vNamesIn );
Vec_PtrFreeFree( p->vNamesOut ); Vec_PtrFreeFree( p->vNamesOut );
Vec_IntFreeP( &p->vClassNew );
Vec_IntFreeP( &p->vClassOld );
Vec_WrdFreeP( &p->vSims );
Vec_WrdFreeP( &p->vSimsPi );
Vec_FltFreeP( &p->vTiming ); Vec_FltFreeP( &p->vTiming );
Vec_VecFreeP( &p->vClockDoms ); Vec_VecFreeP( &p->vClockDoms );
Vec_IntFreeP( &p->vLutConfigs ); Vec_IntFreeP( &p->vLutConfigs );
......
src/aig/gia/giaSweeper.c
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
#include "gia.h" #include "gia.h"
#include "base/main/main.h" #include "base/main/main.h"
#include "sat/bsat/satSolver.h" #include "sat/bsat/satSolver.h"
#include "proof/ssc/ssc.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -965,62 +966,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * ...@@ -965,62 +966,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperGen64Patterns( Gia_Man_t * pGiaCond, Vec_Wrd_t * vSim )
{
Vec_Int_t * vCex;
int i, k;
for ( i = 0; i < 64; i++ )
{
if ( Gia_SweeperCondCheckUnsat( pGiaCond ) != 0 )
return 0;
vCex = Gia_SweeperGetCex( pGiaCond );
for ( k = 0; k < Gia_ManPiNum(pGiaCond); k++ )
{
if ( Vec_IntEntry(vCex, k) )
Abc_InfoXorBit( (unsigned *)Vec_WrdEntryP(vSim, i), k );
printf( "%d", Vec_IntEntry(vCex, k) );
}
printf( "\n" );
}
return 1;
}
int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim )
{
Gia_Obj_t * pObj;
word Sim, Sim0, Sim1;
int i, Count = 0;
assert( Vec_WrdEntry(vSim, 0) == 0 );
// assert( Vec_WrdEntry(vSim, 1) != 0 ); // may not hold
Gia_ManForEachAnd( p, pObj, i )
{
Sim0 = Vec_WrdEntry( vSim, Gia_ObjFaninId0p( p, pObj ) );
Sim1 = Vec_WrdEntry( vSim, Gia_ObjFaninId1p( p, pObj ) );
Sim = (Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0) & (Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1);
Vec_WrdWriteEntry( vSim, i, Sim );
if ( pObj->fMark0 == 1 ) // considered
continue;
if ( pObj->fMark1 == 1 ) // non-constant
continue;
if ( (pObj->fPhase ? ~Sim : Sim) != 0 )
{
pObj->fMark1 = 1;
Count++;
}
}
return Count;
}
/**Function*************************************************************
Synopsis [Performs conditional sweeping of the cone.] Synopsis [Performs conditional sweeping of the cone.]
Description [Returns the result as a new GIA manager with as many inputs Description [Returns the result as a new GIA manager with as many inputs
...@@ -1031,16 +976,15 @@ int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) ...@@ -1031,16 +976,15 @@ int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_SweeperSweepInt( Gia_Man_t * pGiaCond, Gia_Man_t * pGiaOuts, Vec_Wrd_t * vSim ) Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerbose )
{
}
Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts )
{ {
Gia_Man_t * pGiaCond, * pGiaOuts;
Vec_Int_t * vProbeConds; Vec_Int_t * vProbeConds;
Vec_Wrd_t * vSim; Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes;
Gia_Obj_t * pObj; Ssc_Pars_t Pars, * pPars = &Pars;
int i, Count; Ssc_ManSetDefaultParams( pPars );
pPars->nWords = nWords;
pPars->nBTLimit = nConfs;
pPars->fVerbose = fVerbose;
// sweeper is running // sweeper is running
assert( Gia_SweeperIsRunning(p) ); assert( Gia_SweeperIsRunning(p) );
// extract conditions and logic cones // extract conditions and logic cones
...@@ -1048,22 +992,11 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) ...@@ -1048,22 +992,11 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts )
pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
Gia_ManSetPhase( pGiaOuts ); Gia_ManSetPhase( pGiaOuts );
// start the sweeper for the conditions // perform sweeping under constraints
Gia_SweeperStart( pGiaCond ); pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars );
Gia_ManForEachPo( pGiaCond, pObj, i ) Gia_ManStop( pGiaCond );
Gia_SweeperCondPush( pGiaCond, Gia_SweeperProbeCreate(pGiaCond, Gia_ObjFaninLit0p(pGiaCond, pObj)) );
// generate 64 patterns that satisfy the conditions
vSim = Vec_WrdStart( Gia_ManObjNum(pGiaOuts) );
Gia_SweeperGen64Patterns( pGiaCond, vSim );
Count = Gia_SweeperSimulate( pGiaOuts, vSim );
printf( "Disproved %d nodes.\n", Count );
// consider the remaining ones
// Gia_SweeperSweepInt( pGiaCond, pGiaOuts, vSim );
Vec_WrdFree( vSim );
Gia_ManStop( pGiaOuts ); Gia_ManStop( pGiaOuts );
Gia_SweeperStop( pGiaCond ); return pGiaRes;
return pGiaCond;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1085,14 +1018,14 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) ...@@ -1085,14 +1018,14 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ) Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose )
{ {
Gia_Man_t * pNew; Gia_Man_t * pNew;
Vec_Int_t * vLits; Vec_Int_t * vLits;
// sweeper is running // sweeper is running
assert( Gia_SweeperIsRunning(p) ); assert( Gia_SweeperIsRunning(p) );
// sweep the logic // sweep the logic
pNew = Gia_SweeperSweep( p, vProbeIds ); pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerbose );
// execute command line // execute command line
if ( pCommLime ) if ( pCommLime )
{ {
...@@ -1110,37 +1043,6 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm ...@@ -1110,37 +1043,6 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits )
{
if ( Vec_IntSize(vLits) == 0 )
return 0;
while ( Vec_IntSize(vLits) > 1 )
{
int i, k = 0, Lit1, Lit2, LitRes;
Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i )
{
LitRes = Gia_ManHashAnd( p, Lit1, Lit2 );
Vec_IntWriteEntry( vLits, k++, LitRes );
}
if ( Vec_IntSize(vLits) & 1 )
Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) );
Vec_IntShrink( vLits, k );
}
assert( Vec_IntSize(vLits) == 1 );
return Vec_IntEntry(vLits, 0);
}
/**Function*************************************************************
Synopsis [Sweeper sweeper test.] Synopsis [Sweeper sweeper test.]
Description [] Description []
...@@ -1150,43 +1052,30 @@ int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) ...@@ -1150,43 +1052,30 @@ int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ) Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose )
{ {
Gia_Man_t * pGia; Gia_Man_t * p, * pGia;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Vec_Int_t * vLits, * vOuts; Vec_Int_t * vOuts;
int i, k, Lit; int i;
// add one-hotness constraints
p = Gia_ManDupOneHot( pInit );
// create sweeper // create sweeper
Gia_SweeperStart( p ); Gia_SweeperStart( p );
// collect outputs and create conditions
// create 1-hot constraint
vLits = Vec_IntAlloc( 1000 );
for ( i = 0; i < Gia_ManPiNum(p); i++ )
for ( k = i+1; k < Gia_ManPiNum(p); k++ )
{
int Lit0 = Gia_Obj2Lit(p, Gia_ManPi(p, i));
int Lit1 = Gia_Obj2Lit(p, Gia_ManPi(p, k));
Vec_IntPush( vLits, Abc_LitNot(Gia_ManHashAnd(p, Lit0, Lit1)) );
}
Lit = 0;
for ( i = 0; i < Gia_ManPiNum(p); i++ )
Lit = Gia_ManHashOr( p, Lit, Gia_Obj2Lit(p, Gia_ManPi(p, i)) );
Vec_IntPush( vLits, Lit );
Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ManCreateAndGate( p, vLits ) ) );
Vec_IntFree( vLits );
//Gia_ManPrint( p );
// create outputs
vOuts = Vec_IntAlloc( Gia_ManPoNum(p) ); vOuts = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i ) Gia_ManForEachPo( p, pObj, i )
Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); if ( i < Gia_ManPoNum(p) - p->nConstrs ) // this is the user's output
Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
else // this is a constraint
Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
// perform the sweeping // perform the sweeping
pGia = Gia_SweeperSweep( p, vOuts ); pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose );
// pGia = Gia_ManDup( p );
Vec_IntFree( vOuts ); Vec_IntFree( vOuts );
// sop the sweeper
Gia_SweeperStop( p ); Gia_SweeperStop( p );
Gia_ManStop( p );
return pGia; return pGia;
} }
......
src/aig/gia/giaUtil.c
...@@ -1163,10 +1163,15 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig ) ...@@ -1163,10 +1163,15 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig )
if ( Gia_ManConstrNum(pAig) == 0 ) if ( Gia_ManConstrNum(pAig) == 0 )
return; return;
Gia_ManForEachPo( pAig, pObj, i ) Gia_ManForEachPo( pAig, pObj, i )
{
if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) ) if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
Gia_ObjFlipFaninC0( pObj ); Gia_ObjFlipFaninC0( pObj );
} }
void Gia_ManInvertPos( Gia_Man_t * pAig )
{
Gia_Obj_t * pObj;
int i;
Gia_ManForEachPo( pAig, pObj, i )
Gia_ObjFlipFaninC0( pObj );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/base/abci/abc.c
...@@ -51,6 +51,7 @@ ...@@ -51,6 +51,7 @@
#include "base/cmd/cmd.h" #include "base/cmd/cmd.h"
#include "proof/abs/abs.h" #include "proof/abs/abs.h"
#include "sat/bmc/bmc.h" #include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h"
#ifndef _WIN32 #ifndef _WIN32
#include <unistd.h> #include <unistd.h>
...@@ -321,6 +322,7 @@ static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, cha ...@@ -321,6 +322,7 @@ static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Add1Hot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -817,6 +819,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -817,6 +819,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&show", Abc_CommandAbc9Show, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&show", Abc_CommandAbc9Show, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Hash, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Hash, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&add1hot", Abc_CommandAbc9Add1Hot, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 );
...@@ -24543,6 +24546,52 @@ usage: ...@@ -24543,6 +24546,52 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Add1Hot( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Add1Hot(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManDupOneHot( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &add1hot [-vh]\n" );
Abc_Print( -2, "\t adds 1-hotness constraints as additional primary outputs\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
...@@ -27081,12 +27130,10 @@ usage: ...@@ -27081,12 +27130,10 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
int c; int c;
int nWords = 1; Ssc_Pars_t Pars, * pPars = &Pars;
int nConfs = 0; Ssc_ManSetDefaultParams( pPars );
int fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF )
{ {
...@@ -27098,9 +27145,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27098,9 +27145,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nWords = atoi(argv[globalUtilOptind]); pPars->nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nWords < 0 ) if ( pPars->nWords < 0 )
goto usage; goto usage;
break; break;
case 'C': case 'C':
...@@ -27109,13 +27156,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27109,13 +27156,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nConfs = atoi(argv[globalUtilOptind]); pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nConfs < 0 ) if ( pPars->nBTLimit < 0 )
goto usage; goto usage;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
default: default:
goto usage; goto usage;
...@@ -27126,16 +27173,17 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27126,16 +27173,17 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" );
return 1; return 1;
} }
pTemp = Gia_SweeperFraigTest( pAbc->pGia, nWords, nConfs, fVerbose ); Abc_Print( 0, "Current AIG contains %d constraints.\n", pAbc->pGia->nConstrs );
pTemp = Ssc_PerformSweepingConstr( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp ); Abc_FrameUpdateGia( pAbc, pTemp );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" );
Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" ); Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", nWords ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfs ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -31438,7 +31486,7 @@ usage: ...@@ -31438,7 +31486,7 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
// Gia_Man_t * pTemp = NULL; Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0; int c, fVerbose = 0;
int fSwitch = 0; int fSwitch = 0;
// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
...@@ -31451,6 +31499,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31451,6 +31499,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Unr_ManTest( Gia_Man_t * pGia ); // extern void Unr_ManTest( Gia_Man_t * pGia );
// extern void Mig_ManTest( Gia_Man_t * pGia ); // extern void Mig_ManTest( Gia_Man_t * pGia );
// extern int Gia_ManVerify( Gia_Man_t * pGia ); // extern int Gia_ManVerify( Gia_Man_t * pGia );
extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
...@@ -31502,6 +31551,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31502,6 +31551,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Unr_ManTest( pAbc->pGia ); // Unr_ManTest( pAbc->pGia );
// Mig_ManTest( pAbc->pGia ); // Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia ); // Gia_ManVerifyWithBoxes( pAbc->pGia );
pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &test [-svh]\n" ); Abc_Print( -2, "usage: &test [-svh]\n" );
......
src/proof/ssc/module.make 0 → 100644
SRC += src/proof/ssc/sscClass.c \
src/proof/ssc/sscCore.c \
src/proof/ssc/sscSat.c \
src/proof/ssc/sscSim.c \
src/proof/ssc/sscUtil.c
src/proof/ssc/ssc.h 0 → 100644
/**CFile****************************************************************
FileName [ssc.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__ssc__ssc_h
#define ABC__aig__ssc__ssc_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// choicing parameters
typedef struct Ssc_Pars_t_ Ssc_Pars_t;
struct Ssc_Pars_t_
{
int nWords; // the number of simulation words
int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver
int fVerbose; // verbose stats
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sscCore.c ==========================================================*/
extern void Ssc_ManSetDefaultParams( Ssc_Pars_t * p );
extern Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars );
extern Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/proof/ssc/sscClass.c 0 → 100644
/**CFile****************************************************************
FileName [sscClass.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [Equivalence classes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes hash key of the simuation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Ssc_GiaSimHashKey( Gia_Man_t * p, int iObj, int nTableSize )
{
static int s_Primes[16] = {
1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
word * pSim = Gia_ObjSim( p, iObj );
unsigned uHash = 0;
int i, nWords = Gia_ObjSimWords(p);
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 [Returns 1 if sim patterns are equal up to the complement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Ssc_GiaSimIsConst0( Gia_Man_t * p, int iObj0 )
{
int w, nWords = Gia_ObjSimWords(p);
word * pSim = Gia_ObjSim( p, iObj0 );
if ( pSim[0] & 1 )
{
for ( w = 0; w < nWords; w++ )
if ( ~pSim[w] )
return 0;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( pSim[w] )
return 0;
}
return 1;
}
static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
{
int w, nWords = Gia_ObjSimWords(p);
word * pSim0 = Gia_ObjSim( p, iObj0 );
word * pSim1 = Gia_ObjSim( p, iObj1 );
if ( (pSim0[0] & 1) != (pSim1[0] & 1) )
{
for ( w = 0; w < nWords; w++ )
if ( pSim0[w] != ~pSim1[w] )
return 0;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( pSim0[w] != pSim1[w] )
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Refines one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
{
int Repr = GIA_VOID, EntPrev = -1, Ent, i;
assert( Vec_IntSize(vClass) > 0 );
Vec_IntForEachEntry( vClass, Ent, i )
{
if ( i == 0 )
{
Repr = Ent;
Gia_ObjSetRepr( p, Ent, GIA_VOID );
EntPrev = Ent;
}
else
{
assert( Repr < Ent );
Gia_ObjSetRepr( p, Ent, Repr );
Gia_ObjSetNext( p, EntPrev, Ent );
EntPrev = Ent;
}
}
Gia_ObjSetNext( p, EntPrev, 0 );
}
int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
{
Gia_Obj_t * pObj;
int Ent;
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
pObj = Gia_ManObj(p, i);
Gia_ClassForEachObj1( p, i, Ent )
{
if ( Ssc_GiaSimAreEqual( p, i, Ent ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
Ssc_GiaSimClassCreate( p, p->vClassOld );
Ssc_GiaSimClassCreate( p, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
{
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
assert( !Ssc_GiaSimIsConst0( p, i ) );
Key = Ssc_GiaSimHashKey( p, i, nTableSize );
if ( pTable[Key] == 0 )
{
assert( Gia_ObjRepr(p, i) == 0 );
assert( Gia_ObjNext(p, i) == 0 );
Gia_ObjSetRepr( p, i, GIA_VOID );
}
else
{
Gia_ObjSetNext( p, pTable[Key], i );
Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) );
if ( Gia_ObjRepr(p, i) == GIA_VOID )
Gia_ObjSetRepr( p, i, pTable[Key] );
assert( Gia_ObjRepr(p, i) > 0 );
}
pTable[Key] = i;
}
Vec_IntForEachEntry( vRefined, i, k )
if ( Gia_ObjIsHead( p, i ) )
Ssc_GiaSimClassRefineOne( p, i );
ABC_FREE( pTable );
}
/**Function*************************************************************
Synopsis [Refines equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaClassesRefine( Gia_Man_t * p )
{
Vec_Int_t * vRefinedC;
Gia_Obj_t * pObj;
int i;
if ( p->pReprs == NULL )
{
assert( p->pReprs == NULL );
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachObj( p, pObj, i )
Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
if ( p->vClassOld == NULL )
p->vClassOld = Vec_IntAlloc( 100 );
if ( p->vClassNew == NULL )
p->vClassNew = Vec_IntAlloc( 100 );
}
vRefinedC = Vec_IntAlloc( 100 );
Gia_ManForEachCand( p, pObj, i )
if ( Gia_ObjIsTail(p, i) )
Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
Vec_IntPush( vRefinedC, i );
Ssc_GiaSimProcessRefined( p, vRefinedC );
Vec_IntFree( vRefinedC );
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/ssc/sscCore.c 0 → 100644
/**CFile****************************************************************
FileName [sscCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [The core procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
{
memset( p, 0, sizeof(Ssc_Pars_t) );
p->nWords = 4; // the number of simulation words
p->nBTLimit = 1000; // conflict limit at a node
p->nSatVarMax = 5000; // the max number of SAT variables
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
p->fVerbose = 0; // verbose stats
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_ManStop( Ssc_Man_t * p )
{
if ( p->pSat )
sat_solver_delete( p->pSat );
Vec_IntFreeP( &p->vSatVars );
Gia_ManStopP( &p->pFraig );
Vec_IntFreeP( &p->vPivot );
ABC_FREE( p );
}
Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
{
Ssc_Man_t * p;
p = ABC_CALLOC( Ssc_Man_t, 1 );
p->pPars = pPars;
p->pAig = pAig;
p->pCare = pCare;
p->pFraig = Gia_ManDup( p->pCare );
Gia_ManInvertPos( p->pFraig );
Ssc_ManStartSolver( p );
if ( p->pSat == NULL )
{
printf( "Constraints are UNSAT after propagation.\n" );
Ssc_ManStop( p );
return NULL;
}
p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
// Vec_IntFreeP( &p->vPivot );
if ( p->vPivot == NULL )
p->vPivot = Ssc_ManFindPivotSat( p );
if ( p->vPivot == NULL )
{
printf( "Constraints are UNSAT or conflict limit is too low.\n" );
Ssc_ManStop( p );
return NULL;
}
Vec_IntPrint( p->vPivot );
return p;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description [Takes several AIGs and performs choicing.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
{
Ssc_Man_t * p;
Gia_Man_t * pResult;
clock_t clk, clkTotal = clock();
int i;
assert( Gia_ManRegNum(pCare) == 0 );
assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) );
assert( Gia_ManIsNormalized(pAig) );
assert( Gia_ManIsNormalized(pCare) );
// reset random numbers
Gia_ManRandom( 1 );
// sweeping manager
p = Ssc_ManStart( pAig, pCare, pPars );
if ( p == NULL )
return Gia_ManDup( pAig );
// perform simulation
clk = clock();
for ( i = 0; i < 16; i++ )
{
Ssc_GiaRandomPiPattern( pAig, 10, NULL );
Ssc_GiaSimRound( pAig );
Ssc_GiaClassesRefine( pAig );
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
p->timeSimInit += clock() - clk;
// remember the resulting AIG
pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
if ( pResult == NULL )
{
printf( "There is no equivalences.\n" );
pResult = Gia_ManDup( pAig );
}
Ssc_ManStop( p );
// count the number of representatives
if ( pPars->fVerbose )
{
Gia_ManEquivPrintClasses( pAig, 0, 0 );
Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d. ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
return pResult;
}
Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
{
Gia_Man_t * pAig, * pCare, * pResult;
int i;
if ( p->nConstrs == 0 )
{
pAig = Gia_ManDup( p );
pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 );
pCare->pName = Abc_UtilStrsav( "care" );
for ( i = 0; i < Gia_ManPiNum(p); i++ )
Gia_ManAppendCi( pCare );
Gia_ManAppendCo( pCare, 1 );
}
else
{
Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
Vec_IntFree( vOuts );
}
pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
Gia_ManStop( pAig );
Gia_ManStop( pCare );
return pResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/ssc/sscInt.h 0 → 100644
/**CFile****************************************************************
FileName [sscInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Choice computation for tech-mapping.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__ssc__sscInt_h
#define ABC__aig__ssc__sscInt_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/gia/gia.h"
#include "sat/bsat/satSolver.h"
#include "ssc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// choicing manager
typedef struct Ssc_Man_t_ Ssc_Man_t;
struct Ssc_Man_t_
{
// parameters
Ssc_Pars_t * pPars; // choicing parameters
Gia_Man_t * pAig; // subject AIG
Gia_Man_t * pCare; // care set AIG
Gia_Man_t * pFraig; // resulting AIG
Vec_Int_t * vPivot; // one SAT pattern
// SAT solving
sat_solver * pSat; // recyclable SAT solver
Vec_Int_t * vSatVars; // mapping of each node into its SAT var
Vec_Int_t * vUsedNodes; // nodes whose SAT vars are assigned
int nRecycles; // the number of times SAT solver was recycled
int nCallsSince; // the number of calls since the last recycle
Vec_Int_t * vFanins; // fanins of the CNF node
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
int nSatFailsReal; // the number of timeouts
int nSatCallsUnsat; // the number of unsat SAT calls
int nSatCallsSat; // the number of sat SAT calls
// runtime stats
clock_t timeSimInit; // simulation and class computation
clock_t timeSimSat; // simulation of the counter-examples
clock_t timeSat; // solving SAT
clock_t timeSatSat; // sat
clock_t timeSatUnsat; // unsat
clock_t timeSatUndec; // undecided
clock_t timeChoice; // choice computation
clock_t timeOther; // other runtime
clock_t timeTotal; // total runtime
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Ssc_ObjSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj)); }
static inline void Ssc_ObjSetSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj, int Num ) { Vec_IntWriteEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj), Num); }
static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; }
static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sscClass.c =================================================*/
extern int Ssc_GiaClassesRefine( Gia_Man_t * p );
/*=== sscCnf.c ===================================================*/
extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
/*=== sscCore.c ==================================================*/
/*=== sscSat.c ===================================================*/
extern int Ssc_NodesAreEquiv( Ssc_Man_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Ssc_ManSatSolverRecycle( Ssc_Man_t * p );
extern void Ssc_ManStartSolver( Ssc_Man_t * p );
extern Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p );
/*=== sscSim.c ===================================================*/
extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
extern void Ssc_GiaSimRound( Gia_Man_t * p );
extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p );
/*=== sscUtil.c ===================================================*/
extern Gia_Man_t * Ssc_GenerateOneHot( int nVars );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/proof/ssc/sscSat.c 0 → 100644
/**CFile****************************************************************
FileName [sscSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [SAT procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
#include "sat/cnf/cnf.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the SAT solver for constraints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_ManStartSolver( Ssc_Man_t * p )
{
Aig_Man_t * pAig = Gia_ManToAig( p->pFraig, 0 );
Cnf_Dat_t * pDat = Cnf_Derive( pAig, 0 );
sat_solver * pSat;
int i, status;
assert( p->pSat == NULL && p->vSatVars == NULL );
assert( Aig_ManObjNumMax(pAig) == Gia_ManObjNum(p->pFraig) );
Aig_ManStop( pAig );
//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
// save variable mapping
p->vSatVars = Vec_IntAllocArray( pDat->pVarNums, Gia_ManObjNum(p->pFraig) ); pDat->pVarNums = NULL;
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pDat->nVars + 1000 );
for ( i = 0; i < pDat->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
{
Cnf_DataFree( pDat );
sat_solver_delete( pSat );
return;
}
}
Cnf_DataFree( pDat );
status = sat_solver_simplify( pSat );
if ( status == 0 )
{
sat_solver_delete( pSat );
return;
}
p->pSat = pSat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
{
Vec_Int_t * vInit;
Gia_Obj_t * pObj;
int i, status;
status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
if ( status != l_True ) // unsat or undec
return NULL;
vInit = Vec_IntAlloc( Gia_ManPiNum(p->pFraig) );
Gia_ManForEachPi( p->pFraig, pObj, i )
Vec_IntPush( vInit, sat_solver_var_value(p->pSat, Ssc_ObjSatNum(p, pObj)) );
return vInit;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/ssc/sscSim.c 0 → 100644
/**CFile****************************************************************
FileName [sscSim.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [Simulation procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline word Ssc_Random() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 0); }
static inline word Ssc_Random1( int Bit ) { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 1) | (word)Bit; }
static inline word Ssc_Random2() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 2) | (word)2; }
static inline void Ssc_SimAnd( word * pSim, word * pSim0, word * pSim1, int nWords, int fComp0, int fComp1 )
{
int w;
if ( fComp0 && fComp1 )
for ( w = 0; w < nWords; w++ )
pSim[w] = ~(pSim0[w] | pSim1[w]);
else if ( fComp0 )
for ( w = 0; w < nWords; w++ )
pSim[w] = ~pSim0[w] & pSim1[w];
else if ( fComp1 )
for ( w = 0; w < nWords; w++ )
pSim[w] = pSim0[w] & ~pSim1[w];
else
for ( w = 0; w < nWords; w++ )
pSim[w] = pSim0[w] & pSim1[w];
}
static inline void Ssc_SimDup( word * pSim, word * pSim0, int nWords, int fComp0 )
{
int w;
if ( fComp0 )
for ( w = 0; w < nWords; w++ )
pSim[w] = ~pSim0[w];
else
for ( w = 0; w < nWords; w++ )
pSim[w] = pSim0[w];
}
static inline void Ssc_SimConst( word * pSim, int nWords, int fComp0 )
{
int w;
if ( fComp0 )
for ( w = 0; w < nWords; w++ )
pSim[w] = ~(word)0;
else
for ( w = 0; w < nWords; w++ )
pSim[w] = 0;
}
static inline void Ssc_SimOr( word * pSim, word * pSim0, int nWords, int fComp0 )
{
int w;
if ( fComp0 )
for ( w = 0; w < nWords; w++ )
pSim[w] |= ~pSim0[w];
else
for ( w = 0; w < nWords; w++ )
pSim[w] |= pSim0[w];
}
static inline int Ssc_SimFindBitWord( word t )
{
int n = 0;
if ( t == 0 ) return -1;
if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; }
if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; }
if ( (t & 0x00000000000000FF) == 0 ) { n += 8; t >>= 8; }
if ( (t & 0x000000000000000F) == 0 ) { n += 4; t >>= 4; }
if ( (t & 0x0000000000000003) == 0 ) { n += 2; t >>= 2; }
if ( (t & 0x0000000000000001) == 0 ) { n++; }
return n;
}
static inline int Ssc_SimFindBit( word * pSim, int nWords )
{
int w;
for ( w = 0; w < nWords; w++ )
if ( pSim[w] )
return 64*w + Ssc_SimFindBitWord(pSim[w]);
return -1;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vec_WrdDoubleSimInfo( Vec_Wrd_t * p, int nObjs )
{
word * pArray = ABC_CALLOC( word, 2 * Vec_WrdSize(p) );
int i, nWords = Vec_WrdSize(p) / nObjs;
assert( Vec_WrdSize(p) % nObjs == 0 );
for ( i = 0; i < nObjs; i++ )
memcpy( pArray + 2*i*nWords, p->pArray + i*nWords, sizeof(word) * nWords );
ABC_FREE( p->pArray ); p->pArray = pArray;
p->nSize = p->nCap = 2*nWords*nObjs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords )
{
p->iPatsPi = 0;
if ( p->vSimsPi == NULL )
p->vSimsPi = Vec_WrdStart(0);
Vec_WrdFill( p->vSimsPi, nWords * Gia_ManPiNum(p), 0 );
assert( nWords == Gia_ObjSimWords( p ) );
}
void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
{
word * pSimPi;
int i, w;
Ssc_GiaResetPiPattern( p, nWords );
pSimPi = Gia_ObjSimPi( p, 0 );
for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += nWords )
{
pSimPi[0] = vPivot ? Ssc_Random1(Vec_IntEntry(vPivot, i)) : Ssc_Random2();
for ( w = 1; w < nWords; w++ )
pSimPi[w] = Ssc_Random();
// if ( i < 10 )
// Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
}
}
void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
{
word * pSimPi;
int i;
assert( Vec_IntSize(vPat) == Gia_ManPiNum(p) );
if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManPiNum(p) );
assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
pSimPi = Gia_ObjSimPi( p, 0 );
for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
if ( Vec_IntEntry(vPat, i) )
Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
p->iPatsPi++;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaResetSimInfo( Gia_Man_t * p )
{
assert( Vec_WrdSize(p->vSimsPi) % Gia_ManPiNum(p) == 0 );
if ( p->vSims == NULL )
p->vSims = Vec_WrdAlloc(0);
Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 );
}
void Ssc_GiaSimRound( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
word * pSim, * pSim0, * pSim1;
int i, nWords = Gia_ObjSimWords(p);
Ssc_GiaResetSimInfo( p );
assert( nWords == Vec_WrdSize(p->vSims) / Gia_ManObjNum(p) );
// constant node
Ssc_SimConst( Gia_ObjSim(p, 0), nWords, 0 );
// primary inputs
pSim = Gia_ObjSim( p, 1 );
pSim0 = Gia_ObjSimPi( p, 0 );
Gia_ManForEachPi( p, pObj, i )
{
assert( pSim == Gia_ObjSimObj( p, pObj ) );
Ssc_SimDup( pSim, pSim0, nWords, 0 );
pSim += nWords;
pSim0 += nWords;
}
// intermediate nodes
pSim = Gia_ObjSim( p, 1+Gia_ManPiNum(p) );
Gia_ManForEachAnd( p, pObj, i )
{
assert( pSim == Gia_ObjSim( p, i ) );
pSim0 = pSim - pObj->iDiff0 * nWords;
pSim1 = pSim - pObj->iDiff1 * nWords;
Ssc_SimAnd( pSim, pSim0, pSim1, nWords, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
pSim += nWords;
}
// primary outputs
pSim = Gia_ObjSim( p, Gia_ManObjNum(p) - Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
{
assert( pSim == Gia_ObjSimObj( p, pObj ) );
pSim0 = pSim - pObj->iDiff0 * nWords;
Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) );
pSim += nWords;
}
}
/**Function*************************************************************
Synopsis [Returns one SAT assignment of the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
{
Vec_Int_t * vInit;
Gia_Obj_t * pObj;
int i, iBit, nWords = Gia_ObjSimWords( p );
word * pRes = ABC_FALLOC( word, nWords );
Gia_ManForEachPo( p, pObj, i )
Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
iBit = Ssc_SimFindBit( pRes, nWords );
ABC_FREE( pRes );
if ( iBit == -1 )
return NULL;
vInit = Vec_IntAlloc( 100 );
Gia_ManForEachPi( p, pObj, i )
Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
return vInit;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
{
Vec_Int_t * vInit;
Ssc_GiaRandomPiPattern( p, 1, NULL );
Ssc_GiaSimRound( p );
vInit = Ssc_GiaGetOneSim( p );
return vInit;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/ssc/sscUtil.c 0 → 100644
/**CFile****************************************************************
FileName [sscUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [Various utilities.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscUtil.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Hsh_Obj_t_ Hsh_Obj_t;
struct Hsh_Obj_t_
{
int iThis;
int iNext;
};
typedef struct Hsh_Man_t_ Hsh_Man_t;
struct Hsh_Man_t_
{
unsigned * pData; // user's data
int * pTable; // hash table
Hsh_Obj_t * pObjs;
int nObjs;
int nSize;
int nTableSize;
};
static inline int * Hsh_ObjData( Hsh_Man_t * p, int iThis ) { return p->pData + p->nSize * iThis; }
static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return iObj == -1 ? NULL : p->pObjs + iObj; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize )
{
Hsh_Man_t * p;
p = ABC_CALLOC( Hsh_Man_t, 1 );
p->pData = pData;
p->nSize = nSize;
p->nTableSize = Abc_PrimeCudd( nDatas );
p->pTable = ABC_FALLOC( int, p->nTableSize );
p->pObjs = ABC_FALLOC( Hsh_Obj_t, p->nTableSize );
return p;
}
void Hsh_ManStop( Hsh_Man_t * p )
{
ABC_FREE( p->pObjs );
ABC_FREE( p->pTable );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize )
{
static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
unsigned char * pDataC = (unsigned char *)pData;
int c, nChars = nSize * 4, Key = 0;
for ( c = 0; c < nChars; c++ )
Key += pDataC[c] * s_BigPrimes[c % 7];
return Key % nTableSize;
}
int Hsh_ManAdd( Hsh_Man_t * p, int iThis )
{
Hsh_Obj_t * pObj;
int * pThis = Hsh_ObjData( p, iThis );
int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize );
for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) )
if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(int) * p->nSize ) )
return pObj - p->pObjs;
assert( p->nObjs < p->nTableSize );
pObj = p->pObjs + p->nObjs;
pObj->iThis = iThis;
return (*pPlace = p->nObjs++);
}
/**Function*************************************************************
Synopsis [Hashes data by value.]
Description [Array of 'nTotal' int entries, each of size 'nSize' ints,
is hashed and the resulting unique numbers is returned in the array.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Hsh_ManHashData( int * pData, int nDatas, int nSize, int nInts )
{
Vec_Int_t * vRes;
Hsh_Man_t * p;
int i;
assert( nDatas * nSize == nInts );
p = Hsh_ManStart( pData, nDatas, nSize );
vRes = Vec_IntAlloc( 1000 );
for ( i = 0; i < nDatas; i++ )
Vec_IntPush( vRes, Hsh_ManAdd(p, i) );
Hsh_ManStop( p );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
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