Version abc80519

3 files changed, 57 insertions, 137 deletions

diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index e5222e2e..c957a751 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -533,7 +533,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Fra_Lcr_t * p;
     Fra_Sml_t * pSml;
     Fra_Man_t * pTemp;
-    Aig_Man_t * pAigPart, * pAigNew = NULL;
+    Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
     Vec_Int_t * vPart;
     int i, nIter, timeSim, clk = clock(), clk2, clk3;
     int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
@@ -623,9 +623,9 @@ clk2 = clock();
             pAigPart = Fra_LcrCreatePart( p, vPart );
 p->timeTrav += clock() - clk2;
 clk2 = clock();
-            pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
+            pAigTemp  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
 p->timeFraig += clock() - clk2;
-            Vec_PtrPush( p->vFraigs, pAigNew );
+            Vec_PtrPush( p->vFraigs, pAigTemp );
             Aig_ManStop( pAigPart );
         }
         Fra_ClassNodesUnmark( p );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 2ca99cbf..4528b9c4 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -57,7 +57,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fVeryVerbose      =   0;  // enables very verbose reporting  
     p->TimeLimit         =   0;  // enables the timeout
     // internal parameters
-    p->fReportSolution   =   0;  // enables specialized format for reporting solution
+    p->fReportSolution   =   1;  // enables specialized format for reporting solution
 }
 
 /**Function*************************************************************
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 8974ecb9..4250ca79 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -195,169 +195,89 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManHaigVerifyComb( Aig_Man_t * pHaig )
+int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
 {
     int nBTLimit = 0;
-    Vec_Ptr_t * vResult;
-    Aig_Man_t * pFrames;
+    Aig_Man_t * pFrames, * pTemp;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
     Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue, RetValue1, RetValue2, Counter, Lits[2];
+    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
     int clk = clock();
 
-    printf( "Filtering combinational cases:\n" );
-//    return;
+    nOvers = Aig_ManMapHaigNodes( pHaig );
 
     // create time frames with speculative reduction and convert them into CNF
 clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, 1 );
-
-    // collect the HAIG nodes that were used to create spec miters
-    vResult = Vec_PtrAlloc( Aig_ManPoNum(pFrames)/2 );
-    Aig_ManForEachPo( pFrames, pObj1, i )
-    {
-        pObj2 = Aig_ManPo( pFrames, ++i );
-        Vec_PtrPush( vResult, pObj1->pData );
-    }
+    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+    Aig_ManCleanMarkA( pHaig );
 
     printf( "Frames:     " );
     Aig_ManPrintStats( pFrames );
 
-//    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
-//    Aig_ManStop( pTemp );
+    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
+    Aig_ManStop( pTemp );
 
-    printf( "Frames:     " );
+    printf( "Frames synt:" );
     Aig_ManPrintStats( pFrames );
 
-    printf( "Additional frames stats: Assumptions = %d. Asserts = %d. Pairs = %d.\n", 
-        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2 );
+    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
+        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
 //    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
     pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
 
-//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
-//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-//    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
-//    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
-    // create the SAT solver to be used for this problem
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return;
-    }
-PRT( "Preparation", clock() - clk );
-
-
-    // check in the second timeframe
-clk = clock();
-    Counter = 0;
-    printf( "Started solving ...\r" );
-    Aig_ManForEachPo( pFrames, pObj1, i )
+/*
+    // print the statistic into a file
     {
-        pObj2 = Aig_ManPo( pFrames, ++i );
-        assert( pObj1->fPhase == pObj2->fPhase );
-
-        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-
-        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
-        if ( RetValue1 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-            assert( RetValue );
-        }
-
-        Lits[0]++;
-        Lits[1]--;
-
-        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)10, (sint64)0, (sint64)0, (sint64)0 );
-        if ( RetValue2 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-            assert( RetValue );
-        }
-
-        if ( RetValue1 != l_False || RetValue2 != l_False )
-        {
-            Counter++;
-        }
-        else
-        {
-            pObj1 = Vec_PtrEntry( vResult, i/2 );
-            assert( pObj1->pHaig != NULL );
-            pObj1->fMarkA = 1;
-        }
-        
-        if ( i % 50 == 1 )
-            printf( "Solving assertion %6d out of %6d.\r", 
-                (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2, 
-                pFrames->nAsserts/2 );
-//        if ( nClasses == 1000 )
-//            break;
-    }
-    printf( "                                                          \r" );
-PRT( "Solving    ", clock() - clk );
-    if ( Counter )
-        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
-    else
-        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
+        FILE * pTable;
+        Aig_Man_t * pTemp, * pHaig2;
 
-    // clean up
-    Aig_ManStop( pFrames );
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    Vec_PtrFree( vResult );
-}
- 
-/**Function*************************************************************
+        pHaig2 = pAig->pManHaig; 
+        pAig->pManHaig = NULL;
+        pTemp = Aig_ManDupDfs( pAig );
+        pAig->pManHaig = pHaig2;
 
-  Synopsis    []
+        Aig_ManSeqCleanup( pTemp );
 
-  Description []
-               
-  SideEffects []
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pName );
+        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
+        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
 
-  SeeAlso     []
+        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
 
-***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
-{
-    int nBTLimit = 0;
-    Aig_Man_t * pFrames, * pTemp;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    int clk = clock();
+        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
 
-    nOvers = Aig_ManMapHaigNodes( pHaig );
+        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
 
-//    if ( nFrames == 2 )
-//        Aig_ManHaigVerifyComb( pHaig );
 
-    // create time frames with speculative reduction and convert them into CNF
-clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
-    Aig_ManCleanMarkA( pHaig );
+        pTable = fopen( "stats2.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pSpec );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
 
-    printf( "Frames:     " );
-    Aig_ManPrintStats( pFrames );
+        fprintf( pTable, "%d ", pCnf->nVars );
+        fprintf( pTable, "%d ", pCnf->nClauses );
+        fprintf( pTable, "%d ", pCnf->nLiterals );
 
-    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
-    Aig_ManStop( pTemp );
+        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
 
-    printf( "Frames synt:" );
-    Aig_ManPrintStats( pFrames );
+        Aig_ManStop( pTemp );
+    }
+*/
 
-    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
-        Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
-//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
-    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
 
 //    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
@@ -478,7 +398,7 @@ PRT( "Solving    ", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
 {
     int nBTLimit = 0;
     Cnf_Dat_t * pCnf;
@@ -774,12 +694,12 @@ PRT( "Synthesis time ", clock() - clk );
 
     if ( fUseCnf )
     {
-        if ( !Aig_ManHaigVerify2( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+        if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
             printf( "Constructing SAT solver has failed.\n" );         
     }
     else
     {
-        if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fSeqHaig ) )
+        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
             printf( "Constructing SAT solver has failed.\n" );         
     }