summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-09-09 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-09-09 08:01:00 -0700
commita30c08bbe55d624ec3269577bf16f2f09215be12 (patch)
treef0670e8bef0dfb14d53debd37b431d6863b38cad /src/aig/fra
parent092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (diff)
downloadabc-a30c08bbe55d624ec3269577bf16f2f09215be12.tar.gz
abc-a30c08bbe55d624ec3269577bf16f2f09215be12.tar.bz2
abc-a30c08bbe55d624ec3269577bf16f2f09215be12.zip
Version abc80909
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fraClass.c1
-rw-r--r--src/aig/fra/fraInd.c6
-rw-r--r--src/aig/fra/fraLcr.c3
3 files changed, 7 insertions, 3 deletions
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