From a30c08bbe55d624ec3269577bf16f2f09215be12 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 9 Sep 2008 08:01:00 -0700
Subject: Version abc80909

---
 src/aig/fra/fraClass.c | 1 +
 src/aig/fra/fraInd.c   | 6 +++---
 src/aig/fra/fraLcr.c   | 3 +++
 3 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'src/aig/fra')

diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 442cf80e..064d2b9c 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -378,6 +378,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
     free( ppNexts );
     // now it is time to refine the classes
     Fra_ClassesRefine( p );
+//    Fra_ClassesPrint( p, 0 );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 76c7abad..ce9ec69b 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -568,7 +568,7 @@ p->timeTrav += clock() - clk2;
             Fra_OneHotAssume( p, p->vOneHots );
 //        if ( p->pManAig->vOnehots )
 //            Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
-
+ 
         // report the intermediate results
         if ( pPars->fVerbose )
         {
@@ -580,7 +580,6 @@ p->timeTrav += clock() - clk2;
             if ( p->pPars->fUse1Hot )
                 printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
             printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
-            PRT( "T", clock() - clk3 );
 //            printf( "\n" );
         } 
 
@@ -593,12 +592,13 @@ clk2 = clock();
         Fra_FraigSweep( p );
         if ( pPars->fVerbose )
         {
-//            PRT( "t", clock() - clk2 ); 
+            PRT( "T", clock() - clk3 );
         } 
 
 //        Sat_SolverPrintStats( stdout, p->pSat );
         // remove FRAIG and SAT solver
         Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
+//        printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
         sat_solver_delete( p->pSat );  p->pSat = NULL; 
         memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
 //        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 92e0d94b..4b2383aa 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -629,6 +629,9 @@ clk2 = clock();
 p->timeFraig += clock() - clk2;
             Vec_PtrPush( p->vFraigs, pAigTemp );
             Aig_ManStop( pAigPart );
+
+//intf( "finished part %d (out of %d)\n", i, Vec_PtrSize(p->vParts) );
+
         }
         Fra_ClassNodesUnmark( p );
         // report the intermediate results
-- 
cgit v1.2.3