SAT sweeping under constraints.

src/aig/gia/gia.h

@@ -874,6 +874,7 @@ 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 );
+extern Gia_Man_t *         Gia_ManDupLevelized( 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 );
@@ -1071,8 +1072,10 @@ extern void                Gia_ManCleanTruth( Gia_Man_t * p );
 extern void                Gia_ManFillValue( Gia_Man_t * p );
 extern void                Gia_ObjSetPhase( Gia_Obj_t * pObj );
 extern void                Gia_ManSetPhase( Gia_Man_t * p );
+extern void                Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues );
 extern void                Gia_ManSetPhase1( Gia_Man_t * p );
 extern void                Gia_ManCleanPhase( Gia_Man_t * p );
+extern int                 Gia_ManCheckCoPhase( Gia_Man_t * p );
 extern int                 Gia_ManLevelNum( Gia_Man_t * p );
 extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );

src/aig/gia/giaAiger.c

@@ -1044,6 +1044,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         p->vNamesOut  = pInit->vNamesOut;  pInit->vNamesOut  = NULL;
         p->pAigExtra  = pInit->pAigExtra;  pInit->pAigExtra  = NULL;
         p->nAnd2Delay = pInit->nAnd2Delay; pInit->nAnd2Delay = 0;
+        p->nConstrs   = pInit->nConstrs;   pInit->nConstrs   = 0;
     }
     else
         p = pInit;
@@ -1137,7 +1138,6 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Vec_StrFree( vStrExt );
         if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
     }
-/*
     // write constraints
     if ( p->nConstrs )
     {
@@ -1145,7 +1145,6 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Gia_FileWriteBufferSize( pFile, 4 );
         Gia_FileWriteBufferSize( pFile, p->nConstrs );
     }
-*/
     // write timing information
     if ( p->nAnd2Delay )
     {

src/aig/gia/giaDup.c

@@ -2243,6 +2243,47 @@ Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG with nodes ordered by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, nLevels = Gia_ManLevelNum( p );
+    int * pCounts = ABC_CALLOC( int, nLevels + 1 );
+    int * pNodes = ABC_ALLOC( int, Gia_ManAndNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+        pCounts[Gia_ObjLevel(p, pObj)]++;
+    for ( i = 1; i <= nLevels; i++ )
+        pCounts[i] += pCounts[i-1];
+    Gia_ManForEachAnd( p, pObj, i )
+        pNodes[pCounts[Gia_ObjLevel(p, pObj)-1]++] = i;
+    // duplicate
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    for ( i = 0; i < Gia_ManAndNum(p) && (pObj = Gia_ManObj(p, pNodes[i])); i++ )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    ABC_FREE( pCounts );
+    ABC_FREE( pNodes );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaUtil.c

@@ -366,6 +366,16 @@ void Gia_ManSetPhase( Gia_Man_t * p )
     Gia_ManForEachObj( p, pObj, i )
         Gia_ObjSetPhase( pObj );
 }
+void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues )  
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjIsCi(pObj) )
+            pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) );
+        else
+            Gia_ObjSetPhase( pObj );
+}
 
 /**Function*************************************************************
 
@@ -410,6 +420,26 @@ void Gia_ManCleanPhase( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of COs whose value is 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckCoPhase( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        Counter += pObj->fPhase;
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prepares copies for the model.]
 
   Description []

src/proof/ssc/sscClass.c

@@ -208,23 +208,26 @@ void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
   SeeAlso     []
 
 ***********************************************************************/
+void Ssc_GiaClassesInit( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    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 );
+}
 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 );
-    }
+    if ( p->pReprs != NULL );
     vRefinedC = Vec_IntAlloc( 100 );
     Gia_ManForEachCand( p, pObj, i )
         if ( Gia_ObjIsTail(p, i) )
@@ -236,6 +239,29 @@ int Ssc_GiaClassesRefine( Gia_Man_t * p )
     return 0;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the pairs have been disproved.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs )
+{
+    int i, iRepr, iObj, Result = 1;
+    Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i )
+        if ( iRepr == Gia_ObjRepr(p, iObj) )
+            printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0;
+    if ( Result )
+        printf( "Classes are refined correctly.\n" );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/proof/ssc/sscCore.c

@@ -45,13 +45,14 @@ ABC_NAMESPACE_IMPL_START
 void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
 {
     memset( p, 0, sizeof(Ssc_Pars_t) );
-    p->nWords         =     4;  // the number of simulation words
+    p->nWords         =     1;  // 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    []
@@ -65,11 +66,15 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
 ***********************************************************************/
 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->vFront );
+    Vec_IntFreeP( &p->vFanins );
+    Vec_IntFreeP( &p->vPattern );
+    Vec_IntFreeP( &p->vDisPairs );
     Vec_IntFreeP( &p->vPivot );
+    Vec_IntFreeP( &p->vId2Var );
+    Vec_IntFreeP( &p->vVar2Id );
+    if ( p->pSat ) sat_solver_delete( p->pSat );
+    Gia_ManStopP( &p->pFraig );
     ABC_FREE( p );
 }
 Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
@@ -80,33 +85,48 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     p->pAig   = pAig;
     p->pCare  = pCare;
     p->pFraig = Gia_ManDup( p->pCare );
+    Gia_ManHashStart( p->pFraig );
     Gia_ManInvertPos( p->pFraig );
     Ssc_ManStartSolver( p );
     if ( p->pSat == NULL )
     {
-        printf( "Constraints are UNSAT after propagation.\n" );
+        printf( "Constraints are UNSAT after propagation (likely a bug!).\n" );
         Ssc_ManStop( p );
         return NULL;
     }
-    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
+//    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
 //    Vec_IntFreeP( &p->vPivot  );
-    if ( p->vPivot == NULL )
-        p->vPivot = Ssc_ManFindPivotSat( p );
+    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;
     }
+    sat_solver_bookmark( p->pSat );
     Vec_IntPrint( p->vPivot );
+    Gia_ManSetPhasePattern( p->pAig, p->vPivot );
+    Gia_ManSetPhasePattern( p->pCare, p->vPivot );
+    if ( Gia_ManCheckCoPhase(p->pCare) )
+    {
+        printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
+        Ssc_ManStop( p );
+        return NULL;
+    }
+    // other things
+    p->vDisPairs = Vec_IntAlloc( 100 );
+    p->vPattern = Vec_IntAlloc( 100 );
+    p->vFanins = Vec_IntAlloc( 100 );
+    p->vFront = Vec_IntAlloc( 100 );
+    Ssc_GiaClassesInit( pAig );
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs computation of AIGs with choices.]
+  Synopsis    []
 
-  Description [Takes several AIGs and performs choicing.]
+  Description []
                
   SideEffects []
 
@@ -117,10 +137,11 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
 {
     Ssc_Man_t * p;
     Gia_Man_t * pResult;
+    Gia_Obj_t * pObj, * pRepr;
     clock_t clk, clkTotal = clock();
-    int i;
+    int i, fCompl, status;
     assert( Gia_ManRegNum(pCare) == 0 );
-    assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) );
+    assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
     assert( Gia_ManIsNormalized(pAig) );
     assert( Gia_ManIsNormalized(pCare) );
     // reset random numbers
@@ -131,14 +152,74 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
         return Gia_ManDup( pAig );
     // perform simulation 
 clk = clock();
-    for ( i = 0; i < 16; i++ )
+    if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
     {
-        Ssc_GiaRandomPiPattern( pAig, 10, NULL );
-        Ssc_GiaSimRound( pAig );
-        Ssc_GiaClassesRefine( pAig );
-        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        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;
+
+    // prepare user's AIG
+    Gia_ManFillValue(pAig);
+    Gia_ManConst0(pAig)->Value = 0;
+    Gia_ManForEachCi( pAig, pObj, i )
+        pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
+    // perform sweeping
+    Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+    Ssc_GiaSavePiPattern( pAig, p->vPivot );
+    Gia_ManForEachCand( pAig, pObj, i )
+    {
+        if ( pAig->iPatsPi == 64 * pPars->nWords )
+        {
+            Ssc_GiaSimRound( pAig );
+            Ssc_GiaClassesRefine( pAig );
+            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+            Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
+            Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+            Ssc_GiaSavePiPattern( pAig, p->vPivot );
+            Vec_IntClear( p->vDisPairs );
+        }
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( !Gia_ObjHasRepr(pAig, i) )
+            continue;
+        pRepr = Gia_ObjReprObj(pAig, i);
+        if ( pRepr->Value == pObj->Value )
+            continue;
+        assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
+        fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
+
+        // perform SAT call
+        clk = clock();
+        p->nSatCalls++;
+        status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
+        if ( status == l_False )
+        {
+            p->nSatCallsUnsat++;
+            p->timeSatUnsat += clock() - clk;
+            pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
+        }
+        else if ( status == l_True )
+        {
+            p->nSatCallsSat++;
+            p->timeSatSat += clock() - clk;
+            Ssc_GiaSavePiPattern( pAig, p->vPattern );
+            Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
+            Vec_IntPush( p->vDisPairs, i );
+        }
+        else if ( status == l_Undef )
+        {
+            p->nSatCallsUndec++;
+            p->timeSatUndec += clock() - clk;
+        }
+        else assert( 0 );
+    }
+
     // remember the resulting AIG
     pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
     if ( pResult == NULL )
@@ -163,11 +244,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
     if ( p->nConstrs == 0 )
     {
         pAig = Gia_ManDup( p );
-        pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 );
+        pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
         pCare->pName = Abc_UtilStrsav( "care" );
-        for ( i = 0; i < Gia_ManPiNum(p); i++ )
+        for ( i = 0; i < Gia_ManCiNum(p); i++ )
             Gia_ManAppendCi( pCare );
-        Gia_ManAppendCo( pCare, 1 );
+        Gia_ManAppendCo( pCare, 0 );
     }
     else
     {
@@ -176,6 +257,8 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
         pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
         Vec_IntFree( vOuts );
     }
+    pAig = Gia_ManDupLevelized( pResult = pAig );
+    Gia_ManStop( pResult );
     pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
     Gia_ManStop( pAig );
     Gia_ManStop( pCare );

src/proof/ssc/sscInt.h

@@ -35,7 +35,6 @@
 ////////////////////////////////////////////////////////////////////////
 
 
-
 ABC_NAMESPACE_HEADER_START
 
 
@@ -47,33 +46,37 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Ssc_Man_t_ Ssc_Man_t;
 struct Ssc_Man_t_
 {
-    // parameters
+    // user data
     Ssc_Pars_t *     pPars;          // choicing parameters
     Gia_Man_t *      pAig;           // subject AIG
     Gia_Man_t *      pCare;          // care set AIG
+    // internal data
     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
+    Vec_Int_t *      vId2Var;        // mapping of each node into its SAT var
+    Vec_Int_t *      vVar2Id;        // mapping of each SAT var into its node
+    Vec_Int_t *      vPivot;         // one SAT pattern
+    int              nSatVarsPivot;  // the number of variables for constraints
+    int              nSatVars;       // the current number of variables  
+    // temporary storage
+    Vec_Int_t *      vFront;         // supergate fanins
+    Vec_Int_t *      vFanins;        // supergate fanins
+    Vec_Int_t *      vPattern;       // counter-example
+    Vec_Int_t *      vDisPairs;      // disproved pairs
+    // SAT calls statistics
     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
+    int              nSatCallsUndec; // the number of undec 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          timeCnfGen;     // generation of CNF
     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
 };
@@ -82,28 +85,33 @@ struct Ssc_Man_t_
 ///                      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_ObjSatVar( Ssc_Man_t * p, int iObj )             { return Vec_IntEntry(p->vId2Var, iObj);     }
+static inline void   Ssc_ObjSetSatVar( Ssc_Man_t * p, int iObj, int Num ) { Vec_IntWriteEntry(p->vId2Var, iObj, Num);  Vec_IntWriteEntry(p->vVar2Id, Num, iObj);  }
+static inline void   Ssc_ObjCleanSatVar( Ssc_Man_t * p, int Num )         { Vec_IntWriteEntry(p->vId2Var, Vec_IntEntry(p->vVar2Id, Num), Num);  Vec_IntWriteEntry(p->vVar2Id, Num, 0);                        }
 
-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;          }
+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 void          Ssc_GiaClassesInit( Gia_Man_t * p );
 extern int           Ssc_GiaClassesRefine( Gia_Man_t * p );
+extern void          Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
 /*=== 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 );
+extern int           Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj, int fCompl );
 /*=== sscSim.c ===================================================*/
+extern void          Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
 extern void          Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
+extern void          Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
 extern void          Ssc_GiaSimRound( Gia_Man_t * p );
 extern Vec_Int_t *   Ssc_GiaFindPivotSim( Gia_Man_t * p );
 /*=== sscUtil.c ===================================================*/

src/proof/ssc/sscSat.c

@@ -29,6 +29,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Ssc_ObjSatLit( Ssc_Man_t * p, int Lit ) { return Abc_Var2Lit( Ssc_ObjSatVar(p, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -36,6 +37,217 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Gia_ManAddClausesMux( Ssc_Man_t * p, Gia_Obj_t * pNode )
+{
+    Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], LitF, LitI, LitT, LitE, RetValue;
+    assert( !Gia_IsComplement( pNode ) );
+    assert( Gia_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the Litiable numbers
+    LitF = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
+    LitI = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeI) );
+    LitT = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeT) );
+    LitE = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeE) );
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = Abc_LitNotCond(LitI, 1);
+    pLits[1] = Abc_LitNotCond(LitT, 1);
+    pLits[2] = Abc_LitNotCond(LitF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = Abc_LitNotCond(LitI, 1);
+    pLits[1] = Abc_LitNotCond(LitT, 0);
+    pLits[2] = Abc_LitNotCond(LitF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = Abc_LitNotCond(LitI, 0);
+    pLits[1] = Abc_LitNotCond(LitE, 1);
+    pLits[2] = Abc_LitNotCond(LitF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = Abc_LitNotCond(LitI, 0);
+    pLits[1] = Abc_LitNotCond(LitE, 0);
+    pLits[2] = Abc_LitNotCond(LitF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f
+
+    // t  + e   + f'
+    // t' + e'  + f
+
+    if ( LitT == LitE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = Abc_LitNotCond(LitT, 0);
+    pLits[1] = Abc_LitNotCond(LitE, 0);
+    pLits[2] = Abc_LitNotCond(LitF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = Abc_LitNotCond(LitT, 1);
+    pLits[1] = Abc_LitNotCond(LitE, 1);
+    pLits[2] = Abc_LitNotCond(LitF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Gia_ManAddClausesSuper( Ssc_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
+{
+    int i, RetValue, Lit, LitNode, pLits[2];
+    assert( !Gia_IsComplement(pNode) );
+    assert( Gia_ObjIsAnd( pNode ) );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    // add !B => !C   or   B + !C
+    LitNode = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
+    Vec_IntForEachEntry( vSuper, Lit, i )
+    {
+        pLits[0] = Ssc_ObjSatLit( p, Lit );
+        pLits[1] = Abc_LitNot( LitNode );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        // update literals
+        Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_IntPush( vSuper, LitNode );
+    RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
+    assert( RetValue );
+    (void) RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ssc_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+    // stop at complements, PIs, and MUXes
+    if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
+    {
+        Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
+        return;
+    }
+    Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
+    Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
+}
+static void Ssc_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+    assert( !Gia_IsComplement(pObj) );
+    assert( Gia_ObjIsAnd(pObj) );
+    Vec_IntClear( vSuper );
+    Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
+    Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ssc_ManCnfAddToFrontier( Ssc_Man_t * p, int Id, Vec_Int_t * vFront )
+{
+    Gia_Obj_t * pObj;
+    assert( Id > 0 );
+    if ( Ssc_ObjSatVar(p, Id) )
+        return;
+    pObj = Gia_ManObj( p->pFraig, Id );
+    Ssc_ObjSetSatVar( p, Id, p->nSatVars++ );
+    sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
+    if ( Gia_ObjIsAnd(pObj) )
+        Vec_IntPush( vFront, Id );
+}
+static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
+{
+    Gia_Obj_t * pNode;
+    int i, k, Id, Lit;
+    clock_t clk;
+    // quit if CNF is ready
+    if ( NodeId == 0 || Ssc_ObjSatVar(p, NodeId) )
+        return;
+clk = clock();
+    // start the frontier
+    Vec_IntClear( p->vFront );
+    Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
+    // explore nodes in the frontier
+    Gia_ManForEachObjVec( p->vFront, p->pFraig, pNode, i )
+    {
+        // create the supergate
+        assert( Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pNode)) );
+        if ( Gia_ObjIsMuxType(pNode) )
+        {
+            Vec_IntClear( p->vFanins );
+            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin0(pNode) ) );
+            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin1(pNode) ) );
+            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin0(pNode) ) );
+            Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin1(pNode) ) );
+            Vec_IntForEachEntry( p->vFanins, Id, k )
+                Ssc_ManCnfAddToFrontier( p, Id, p->vFront );
+            Gia_ManAddClausesMux( p, pNode );
+        }
+        else
+        {
+            Ssc_ManCollectSuper( p->pFraig, pNode, p->vFanins );
+            Vec_IntForEachEntry( p->vFanins, Lit, k )
+                Ssc_ManCnfAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
+            Gia_ManAddClausesSuper( p, pNode, p->vFanins );
+        }
+        assert( Vec_IntSize(p->vFanins) > 1 );
+    }
+p->timeCnfGen += clock() - clk;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Starts the SAT solver for constraints.]
 
   Description []
@@ -47,16 +259,25 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Ssc_ManStartSolver( Ssc_Man_t * p )
 {
-    Aig_Man_t * pAig = Gia_ManToAig( p->pFraig, 0 );
-    Cnf_Dat_t * pDat = Cnf_Derive( pAig, 0 );
+    Aig_Man_t * pMan = Gia_ManToAig( p->pFraig, 0 );
+    Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
+    Gia_Obj_t * pObj;
     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 );
+    assert( p->pSat == NULL && p->vId2Var == NULL );
+    assert( Aig_ManObjNumMax(pMan) == Gia_ManObjNum(p->pFraig) );
+    Aig_ManStop( pMan );
     // save variable mapping
-    p->vSatVars = Vec_IntAllocArray( pDat->pVarNums, Gia_ManObjNum(p->pFraig) );  pDat->pVarNums = NULL;
+    p->nSatVarsPivot = p->nSatVars = pDat->nVars;
+    p->vId2Var = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each node into its SAT var
+    p->vVar2Id = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each SAT var into its node
+    Ssc_ObjSetSatVar( p, 0, pDat->pVarNums[0] );
+    Gia_ManForEachCi( p->pFraig, pObj, i )
+    {
+        int iObj = Gia_ObjId( p->pFraig, pObj );
+        Ssc_ObjSetSatVar( p, iObj, pDat->pVarNums[iObj] );
+    }
+//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
     // start the SAT solver
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, pDat->nVars + 1000 );
@@ -90,20 +311,109 @@ void Ssc_ManStartSolver( Ssc_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Ssc_ManCollectSatPattern( Ssc_Man_t * p, Vec_Int_t * vPattern )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Vec_IntClear( vPattern );
+    Gia_ManForEachCi( p->pFraig, pObj, i )
+        Vec_IntPush( vPattern, sat_solver_var_value(p->pSat, Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pObj))) );
+}
 Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
 {
     Vec_Int_t * vInit;
-    Gia_Obj_t * pObj;
-    int i, status;
+    int 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)) );
+    vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) );
+    Ssc_ManCollectSatPattern( p, vInit );
     return vInit;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
+{
+    int pLitsSat[2], RetValue;
+//    if ( p->nTimeOut )
+//        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+
+    // create CNF
+    Ssc_ManCnfNodeAddToSolver( p, iRepr );
+    Ssc_ManCnfNodeAddToSolver( p, iNode );
+    sat_solver_compress( p->pSat );
+
+    // order the literals
+    pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 );
+    pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), 0 );
+    if ( pLitsSat[0] < pLitsSat[1] )
+        ABC_SWAP( int, pLitsSat[0], pLitsSat[1] );
+
+    // correct polarity
+    pLitsSat[1] = Abc_LitNotCond( pLitsSat[1], !fCompl ); // extra complement!
+    if ( !Abc_LitIsCompl(pLitsSat[1]) )
+    {
+        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
+        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
+    }
+    assert( pLitsSat[0] > pLitsSat[1] );
+    assert( Abc_LitIsCompl(pLitsSat[1]) );
+    assert( pLitsSat[1] != 0 );
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_False )
+    {
+        pLitsSat[0] = Abc_LitNot( pLitsSat[0] ); // compl
+        pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
+        RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
+        assert( RetValue );
+    }
+    else if ( RetValue == l_True )
+    {
+        Ssc_ManCollectSatPattern( p, p->vPattern );
+        return l_True;
+    }
+    else // if ( RetValue1 == l_Undef )
+        return l_Undef;
+
+    // if the old node was constant 0, we already know the answer
+    if ( pLitsSat[1] == 0 )
+        return l_False;
+    assert( pLitsSat[1] > 1 );
+
+    // solve under assumptions
+    // A = 0; B = 1     OR     A = 0; B = 0 
+    RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_False )
+    {
+        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
+        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
+        assert( RetValue );
+    }
+    else if ( RetValue == l_True )
+    {
+        Ssc_ManCollectSatPattern( p, p->vPattern );
+        return l_True;
+    }
+    else // if ( RetValue1 == l_Undef )
+        return l_Undef;
+    return l_False;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/proof/ssc/sscSim.c

@@ -34,51 +34,31 @@ static inline word Ssc_Random2()           { return ((word)Gia_ManRandom(0) << 3
 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];
+    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];
+    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;
+    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];
+    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 )
@@ -145,9 +125,23 @@ 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 );
+    Vec_WrdFill( p->vSimsPi, nWords * Gia_ManCiNum(p), 0 );
     assert( nWords == Gia_ObjSimWords( p ) );
 }
+void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
+{
+    word * pSimPi;
+    int i;
+    assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
+    if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
+        Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManCiNum(p) );
+    assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
+    pSimPi = Gia_ObjSimPi( p, 0 );
+    for ( i = 0; i < Gia_ManCiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
+        if ( Vec_IntEntry(vPat, i) )
+            Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
+    p->iPatsPi++;
+}
 void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
 {
     word * pSimPi;
@@ -163,20 +157,6 @@ void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
 //            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*************************************************************
 
@@ -191,7 +171,7 @@ void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
 ***********************************************************************/
 void Ssc_GiaResetSimInfo( Gia_Man_t * p )
 {
-    assert( Vec_WrdSize(p->vSimsPi) % Gia_ManPiNum(p) == 0 );
+    assert( Vec_WrdSize(p->vSimsPi) % Gia_ManCiNum(p) == 0 );
     if ( p->vSims == NULL )
         p->vSims = Vec_WrdAlloc(0);
     Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 );
@@ -208,7 +188,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
     // primary inputs
     pSim = Gia_ObjSim( p, 1 );
     pSim0 = Gia_ObjSimPi( p, 0 );
-    Gia_ManForEachPi( p, pObj, i )
+    Gia_ManForEachCi( p, pObj, i )
     {
         assert( pSim == Gia_ObjSimObj( p, pObj ) );
         Ssc_SimDup( pSim, pSim0, nWords, 0 );
@@ -216,7 +196,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
         pSim0 += nWords;
     }
     // intermediate nodes
-    pSim = Gia_ObjSim( p, 1+Gia_ManPiNum(p) );
+    pSim = Gia_ObjSim( p, 1+Gia_ManCiNum(p) );
     Gia_ManForEachAnd( p, pObj, i )
     {
         assert( pSim == Gia_ObjSim( p, i ) );
@@ -260,7 +240,7 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
     if ( iBit == -1 )
         return NULL;
     vInit = Vec_IntAlloc( 100 );
-    Gia_ManForEachPi( p, pObj, i )
+    Gia_ManForEachCi( p, pObj, i )
         Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
     return vInit;
 }