summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h21
-rw-r--r--src/aig/gia/giaDup.c85
-rw-r--r--src/aig/gia/giaHash.c31
-rw-r--r--src/aig/gia/giaMan.c4
-rw-r--r--src/aig/gia/giaSweeper.c169
-rw-r--r--src/aig/gia/giaUtil.c9
-rw-r--r--src/base/abci/abc.c79
-rw-r--r--src/proof/ssc/module.make5
-rw-r--r--src/proof/ssc/ssc.h76
-rw-r--r--src/proof/ssc/sscClass.c245
-rw-r--r--src/proof/ssc/sscCore.c191
-rw-r--r--src/proof/ssc/sscInt.h122
-rw-r--r--src/proof/ssc/sscSat.c113
-rw-r--r--src/proof/ssc/sscSim.c294
-rw-r--r--src/proof/ssc/sscUtil.c152
15 files changed, 1424 insertions, 172 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 737f6a67..6dad5eb5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -167,6 +167,12 @@ struct Gia_Man_t_
int iData2; // various user data
int nAnd2Delay; // AND2 delay scaled to match delay numbers used
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
int nTtVars; // truth table variables
int nTtWords; // truth table words
@@ -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 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_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 *
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 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
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 )
@@ -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-- )
#define Gia_ManForEachAnd( p, pObj, i ) \
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 ) \
for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachCi( p, pObj, i ) \
@@ -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_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
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_ManDupSelf( Gia_Man_t * p );
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 );
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_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
+extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p );
/*=== giaEnable.c ==========================================================*/
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 );
@@ -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 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_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
/*=== giaIf.c ===========================================================*/
extern void Gia_ManPrintMappingStats( 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
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 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 ============================================================*/
extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
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 );
extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
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 void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 74867eff..78aac33c 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -577,7 +577,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
if ( pNew->nRegs > 0 )
pNew->nRegs = 0;
if ( pNew->pHTable == NULL )
- Gia_ManHashAlloc( pNew );
+ Gia_ManHashStart( pNew );
Gia_ManConst0(pTwo)->Value = 0;
Gia_ManForEachObj1( pTwo, pObj, i )
{
@@ -589,19 +589,24 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
}
-
-
-/**Function*************************************************************
-
- Synopsis [Append second AIG on top of the first with the permutation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
+void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) );
+ if ( pNew->pHTable == NULL )
+ Gia_ManHashStart( pNew );
+ Gia_ManConst0(pTwo)->Value = 0;
+ Gia_ManForEachObj1( pTwo, pObj, i )
+ {
+ 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 * pNew;
@@ -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 ///
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 4ae01f06..81980b40 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 732a5075..75a0f801 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -77,6 +77,10 @@ void Gia_ManStop( Gia_Man_t * p )
assert( p->pManTime == NULL );
Vec_PtrFreeFree( p->vNamesIn );
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_VecFreeP( &p->vClockDoms );
Vec_IntFreeP( &p->vLutConfigs );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 844c3e45..3f597982 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -21,6 +21,7 @@
#include "gia.h"
#include "base/main/main.h"
#include "sat/bsat/satSolver.h"
+#include "proof/ssc/ssc.h"
ABC_NAMESPACE_IMPL_START
@@ -965,62 +966,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
/**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.]
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 )
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 )
+Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerbose )
{
- Gia_Man_t * pGiaCond, * pGiaOuts;
Vec_Int_t * vProbeConds;
- Vec_Wrd_t * vSim;
- Gia_Obj_t * pObj;
- int i, Count;
+ Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes;
+ Ssc_Pars_t Pars, * pPars = &Pars;
+ Ssc_ManSetDefaultParams( pPars );
+ pPars->nWords = nWords;
+ pPars->nBTLimit = nConfs;
+ pPars->fVerbose = fVerbose;
// sweeper is running
assert( Gia_SweeperIsRunning(p) );
// extract conditions and logic cones
@@ -1048,22 +992,11 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts )
pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
Gia_ManSetPhase( pGiaOuts );
- // start the sweeper for the conditions
- Gia_SweeperStart( pGiaCond );
- Gia_ManForEachPo( pGiaCond, pObj, i )
- 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 );
+ // perform sweeping under constraints
+ pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars );
+ Gia_ManStop( pGiaCond );
Gia_ManStop( pGiaOuts );
- Gia_SweeperStop( pGiaCond );
- return pGiaCond;
+ return pGiaRes;
}
/**Function*************************************************************
@@ -1085,14 +1018,14 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts )
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;
Vec_Int_t * vLits;
// sweeper is running
assert( Gia_SweeperIsRunning(p) );
// sweep the logic
- pNew = Gia_SweeperSweep( p, vProbeIds );
+ pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerbose );
// execute command line
if ( pCommLime )
{
@@ -1110,37 +1043,6 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm
/**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.]
Description []
@@ -1150,43 +1052,30 @@ int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits )
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;
- Vec_Int_t * vLits, * vOuts;
- int i, k, Lit;
-
+ Vec_Int_t * vOuts;
+ int i;
+ // add one-hotness constraints
+ p = Gia_ManDupOneHot( pInit );
// create sweeper
Gia_SweeperStart( p );
-
- // 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
+ // collect outputs and create conditions
vOuts = Vec_IntAlloc( Gia_ManPoNum(p) );
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
- pGia = Gia_SweeperSweep( p, vOuts );
+ pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose );
+// pGia = Gia_ManDup( p );
Vec_IntFree( vOuts );
-
+ // sop the sweeper
Gia_SweeperStop( p );
+ Gia_ManStop( p );
return pGia;
}
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 5adf9ebd..6f4389a8 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1163,10 +1163,15 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig )
if ( Gia_ManConstrNum(pAig) == 0 )
return;
Gia_ManForEachPo( pAig, pObj, i )
- {
if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
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*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index af1c8ecf..533db448 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -51,6 +51,7 @@
#include "base/cmd/cmd.h"
#include "proof/abs/abs.h"
#include "sat/bmc/bmc.h"
+#include "proof/ssc/ssc.h"
#ifndef _WIN32
#include <unistd.h>
@@ -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_CommandAbc9Hash ( 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_CommandAbc9Trim ( 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 )
Cmd_CommandAdd( pAbc, "ABC9", "&show", Abc_CommandAbc9Show, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Hash, 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", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 );
@@ -24543,6 +24546,52 @@ usage:
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 )
{
Gia_Man_t * pTemp;
@@ -27081,12 +27130,10 @@ usage:
***********************************************************************/
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;
int c;
- int nWords = 1;
- int nConfs = 0;
- int fVerbose = 0;
+ Ssc_Pars_t Pars, * pPars = &Pars;
+ Ssc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF )
{
@@ -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" );
goto usage;
}
- nWords = atoi(argv[globalUtilOptind]);
+ pPars->nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nWords < 0 )
+ if ( pPars->nWords < 0 )
goto usage;
break;
case 'C':
@@ -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" );
goto usage;
}
- nConfs = atoi(argv[globalUtilOptind]);
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nConfs < 0 )
+ if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'v':
- fVerbose ^= 1;
+ pPars->fVerbose ^= 1;
break;
default:
goto usage;
@@ -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" );
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 );
return 0;
usage:
Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\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-C num : the max number of conflicts at a node [default = %d]\n", nConfs );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ 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", pPars->nBTLimit );
+ 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");
return 1;
}
@@ -31438,7 +31486,7 @@ usage:
***********************************************************************/
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 fSwitch = 0;
// 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 )
// extern void Unr_ManTest( Gia_Man_t * pGia );
// extern void Mig_ManTest( 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();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -31502,6 +31551,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Unr_ManTest( pAbc->pGia );
// Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia );
+ pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+ Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/proof/ssc/module.make b/src/proof/ssc/module.make
new file mode 100644
index 00000000..55e845f8
--- /dev/null
+++ b/src/proof/ssc/module.make
@@ -0,0 +1,5 @@
+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
diff --git a/src/proof/ssc/ssc.h b/src/proof/ssc/ssc.h
new file mode 100644
index 00000000..de32ffc1
--- /dev/null
+++ b/src/proof/ssc/ssc.h
@@ -0,0 +1,76 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
new file mode 100644
index 00000000..a6d2b5e3
--- /dev/null
+++ b/src/proof/ssc/sscClass.c
@@ -0,0 +1,245 @@
+/**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
+
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
new file mode 100644
index 00000000..f2cd810a
--- /dev/null
+++ b/src/proof/ssc/sscCore.c
@@ -0,0 +1,191 @@
+/**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
+
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
new file mode 100644
index 00000000..21f5afc2
--- /dev/null
+++ b/src/proof/ssc/sscInt.h
@@ -0,0 +1,122 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
new file mode 100644
index 00000000..1519b89e
--- /dev/null
+++ b/src/proof/ssc/sscSat.c
@@ -0,0 +1,113 @@
+/**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
+
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
new file mode 100644
index 00000000..86837000
--- /dev/null
+++ b/src/proof/ssc/sscSim.c
@@ -0,0 +1,294 @@
+/**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
+
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
new file mode 100644
index 00000000..a96503d0
--- /dev/null
+++ b/src/proof/ssc/sscUtil.c
@@ -0,0 +1,152 @@
+/**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
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 20:03:12 +0000