Experiments with the SAT sweeper.

berkeley-abc · Sep 4, 2023 · 3014694 · 3014694
1 parent a13dae7
commit 3014694
Show file tree

Hide file tree

Showing 2 changed files with 76 additions and 6 deletions.
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
@@ -1604,6 +1604,47 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates while adding self-loops to the registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+    Gia_Man_t * pNew, * pTemp; 
+    Gia_Obj_t * pObj;
+    int i, iLit0, iLit1;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) + 3 * Vec_IntSize(vPairs) );
+    pNew->pName = Abc_UtilStrsav( "miter" );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Vec_IntForEachEntryDouble( vPairs, iLit0, iLit1, i )
+    {
+        int Lit0 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit0))->Value, Abc_LitIsCompl(iLit0) );
+        int Lit1 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit1))->Value, Abc_LitIsCompl(iLit1) );
+        Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Lit0, Lit1) );
+    }
+    Vec_IntForEachEntry( vTemp, iLit0, i )
+        Gia_ManAppendCo( pNew, iLit0 );
+    Vec_IntFree( vTemp );
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG in the DFS order.]

diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
@@ -101,6 +101,7 @@ struct Cec4_Man_t_
     Vec_Int_t *      vDisprPairs;
     Vec_Bit_t *      vFails;
     Vec_Bit_t *      vCoDrivers;
+    Vec_Int_t *      vPairs;   
     int              iPosRead;       // candidate reading position
     int              iPosWrite;      // candidate writing position
     int              iLastConst;     // last const node proved
@@ -250,6 +251,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     p->vPat          = Vec_IntAlloc( 100 );
     p->vDisprPairs   = Vec_IntAlloc( 100 );
     p->vFails        = Vec_BitStart( Gia_ManObjNum(pAig) );
+    p->vPairs        = pPars->fUseCones ? Vec_IntAlloc( 100 ) : NULL;
     //pAig->pData     = p->pSat; // point AIG manager to the solver
     //Vec_IntFreeP( &p->pAig->vPats );
     //p->pAig->vPats = Vec_IntAlloc( 1000 );
@@ -304,6 +306,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
     Vec_IntFreeP( &p->vPat );
     Vec_IntFreeP( &p->vDisprPairs );
     Vec_BitFreeP( &p->vFails );
+    Vec_IntFreeP( &p->vPairs );
     Vec_BitFreeP( &p->vCoDrivers );
     Vec_IntFreeP( &p->vRefClasses );
     Vec_IntFreeP( &p->vRefNodes );
@@ -1686,12 +1689,26 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
     {
         p->nSatUndec++;
         assert( status == GLUCOSE_UNDEC );
-        Gia_ObjSetFailed( p->pAig, iObj );
-        Vec_BitWriteEntry( p->vFails, iObj, 1 );
-        //if ( iRepr )
-        //Vec_BitWriteEntry( p->vFails, iRepr, 1 );
-        p->timeSatUndec += Abc_Clock() - clk;
-        RetValue = 2;
+        if ( p->vPairs ) // speculate
+        {
+            Vec_IntPushTwo( p->vPairs, Abc_Var2Lit(iRepr, 0), Abc_Var2Lit(iObj, fCompl) );
+            p->timeSatUndec += Abc_Clock() - clk;
+            // mark as proved
+            pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
+            Gia_ObjSetProved( p->pAig, iObj );
+            if ( iRepr == 0 )
+                p->iLastConst = iObj;
+            RetValue = 1;
+        }
+        else
+        {
+            Gia_ObjSetFailed( p->pAig, iObj );
+            Vec_BitWriteEntry( p->vFails, iObj, 1 );
+            //if ( iRepr )
+            //Vec_BitWriteEntry( p->vFails, iRepr, 1 );
+            p->timeSatUndec += Abc_Clock() - clk;
+            RetValue = 2;
+        }
     }
     return RetValue;
 }
@@ -1896,6 +1913,18 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
             pMan->nSatSat,   pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat  -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],  
             pMan->nSatUndec,  
             pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
+    if ( pMan->vPairs && Vec_IntSize(pMan->vPairs) )
+    {
+        extern char * Extra_FileNameGeneric( char * FileName );
+        char pFileName[1000], * pBase = Extra_FileNameGeneric(p->pName);
+        extern Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs );
+        Gia_Man_t * pM = Gia_ManDupMiterCones( p, pMan->vPairs );
+        sprintf( pFileName, "%s_miter.aig", pBase );
+        Gia_AigerWrite( pM, pFileName, 0, 0, 0 );
+        Gia_ManStop( pM );
+        ABC_FREE( pBase );
+        printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs) : -1 );
+    }
     Cec4_ManDestroy( pMan );
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );