Experiments with CEC for arithmetic circuits.

1 files changed, 224 insertions, 11 deletions

diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 6224d37f..91edbaa5 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "proof/cec/cec.h"
+#include "proof/acec/acec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,6 +35,147 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+Vec_Int_t * Gia_WriteDotAigMarks( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds )
+{
+    int i;
+    Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) );
+    for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
+    {
+        Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+0), Abc_Var2Lit(i+1, 0) );
+        Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+1), Abc_Var2Lit(i+1, 0) );
+    }
+    for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
+    {
+        Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+3), Abc_Var2Lit(i+1, 1) );
+        Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+4), Abc_Var2Lit(i+1, 1) );
+    }
+    return vMarks;
+}
+int Gia_WriteDotAigLevel_rec( Gia_Man_t * p, Vec_Int_t * vMarks, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int Id, Vec_Int_t * vLevel )
+{
+    int Level = Vec_IntEntry(vLevel, Id), Mark = Vec_IntEntry(vMarks, Id);
+    if ( Level || Mark == -1 )
+        return Level;
+    if ( Mark == 0 )
+    {
+        Gia_Obj_t * pObj = Gia_ManObj( p, Id );
+        int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel );
+        int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel );
+        Level = Abc_MaxInt(Level0, Level1) + 1;
+        Vec_IntWriteEntry( vLevel, Id, Level );
+        Vec_IntWriteEntry( vMarks, Id, -1 );
+    }
+    else if ( Abc_LitIsCompl(Mark) ) // FA
+    {
+        int i, * pFanins = Vec_IntEntryP( vFadds, 5*(Abc_Lit2Var(Mark)-1) );
+        assert( pFanins[3] == Id || pFanins[4] == Id );
+        for ( i = 0; i < 3; i++ )
+            Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, pFanins[i], vLevel ) );
+        Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 );
+        Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 );
+    }
+    else  // HA
+    {
+        int * pFanins = Vec_IntEntryP( vHadds, 2*(Abc_Lit2Var(Mark)-1) );
+        Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] );
+        int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel );
+        int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel );
+        assert( pFanins[0] == Id || pFanins[1] == Id );
+        Level = Abc_MaxInt(Level0, Level1) + 1;
+        Vec_IntWriteEntry( vLevel, pFanins[0], Level );
+        Vec_IntWriteEntry( vLevel, pFanins[1], Level );
+    }
+    return Level;
+}
+int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t ** pvMarks, Vec_Int_t ** pvLevel )
+{
+    Vec_Int_t * vMarks = Gia_WriteDotAigMarks( p, vFadds, vHadds );
+    Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) );
+    int i, Id, Level = 0;
+    Vec_IntWriteEntry( vMarks, 0, -1 );
+    Gia_ManForEachCiId( p, Id, i )
+        Vec_IntWriteEntry( vMarks, Id, -1 );
+    Gia_ManForEachCoDriverId( p, Id, i )
+        Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec(p, vMarks, vFadds, vHadds, Id, vLevel) );
+    Gia_ManForEachCoId( p, Id, i )
+        Vec_IntWriteEntry( vMarks, Id, -1 );
+    *pvMarks = vMarks;
+    *pvLevel = vLevel;
+    return Level;
+}
+*/
+int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap )
+{
+    Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vRemap = Vec_IntStartNatural( Gia_ManObjNum(p) );
+    int i, k, Id, Entry, LevelMax = 0;
+
+    Vec_IntWriteEntry( vMarks, 0, -1 );
+    Gia_ManForEachCiId( p, Id, i )
+        Vec_IntWriteEntry( vMarks, Id, -1 );
+    Gia_ManForEachCoId( p, Id, i )
+        Vec_IntWriteEntry( vMarks, Id, -1 );
+
+    Vec_IntForEachEntry( vRecord, Entry, i )
+    {
+        int Level = 0;
+        int Node = Abc_Lit2Var2(Entry);
+        int Attr = Abc_Lit2Att2(Entry);
+        if ( Attr == 2 )
+        {
+            int * pFanins = Vec_IntEntryP( vFadds, 5*Node );
+            for ( k = 0; k < 3; k++ )
+                Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFanins[k]) );
+            Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 );
+            Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 );
+            Vec_IntWriteEntry( vMarks, pFanins[4], Entry );
+            Vec_IntWriteEntry( vRemap, pFanins[3], pFanins[4] );
+            //printf( "Making FA output %d.\n", pFanins[4] );
+        }
+        else if ( Attr == 1 )
+        {
+            int * pFanins = Vec_IntEntryP( vHadds, 2*Node );
+            Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] );
+            int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, pFanins[1]), Gia_ObjFaninId1(pObj, pFanins[1]) };
+            for ( k = 0; k < 2; k++ )
+                Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) );
+            Vec_IntWriteEntry( vLevel, pFanins[0], Level+1 );
+            Vec_IntWriteEntry( vLevel, pFanins[1], Level+1 );
+            Vec_IntWriteEntry( vMarks, pFanins[1], Entry );
+            Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] );
+            //printf( "Making HA output %d.\n", pFanins[1] );
+        }
+        else
+        {
+            Gia_Obj_t * pObj = Gia_ManObj( p, Node );
+            int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) };
+            for ( k = 0; k < 2; k++ )
+                Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) );
+            Vec_IntWriteEntry( vLevel, Node, Level+1 );
+            Vec_IntWriteEntry( vMarks, Node, -1 );
+            //printf( "Making node %d.\n", Node );
+        }
+        LevelMax = Abc_MaxInt( LevelMax, Level+1 );
+    }
+    *pvLevel = vLevel;
+    *pvMarks = vMarks;
+    *pvRemap = vRemap;
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the graph structure of AIG for DOT.]
 
   Description [Useful for graph visualization using tools such as GraphViz: 
@@ -43,16 +186,17 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
+void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fAdders )
 {
+    Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL;
     FILE * pFile;
     Gia_Obj_t * pNode;//, * pTemp, * pPrev;
     int LevelMax, Prev, Level, i;
     int fConstIsUsed = 0;
 
-    if ( Gia_ManAndNum(pMan) > 300 )
+    if ( Gia_ManAndNum(pMan) > 1000 )
     {
-        fprintf( stdout, "Cannot visualize AIG with more than 300 nodes.\n" );
+        fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" );
         return;
     }
     if ( (pFile = fopen( pFileName, "w" )) == NULL )
@@ -71,7 +215,18 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
                 pNode->fMark0 = 1;
 
     // compute levels
-    LevelMax = 1 + Gia_ManLevelNum( pMan );
+    if ( fAdders )
+    {
+        Vec_IntFreeP( &pMan->vLevels );
+        vFadds   = Gia_ManDetectFullAdders( pMan, 0 );
+        vHadds   = Gia_ManDetectHalfAdders( pMan, 0 );
+        vRecord  = Gia_PolynFindOrder( pMan, vFadds, vHadds, 0, 0 );
+        LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap );
+    }
+    else
+        LevelMax = 1 + Gia_ManLevelNum( pMan );
+
+    // set output levels
     Gia_ManForEachCo( pMan, pNode, i )
         Vec_IntWriteEntry( pMan->vLevels, Gia_ObjId(pMan, pNode), LevelMax );
 
@@ -196,6 +351,8 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
         fprintf( pFile, "  Level%d;\n",  Level );
         Gia_ManForEachObj( pMan, pNode, i )
         {
+            if ( vMarks && Vec_IntEntry(vMarks, i) == 0 )
+                continue;
             if ( (int)Gia_ObjLevel(pMan, pNode) != Level )
                 continue;
 /*
@@ -206,8 +363,14 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
                     Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" );
 */
             fprintf( pFile, "  Node%d [label = \"%d\"", i, i ); 
-
-            if ( Gia_ObjIsXor(pNode) )
+            if ( vMarks && Vec_IntEntry(vMarks, i) > 0 )
+            {
+                if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 )
+                    fprintf( pFile, ", shape = doubleoctagon" );
+                else 
+                    fprintf( pFile, ", shape = octagon" );
+            }
+            else if ( Gia_ObjIsXor(pNode) )
                 fprintf( pFile, ", shape = doublecircle" );
             else if ( Gia_ObjIsMux(pMan, pNode) )
                 fprintf( pFile, ", shape = trapezium" );
@@ -277,10 +440,54 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
     {
         if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) )
             continue;
+        if ( vMarks && Vec_IntEntry(vMarks, i) == 0 )
+            continue;
+        // consider half/full-adder
+        if ( vMarks && Vec_IntEntry(vMarks, i) > 0 )
+        {
+            int k, Mark = Vec_IntEntry(vMarks, i);
+            if ( Abc_Lit2Att2(Mark) == 2 ) // FA
+            {
+                int * pFanins = Vec_IntEntryP( vFadds, 5*Abc_Lit2Var2(Mark) );
+                if ( pFanins[3] == i )
+                    continue;
+                assert( pFanins[4] == i );
+                // generate the edge from this node to the next
+                for ( k = 0; k < 3; k++ )
+                {
+                    fprintf( pFile, "Node%d",  i );
+                    fprintf( pFile, " -> " );
+                    fprintf( pFile, "Node%d",  Vec_IntEntry(vRemap, pFanins[k]) );
+                    fprintf( pFile, " [" );
+                    fprintf( pFile, "style = %s", "bold" );
+                    fprintf( pFile, "]" );
+                    fprintf( pFile, ";\n" );
+                }
+            }
+            else  // HA
+            {
+                int * pFanins = Vec_IntEntryP( vHadds, 2*Abc_Lit2Var2(Mark) );
+                int pFaninsIn[2] = { Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)), Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) };
+                if ( pFanins[0] == i )
+                    continue;
+                assert( pFanins[1] == i );
+                for ( k = 0; k < 2; k++ )
+                {
+                    fprintf( pFile, "Node%d",  i );
+                    fprintf( pFile, " -> " );
+                    fprintf( pFile, "Node%d",  Vec_IntEntry(vRemap, pFaninsIn[k]) );
+                    fprintf( pFile, " [" );
+                    fprintf( pFile, "style = %s", "bold" );
+                    fprintf( pFile, "]" );
+                    fprintf( pFile, ";\n" );
+                }
+            }
+            continue;
+        }
         // generate the edge from this node to the next
         fprintf( pFile, "Node%d",  i );
         fprintf( pFile, " -> " );
-        fprintf( pFile, "Node%d",  Gia_ObjFaninId0(pNode, i) );
+        fprintf( pFile, "Node%d",  vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)) : Gia_ObjFaninId0(pNode, i) );
         fprintf( pFile, " [" );
         fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "bold" );
 //        if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
@@ -292,7 +499,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
         // generate the edge from this node to the next
         fprintf( pFile, "Node%d",  i );
         fprintf( pFile, " -> " );
-        fprintf( pFile, "Node%d",  Gia_ObjFaninId1(pNode, i) );
+        fprintf( pFile, "Node%d",  vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) : Gia_ObjFaninId1(pNode, i) );
         fprintf( pFile, " [" );
         fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "bold" );
 //        if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
@@ -305,7 +512,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
         // generate the edge from this node to the next
         fprintf( pFile, "Node%d",  i );
         fprintf( pFile, " -> " );
-        fprintf( pFile, "Node%d",  Gia_ObjFaninId2(pMan, i) );
+        fprintf( pFile, "Node%d",  vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId2(pMan, i)) : Gia_ObjFaninId2(pMan, i) );
         fprintf( pFile, " [" );
         fprintf( pFile, "style = %s", Gia_ObjFaninC2(pMan, pNode)? "dotted" : "bold" );
 //        if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
@@ -349,7 +556,13 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
     else if ( pMan->nXors || pMan->nMuxes )
         Gia_ManCleanMark0( pMan );
 
+    Vec_IntFreeP( &vFadds );
+    Vec_IntFreeP( &vHadds );
+    Vec_IntFreeP( &vRecord );
+
     Vec_IntFreeP( &pMan->vLevels );
+    Vec_IntFreeP( &vMarks );
+    Vec_IntFreeP( &vRemap );
 }
 
 /**Function*************************************************************
@@ -363,7 +576,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold )
+void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders )
 {
     extern void Abc_ShowFile( char * FileNameDot );
     static int Counter = 0;
@@ -380,7 +593,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold )
     }
     fclose( pFile );
     // generate the file
-    Gia_WriteDotAig( pMan, FileNameDot, vBold );
+    Gia_WriteDotAig( pMan, FileNameDot, vBold, fAdders );
     // visualize the file 
     Abc_ShowFile( FileNameDot );
 }