initial commit of public abc

1 files changed, 234 insertions, 13 deletions

diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index fa9030c5..0e004f87 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -19,6 +19,12 @@
 ***********************************************************************/
 
 #include "giaAig.h"
+#include "fra.h"
+#include "dch.h"
+#include "dar.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -84,6 +90,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
     if ( p->pEquivs )
         pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
@@ -122,6 +129,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManForEachObj( p, pObj, i )
@@ -138,8 +146,6 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
             assert( 0 );
     }
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    if ( pNew->pNexts )
-        Gia_ManDeriveReprs( pNew );
     return pNew;
 }
 
@@ -162,6 +168,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
@@ -178,7 +185,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     Aig_ManForEachPo( p, pObj, i )
         Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachPo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+        pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     return pNew;
 }
@@ -240,6 +247,7 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
 //    pNew->pSpec = Gia_UtilStrsav( p->pName );
     // duplicate representation of choice nodes
     if ( fChoices )
@@ -249,6 +257,10 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
     ppNodes[0] = Aig_ManConst0(pNew);
     Gia_ManForEachCi( p, pObj, i )
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
+    // transfer level
+    if ( p->vLevels )
+    Gia_ManForEachCi( p, pObj, i )
+        Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
@@ -282,6 +294,7 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
 //    pNew->pSpec = Gia_UtilStrsav( p->pName );
     // create the PIs
     ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
@@ -312,6 +325,48 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t ** ppNodes;
+    Gia_Obj_t * pObj;
+    int i;
+    ppNodes = ABC_ALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    // create the new manager
+    pNew = Aig_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->nConstrs = p->nConstrs;
+    // create the PIs
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+        else if ( Gia_ObjIsCi(pObj) )
+            ppNodes[i] = Aig_ObjCreatePi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            ppNodes[i] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+        else if ( Gia_ObjIsConst0(pObj) )
+            ppNodes[i] = Aig_ManConst0(pNew);
+        else
+            assert( 0 );
+        pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
+    }
+    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    ABC_FREE( ppNodes );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
 {
     Aig_Man_t * pMan;
@@ -329,41 +384,69 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
 
   Synopsis    [Transfers representatives from pGia to pAig.]
 
-  Description []
+  Description [Assumes that pGia was created from pAig.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
+void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
 {
     Aig_Obj_t * pObj;
     Gia_Obj_t * pGiaObj, * pGiaRepr;
     int i;
-    assert( p->pReprs == NULL );
+    assert( pAig->pReprs == NULL );
     assert( pGia->pReprs != NULL );
     // move pointers from AIG to GIA
-    Aig_ManForEachObj( p, pObj, i )
+    Aig_ManForEachObj( pAig, pObj, i )
     {
         assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
         pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
         pGiaObj->Value = i;
     }
     // set the pointers to the nodes in AIG
-    Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Gia_ManForEachObj( pGia, pGiaObj, i )
+    {
+        pGiaRepr = Gia_ObjReprObj( pGia, i );
+        if ( pGiaRepr == NULL )
+            continue;
+        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers representatives from pGia to pAig.]
+
+  Description [Assumes that pAig was created from pGia.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
+{
+    Gia_Obj_t * pGiaObj, * pGiaRepr;
+    int i;
+    assert( pAig->pReprs == NULL );
+    assert( pGia->pReprs != NULL );
+    // set the pointers to the nodes in AIG
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
     Gia_ManForEachObj( pGia, pGiaObj, i )
     {
         pGiaRepr = Gia_ObjReprObj( pGia, i );
         if ( pGiaRepr == NULL )
             continue;
-        Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) );
+        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Gia_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Gia_Lit2Var(pGiaObj->Value)) );
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Applied DC2 to the GIA manager.]
+  Synopsis    [Transfers representatives from pAig to pGia.]
 
   Description []
                
@@ -372,21 +455,159 @@ void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p )
+void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
 {
-    extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
+    Gia_Obj_t * pObjGia; 
+    Aig_Obj_t * pObjAig, * pReprAig;
+    int i;
+    assert( pAig->pReprs != NULL );
+    assert( pGia->pReprs == NULL );
+    assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManPoNum(pAig) );
+    pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
+    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
+        Gia_ObjSetRepr( pGia, i, GIA_VOID );
+    Gia_ManForEachObj( pGia, pObjGia, i )
+    {
+//        Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 );
+        if ( Gia_ObjIsCo(pObjGia) )
+            continue;
+        assert( i == 0 || !Gia_LitIsCompl(Gia_ObjValue(pObjGia)) );
+        pObjAig  = Aig_ManObj( pAig, Gia_Lit2Var(Gia_ObjValue(pObjGia)) );
+        pObjAig->iData = i;
+    }
+    Aig_ManForEachObj( pAig, pObjAig, i )
+    {
+        if ( Aig_ObjIsPo(pObjAig) )
+            continue;
+        if ( pAig->pReprs[i] == NULL )
+            continue;
+        pReprAig = pAig->pReprs[i];
+        Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
+    }
+    pGia->pNexts = Gia_ManDeriveNexts( pGia );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Applies DC2 to the GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
+{
+//    extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
     Gia_Man_t * pGia;
     Aig_Man_t * pNew, * pTemp;
     pNew = Gia_ManToAig( p, 0 );
-    pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 );
+    pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
     Aig_ManStop( pTemp );
     pGia = Gia_ManFromAig( pNew );
     Aig_ManStop( pNew );
     return pGia;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
+{
+    Gia_Man_t * pGia;
+    Aig_Man_t * pNew;
+    pNew = Gia_ManToAig( p, 0 );
+    pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
+    pGia = Gia_ManFromAig( pNew );
+    Aig_ManStop( pNew );
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes equivalences after structural sequential cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose )
+{
+    Aig_Man_t * pNew, * pTemp;
+    pNew  = Gia_ManToAigSimple( p );
+    pTemp = Aig_ManScl( pNew, fConst, fEquiv, fVerbose );
+    Gia_ManReprFromAigRepr( pNew, p );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves SAT problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSolveSat( Gia_Man_t * p )
+{
+//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    Aig_Man_t * pNew;
+    int RetValue, clk = clock();
+    pNew = Gia_ManToAig( p, 0 );
+    RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0 );
+    if ( RetValue == 0 )
+    {
+        Gia_Obj_t * pObj;
+        int i, * pInit = (int *)pNew->pData;
+        Gia_ManConst0(p)->fMark0 = 0;
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->fMark0 = pInit[i];
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachPo( p, pObj, i )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
+        Gia_ManForEachPo( p, pObj, i )
+            if ( pObj->fMark0 != 1 )
+                break;
+        if ( i != Gia_ManPoNum(p) )
+            Abc_Print( 1, "Counter-example verification has failed.  " );
+//        else
+//            Abc_Print( 1, "Counter-example verification succeeded.  " );
+    }
+/*
+    else if ( RetValue == 1 )
+        Abc_Print( 1, "The SAT problem is unsatisfiable.  " );
+    else if ( RetValue == -1 )
+        Abc_Print( 1, "The SAT problem is undecided.  " );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+*/
+    Aig_ManStop( pNew );
+    return RetValue;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+