From 94b26fe5a21199ddbd5c564331e7ee2848c8d498 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 25 Jun 2013 11:49:25 -0700
Subject: Improving CEC (command 'dcec') by integrating XOR balancing.

---
 src/base/abci/abc.c    |  6 +++---
 src/proof/fra/fraCec.c | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3279cf46..aeb146e2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19731,10 +19731,10 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
     }
 
-    if ( Abc_NtkLatchNum(pNtk1) || Abc_NtkLatchNum(pNtk2) )
+    if ( (pNtk1 && Abc_NtkLatchNum(pNtk1)) || (pNtk2 && Abc_NtkLatchNum(pNtk2)) )
     {
-        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
-        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+        if ( pNtk1 && fDelete1 ) Abc_NtkDelete( pNtk1 );
+        if ( pNtk2 && fDelete2 ) Abc_NtkDelete( pNtk2 );
         Abc_Print( -1, "Currently this command only works for networks without latches. Run \"comb\".\n" );
         return 1;
     }
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index 662a1d9e..aa95b992 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -272,6 +272,28 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Recognizes what nodes are inputs of the EXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountXors( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFan0, * pFan1;
+    int i, Counter = 0;
+    Aig_ManForEachNode( p, pObj, i )
+        if ( Aig_ObjIsMuxType(pObj) && Aig_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            Counter++;
+    return Counter;
+
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -338,6 +360,19 @@ ABC_PRT( "Time", Abc_Clock() - clk );
     for ( i = 0; i < 6; i++ )
     {
 //printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
+        // try XOR balancing
+        if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 )
+        {
+clk = Abc_Clock();
+            pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 );
+            Aig_ManStop( pTemp );
+            if ( fVerbose )
+            {
+                printf( "Balance-X:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
+ABC_PRT( "Time", Abc_Clock() - clk );
+            } 
+        }
+
         // run fraiging
 clk = Abc_Clock();
         pAig = Fra_FraigPerform( pTemp = pAig, pParams );
-- 
cgit v1.2.3