New abstraction code.

4 files changed, 151 insertions, 14 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;