Experiments with SAT sweeping.

2 files changed, 161 insertions, 30 deletions

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 0e9f5526..f7f873cd 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -269,6 +269,7 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
         pTails[i] = i;
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
     {
+        //if ( p->pReprs[i].iRepr == GIA_VOID )
         if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
             continue;
         pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
@@ -2589,6 +2590,123 @@ void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlo
     Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Changing node order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManChangeOrder_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+Gia_Man_t * Gia_ManChangeOrder( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, k;
+    Gia_ManFillValue( p );
+    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);
+    Gia_ManForEachClass( p, i )
+        Gia_ClassForEachObj( p, i, k )
+            Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
+    Gia_ManForEachConst( p, k )
+        Gia_ManChangeOrder_rec( pNew, p, Gia_ManObj(p, k) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManChangeOrder_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) );
+    return pNew;
+}
+void Gia_ManTransferEquivs( Gia_Man_t * p, Gia_Man_t * pNew )
+{
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr;
+    assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
+    assert( p->pReprs != NULL );
+    assert( p->pNexts != NULL );
+    assert( pNew->pReprs == NULL );
+    assert( pNew->pNexts == NULL );
+    // start representatives
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
+    for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+            Gia_ObjSetRepr( pNew, iNode, iRepr );
+    }
+    Vec_IntFree( vClass );
+    pNew->pNexts = Gia_ManDeriveNexts( pNew );
+}
+void Gia_ManTransferTest( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i;
+    Gia_Rpr_t * pReprs = p->pReprs;  // representatives (for CIs and ANDs)
+    int *       pNexts = p->pNexts;  // next nodes in the equivalence classes
+    Gia_Man_t * pNew = Gia_ManChangeOrder(p);
+    //Gia_ManEquivPrintClasses( p, 1, 0 );
+    assert( Gia_ManObjNum(p) == Gia_ManObjNum(pNew) );
+    Gia_ManTransferEquivs( p, pNew );
+    p->pReprs = NULL;
+    p->pNexts = NULL;
+    // make new point to old
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        assert( !Abc_LitIsCompl(pObj->Value) );
+        Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
+    }
+    Gia_ManTransferEquivs( pNew, p );
+    //Gia_ManEquivPrintClasses( p, 1, 0 );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        pReprs[i].fProved = 0;
+        //printf( "%5d :    %5d %5d    %5d %5d\n", i, *(int*)&p->pReprs[i], *(int*)&pReprs[i], (int)p->pNexts[i], (int)pNexts[i] );
+    if ( memcmp(p->pReprs, pReprs, sizeof(int)*Gia_ManObjNum(p)) )
+        printf( "Verification of reprs failed.\n" );
+    else
+        printf( "Verification of reprs succeeded.\n" );
+    if ( memcmp(p->pNexts, pNexts, sizeof(int)*Gia_ManObjNum(p)) )
+        printf( "Verification of nexts failed.\n" );
+    else
+        printf( "Verification of nexts succeeded.\n" );
+    ABC_FREE( pNew->pReprs );
+    ABC_FREE( pNew->pNexts );
+    ABC_FREE( pReprs );
+    ABC_FREE( pNexts );
+    Gia_ManStop( pNew );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index d01b7bd5..a9332f1d 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -79,6 +79,7 @@ static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -92,24 +93,11 @@ static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
 ***********************************************************************/
 Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
 {
-    Cec4_Man_t * p;
-    Gia_Obj_t * pObj; int i;
-    //assert( Gia_ManRegNum(pAig) == 0 );
-    p = ABC_CALLOC( Cec4_Man_t, 1 );
+    Cec4_Man_t * p = ABC_CALLOC( Cec4_Man_t, 1 );
     memset( p, 0, sizeof(Cec4_Man_t) );
-    p->timeStart    = Abc_Clock();
-    p->pPars        = pPars;
-    p->pAig         = pAig;
-    pAig->pData     = p->pSat; // point AIG manager to the solver
-    // create new manager
-    p->pNew         = Gia_ManStart( Gia_ManObjNum(pAig) );
-    Gia_ManFillValue( pAig );
-    Gia_ManConst0(pAig)->Value = 0;
-    Gia_ManForEachCi( pAig, pObj, i )
-        pObj->Value = Gia_ManAppendCi( p->pNew );
-    Gia_ManHashAlloc( p->pNew );
-    Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
-    // SAT solving
+    p->timeStart     = Abc_Clock();
+    p->pPars         = pPars;
+    p->pAig          = pAig;
     p->pSat          = bmcg_sat_solver_start();
     p->vFrontier     = Vec_PtrAlloc( 1000 );
     p->vFanins       = Vec_PtrAlloc( 100 );
@@ -119,6 +107,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     p->vCands        = Vec_IntAlloc( 100 );
     p->vVisit        = Vec_IntAlloc( 100 );
     p->vPat          = Vec_IntAlloc( 100 );
+    //pAig->pData     = p->pSat; // point AIG manager to the solver
     return p;
 }
 void Cec4_ManDestroy( Cec4_Man_t * p )
@@ -158,6 +147,21 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
     Vec_IntFreeP( &p->vPat );
     ABC_FREE( p );
 }
+Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj; int i;
+    Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
+    pNew->pName = Abc_UtilStrsav( pAig->pName );
+    pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
+    Gia_ManFillValue( pAig );
+    Gia_ManConst0(pAig)->Value = 0;
+    Gia_ManForEachCi( pAig, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManHashAlloc( pNew );
+    Vec_IntFill( &pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(pAig) );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -933,16 +937,24 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p )
 {
     abctime clk = Abc_Clock();
     int i, k, iLit, nPats = 64 * p->pAig->nSimWords;
-    Gia_Obj_t * pObj;
     // collect candidate nodes
-    Vec_IntClear( p->vCands );
-    Gia_ManForEachObj( p->pAig, pObj, i )
+    if ( p->pPars->nGenIters )
     {
-        pObj->fMark0 = pObj->fMark1 = 0;
-        if ( !Gia_ObjIsHead(p->pAig, i) )
-            continue;
-        Gia_ClassForEachObj1( p->pAig, i, k )
-            Vec_IntPush( p->vCands, k );
+        if ( Vec_IntSize(p->vCands) == 0 )
+        {
+            for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
+                if ( Gia_ObjRepr(p->pAig, i) != GIA_VOID )
+                    Vec_IntPush( p->vCands, i );
+        }
+        else
+        {
+            int iObj, k = 0;
+            Vec_IntForEachEntry( p->vCands, iObj, i )
+                if ( Gia_ObjRepr(p->pAig, iObj) != GIA_VOID )
+                    Vec_IntWriteEntry( p->vCands, k++, iObj );
+            Vec_IntShrink( p->vCands, k );
+            assert( Vec_IntSize(p->vCands) > 0 );
+        }
     }
     // generate the given number of patterns
     for ( i = 0, p->pAig->iPatsPi = 1; i < p->pPars->nGenIters * nPats && p->pAig->iPatsPi < nPats; p->pAig->iPatsPi++, i++ )
@@ -969,6 +981,7 @@ void Cec4_ManGeneratePatterns( Cec4_Man_t * p )
     p->timeGenPats += Abc_Clock() - clk;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Internal simulation APIs.]
@@ -1106,7 +1119,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
             p->timeSatSat += Abc_Clock() - clk;
         RetValue = 0;
         // this is not needed, but we keep it here anyway, because it takes very little time
-        Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
+        //Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
         // resimulated once in a while
         if ( p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1 )
         {
@@ -1186,7 +1199,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
     // check if any output trivially fails under all-0 pattern
     Gia_ManRandomW( 1 );
     Gia_ManSetPhase( p );
-    Gia_ManStaticFanoutStart( p );
+    //Gia_ManStaticFanoutStart( p );
     if ( pPars->fCheckMiter ) 
     {
         Gia_ManForEachCo( p, pObj, i )
@@ -1219,7 +1232,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
             Cec4_ManPrintStats( p, pPars, pMan );
     }
+
     p->iPatsPi = 0;
+    pMan->pNew = Cec4_ManStartNew( p );
     Gia_ManForEachAnd( p, pObj, i )
     {
         //Gia_Obj_t * pObjNew; 
@@ -1263,8 +1278,6 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         Gia_ManForEachCo( p, pObj, i )
             pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
         *ppNew = Gia_ManCleanup( pMan->pNew );
-        (*ppNew)->pName = Abc_UtilStrsav( p->pName );
-        (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec );
     }
 finalize:
     if ( pPars->fVerbose )
@@ -1275,7 +1288,7 @@ finalize:
             pMan->nSatUndec,  
             pMan->nSimulates, pMan->nRecycles );
     Cec4_ManDestroy( pMan );
-    Gia_ManStaticFanoutStop( p );
+    //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
     return p->pCexSeq ? 0 : 1;
 }