New abstraction code.

5 files changed, 159 insertions, 18 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f53d05f3..5f2b94a4 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -603,7 +603,7 @@ Gia_Man_t *                Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
 int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
 extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
-extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars );
+extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
 extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 511f418c..e30493a7 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -377,9 +377,9 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars )
+int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf )
 {
-    extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
+    extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses;
     Aig_Man_t * pAig;
@@ -393,7 +393,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars )
 */
     // perform abstraction
     pAig = Gia_ManToAigSimple( pGia );
-    vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
+    vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fUseCnf, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the map
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b879cb05..974f39d0 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1584,6 +1584,27 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) );
+    Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs abstraction of the AIG to preserve the included gates.]
 
   Description [The array contains 1 for those objects (const, RO, AND)
@@ -1642,6 +1663,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
     // create internal nodes
     Gia_ManForEachObjVec( vNodes, p, pObj, i )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+//        Gia_ManDupAbsGates_rec( pNew, pObj );
     // create PO
     Gia_ManForEachPo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigAbsGla.c
index 5c8263eb..1de6221c 100644
--- a/src/aig/saig/saigAbsGla.c
+++ b/src/aig/saig/saigAbsGla.c
@@ -20,6 +20,7 @@
 
 #include "saig.h"
 #include "satSolver.h"
+#include "cnf.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -49,6 +50,12 @@ struct Aig_GlaMan_t_
     Vec_Int_t *    vObj2Vec;   // maps obj ID into its vec ID
     Vec_Int_t *    vVec2Var;   // maps vec ID into its sat Var (nFrames per vec ID)
     Vec_Int_t *    vVar2Inf;   // maps sat Var into its frame and obj ID
+    // CNF computation
+    Vec_Ptr_t *    vLeaves;
+    Vec_Ptr_t *    vVolume;
+    Vec_Int_t *    vCover;
+    Vec_Ptr_t *    vObj2Cnf;
+    Vec_Int_t *    vLits;
     // SAT solver
     sat_solver *   pSat;
     // statistics
@@ -153,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_GlaCollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses )
+Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
 {
     Vec_Int_t * vAssigned;
     Aig_Obj_t * pObj;
@@ -242,6 +249,27 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
+    Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives abstraction.]
 
   Description []
@@ -274,7 +302,8 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // create internal nodes
     Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+//        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        Aig_GlaDeriveAbs_rec( pNew, pObj );
     // create PO
     Saig_ManForEachPo( p->pAig, pObj, i )
         pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@@ -371,11 +400,47 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
                 Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), 
                 Aig_ObjFaninC0(pObjLi) );
     }
-    assert( Aig_ObjIsNode(pObj) );
-    return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), 
-                Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), 
-                Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), 
-                Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+    else
+    { 
+        Vec_Int_t * vClauses;
+        int i, Entry;
+        assert( Aig_ObjIsNode(pObj) );
+        if ( p->vObj2Cnf == NULL )
+            return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), 
+                        Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), 
+                        Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), 
+                        Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+        // derive clauses
+        assert( pObj->fMarkA );
+        vClauses = Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) );
+        if ( vClauses == NULL )
+        {
+            Vec_PtrWriteEntry( p->vObj2Cnf, Aig_ObjId(pObj), (vClauses = Vec_IntAlloc(16)) );
+            Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, vClauses );
+        }
+        // derive variables
+        Cnf_CollectLeaves( pObj, p->vLeaves, 0 );
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i )
+            Aig_GlaFetchVar( p, pObj, k );
+        // translate clauses
+        assert( Vec_IntSize(vClauses) >= 2 );
+        assert( Vec_IntEntry(vClauses, 0) == 0 );
+        Vec_IntForEachEntry( vClauses, Entry, i )
+        {
+            if ( Entry == 0 )
+            {
+                Vec_IntClear( p->vLits );
+                continue;
+            }
+            Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
+            if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 )
+            {
+                if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) )
+                    return 0;
+            }
+        }       
+        return 1;
+    }
 }
 
 /**Function*************************************************************
@@ -389,7 +454,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
+Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fUseCnf )
 {
     Aig_GlaMan_t * p;
     int i;
@@ -416,6 +481,17 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
     Vec_IntPush( p->vVar2Inf, -1 );
     Vec_IntPush( p->vVar2Inf, -1 );
 
+    // CNF computation
+    if ( fUseCnf )
+    {
+        p->vLeaves   = Vec_PtrAlloc( 100 );
+        p->vVolume   = Vec_PtrAlloc( 100 );
+        p->vCover    = Vec_IntAlloc( 1 << 16 );
+        p->vObj2Cnf  = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
+        p->vLits     = Vec_IntAlloc( 100 );
+        Cnf_DeriveFastMark( pAig );
+    }
+
     // start the SAT solver
     p->pSat = sat_solver_new();
     sat_solver_setnvars( p->pSat, 256 );
@@ -448,6 +524,16 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
     Vec_IntFreeP( &p->vVec2Var );
     Vec_IntFreeP( &p->vVar2Inf );
 
+    if ( p->vObj2Cnf )
+    {
+        Vec_PtrFreeP( &p->vLeaves );
+        Vec_PtrFreeP( &p->vVolume );
+        Vec_IntFreeP( &p->vCover );
+        Vec_VecFreeP( (Vec_Vec_t **)&p->vObj2Cnf );
+        Vec_IntFreeP( &p->vLits );
+        Aig_ManCleanMarkA( p->pAig );
+    }
+
     if ( p->pSat )
         sat_solver_delete( p->pSat );
     ABC_FREE( p );
@@ -525,6 +611,34 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints current abstraction statistics.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, k;
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        if ( !Vec_IntEntry( p->vIncluded, i ) )
+            continue;
+        Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, p->vNodes );
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vVolume, pObj, k )
+        {
+            assert( Aig_ObjId(pObj) <= i );
+            Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs gate-level localization abstraction.]
 
   Description [Returns array of objects included in the abstraction. This array
@@ -536,7 +650,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
+Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose )
 {
     int nStart = 0;
     Vec_Int_t * vResult = NULL;
@@ -558,7 +672,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
     }
 
     // start the solver
-    p = Aig_GlaManStart( pAig );
+    p = Aig_GlaManStart( pAig, fUseCnf );
     p->nFramesMax = nFramesMax;
     p->nConfLimit = nConfLimit;
     p->fVerbose   = fVerbose;
@@ -660,6 +774,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
         ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
     }
     // prepare return value
+    Aig_GlaExtendIncluded( p );
     vResult = p->vIncluded;  p->vIncluded = NULL;
     Aig_GlaManStop( p );
     return vResult;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f07a5c5c..8bd9e5ae 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28888,13 +28888,13 @@ usage:
 int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Saig_ParBmc_t Pars, * pPars = &Pars;
-    int c;
+    int c, fUseCnf = 1;
     Saig_ParBmcSetDefaultParams( pPars );
     pPars->nStart     = 0;  //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
     pPars->nFramesMax = 50; //pPars->nStart + 10;
     pPars->nConfLimit = 5000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28953,6 +28953,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 ) 
                 goto usage;
             break;
+        case 'c':
+            fUseCnf ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28972,7 +28975,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars );
+    pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fUseCnf );
     if ( pPars->nStart == 0 )
        pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
@@ -28980,13 +28983,14 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-cvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with CEX-based abstraction\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+    Abc_Print( -2, "\t-c     : toggle using smarter CNF computation [default = %s]\n", fUseCnf? "yes": "no" );
     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;