Version abc80508

6 files changed, 35 insertions, 20 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 44cfe847..7311d414 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -226,7 +226,7 @@ struct Fra_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
-static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
+static inline unsigned     Fra_ObjRandomSim()                                            { return Aig_ManRandom(0);               }
 
 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 05f2493a..e91478a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -47,14 +47,16 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     int status, RetValue, clk = clock();
     Vec_Int_t * vCiIds;
 
-    assert( Aig_ManPoNum(pMan) == 1 );
+    assert( Aig_ManRegNum(pMan) == 0 );
     pMan->pData = NULL;
 
     // derive CNF
-    pCnf = Cnf_Derive( pMan, 0 );
-//    pCnf = Cnf_DeriveSimple( pMan, 0 );
+    pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+//    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
     // convert into the SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // add the OR clause for the outputs
+    Cnf_DataWriteOrClause( pSat, pCnf );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
     Cnf_DataFree( pCnf );
     // solve SAT
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index c9ea4907..6f0a2012 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -606,7 +606,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 
     // simulate the AIG
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
@@ -661,7 +662,8 @@ PRT( "Infoseq", clock() - clk );
 
     // perform combinational simulation
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
@@ -728,7 +730,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
 
     // simulate the AIG
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
@@ -743,7 +746,8 @@ if ( p->fVerbose )
 
     // perform combinational simulation
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
@@ -1614,7 +1618,8 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     int * pStart, * pVar2Id; 
     int clk = clock();
     // simulate the circuit with nCombSimWords * 32 = 64K patterns
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
     // create mapping from SAT vars to node IDs
     pVar2Id = ALLOC( int, p->pCnf->nVars );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 222f5bcc..b2156193 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -333,7 +333,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
 
     // generate random sim-info at register outputs
     vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     for ( i = 0; i < nRegs; i++ )
     {
         pSim1 = Vec_PtrEntry( vSimInfo, i );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index da7c37a3..b8cf13c5 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -120,7 +120,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
     // set random number generator
-    srand( 0xABCABC );
+//    srand( 0xABCABC );
+    Aig_ManRandom(1);
     // set the pointer to the manager
     Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->pData = p;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 64222a47..9a500680 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -44,21 +44,20 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
-    Aig_Man_t * pNew = NULL, * pTemp;
+    Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
 
     // try the miter before solving
-    RetValue = Fra_FraigMiterStatus( p );
-    if ( RetValue == 0 || RetValue == 1 )
+    pNew = Aig_ManDup( p );
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
         goto finish;
 
     // prepare parameters
     memset( pPars, 0, sizeof(Fra_Ssw_t) );
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = fVeryVerbose;
-
-    pNew = Aig_ManDup( p );
     if ( fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
@@ -78,6 +77,9 @@ clk = clock();
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
     }
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
+        goto finish;
 
     // perform phase abstraction
 clk = clock();
@@ -150,6 +152,13 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    if ( pNew->nRegs == 0 )
+        RetValue = Fra_FraigCec( &pNew, 0 );
+
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
+        goto finish;
+
     // perform min-area retiming
     if ( fRetimeRegs && pNew->nRegs )
     {
@@ -262,9 +271,7 @@ PRT( "Time", clock() - clkTotal );
         assert( Aig_ManRegNum(pNew) > 0 );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-clk = clock();
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
-PRT( "Time", clock() - clk );
     }
 
 finish:
@@ -289,8 +296,7 @@ PRT( "Time", clock() - clkTotal );
         Ioa_WriteAiger( pNew, pFileName, 0, 0 );
         printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
     }
-    if ( pNew )
-        Aig_ManStop( pNew );
+    Aig_ManStop( pNew );
     return RetValue;
 }