SAT sweeping under constraints.

18 files changed, 1461 insertions, 173 deletions

diff --git a/Makefile b/Makefile
index b025f8e9..4247a799 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ MODULES := \
 	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/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/miniaig \
 	src/python 
diff --git a/abcexe.dsp b/abcexe.dsp
index c8c4f8f8..bc68d593 100644
--- a/abcexe.dsp
+++ b/abcexe.dsp
@@ -89,6 +89,10 @@ LINK32=link.exe
 
 SOURCE=.\src\base\main\main.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver.c
+# End Source File
 # End Group
 # Begin Group "Header Files"
 
diff --git a/abclib.dsp b/abclib.dsp
index 16d2d3a1..f636f2eb 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4522,6 +4522,38 @@ SOURCE=.\src\proof\abs\absUtil.c
 SOURCE=.\src\proof\abs\absVta.c
 # End Source File
 # 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
 # Begin Group "Header Files"
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
+