From 69b5bcad56f9352eea80d3e9b5e1322782522059 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 3 Apr 2008 20:01:00 -0700
Subject: Version abc80403_2

---
 src/aig/fra/fra.h    |  2 +-
 src/aig/fra/fraCec.c | 30 +++++++++++++++++++++---------
 2 files changed, 22 insertions(+), 10 deletions(-)

(limited to 'src/aig/fra')

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index dbe61522..7c2b95db 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -258,7 +258,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 /*=== fraCec.c ========================================================*/
 extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose );
+extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
 extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 779337bf..05f2493a 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -166,8 +166,7 @@ PRT( "Time", clock() - clk );
 
     // duplicate the AIG
 clk = clock();
-//    pAig = Aig_ManDupDfs( pTemp = pAig );
-    pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
+    pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
     {
@@ -247,22 +246,25 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
 {
     Aig_Man_t * pAig;
     Vec_Ptr_t * vParts;
     int i, RetValue = 1, nOutputs;
     // create partitions
-    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize );
+    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
     // solve the partitions
     nOutputs = -1;
     Vec_PtrForEachEntry( vParts, pAig, i )
     {
         nOutputs++;
         if ( fVerbose )
+        {
             printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
                 i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), 
                 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+            fflush( stdout );
+        }
         RetValue = Fra_FraigMiterStatus( pAig );
         if ( RetValue == 1 )
             continue;
@@ -306,8 +308,9 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose )
+int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
 {
+    Aig_Man_t * pTemp;
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
     int RetValue, clkTotal = clock();
 
@@ -324,10 +327,19 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int f
     assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) );
     assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) );
 
-    if ( fPartition )
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose );
-    else
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), fVerbose );
+    // make sure that the first miter has more nodes
+    if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
+    {
+        pTemp = pMan1;
+        pMan1 = pMan2;
+        pMan2 = pTemp;
+    }
+    assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
+
+    if ( nPartSize )
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+    else // no partitioning
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )
-- 
cgit v1.2.3