From 755935a6df4c84377aff1c67a5d802062cf925e6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 May 2013 13:34:22 -0700 Subject: Added switch -M to set max size of two-cube divisors to extract (often helps both runtime and quality). --- src/opt/fxu/fxu.c | 10 +++++----- src/opt/fxu/fxu.h | 3 ++- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'src/opt') diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index 0095abf9..2b078120 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -83,7 +83,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ); if ( pData->fVerbose ) printf( "Div %5d : Best single = %5d.%s", Counter++, Weight1, fScrollLines?"\n":"\r" ); - if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) ) + if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) ) Fxu_UpdateSingle( p ); else break; @@ -98,7 +98,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) printf( "Div %5d : Best double = %5d.%s", Counter++, Weight2, fScrollLines?"\n":"\r" ); - if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) ) + if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) ) Fxu_UpdateDouble( p ); else break; @@ -119,14 +119,14 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) if ( Weight1 >= Weight2 ) { - if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) ) + if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) ) Fxu_UpdateSingle( p ); else break; } else { - if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) ) + if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) ) Fxu_UpdateDouble( p ); else break; @@ -148,7 +148,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.%s", Counter++, Weight2, Weight1, Weight3, fScrollLines?"\n":"\r" ); - if ( Weight3 > pData->WeightMax || (Weight3 == 0 && pData->fUse0) ) + if ( Weight3 > pData->WeightMin || (Weight3 == 0 && pData->fUse0) ) Fxu_Update( p, pSingle, pDouble ); else break; diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index 3c6384dc..e8ef6586 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -53,7 +53,8 @@ struct FxuDataStruct int nNodesExt; // the number of divisors to extract int nSingleMax; // the max number of single-cube divisors to consider int nPairsMax; // the max number of double-cube divisors to consider - int WeightMax; // the max weight of a divisor to extract + int WeightMin; // the min weight of a divisor to extract + int LitCountMax; // the max literal count of a divisor to consider // the input information Vec_Ptr_t * vSops; // the SOPs for each node in the network Vec_Ptr_t * vFanins; // the fanins of each node in the network -- cgit v1.2.3