summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaMf.c37
-rw-r--r--src/base/abci/abc.c6
-rw-r--r--src/bool/kit/kit.h1
-rw-r--r--src/bool/kit/kitGraph.c25
5 files changed, 54 insertions, 16 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 7f6bbea6..acabe8e0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -339,6 +339,7 @@ struct Jf_Par_t_
int fCutMin;
int fFuncDsd;
int fGenCnf;
+ int fGenLit;
int fCnfObjIds;
int fAddOrCla;
int fCnfMapping;
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index 7e699d9b..4bd08dcf 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -24,6 +24,7 @@
#include "misc/extra/extra.h"
#include "sat/cnf/cnf.h"
#include "opt/dau/dau.h"
+#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@@ -557,8 +558,8 @@ static inline int Mf_CutComputeTruth6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t
assert( (int)(t & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, &t);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
- if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) )
- Vec_IntPush( &p->vCnfSizes, Abc_Tt6CnfSize(t, pCutR->nLeaves) );
+ if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) )
+ Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt6CnfSize(t, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)&t, pCutR->nLeaves, &p->vCnfMem) );
// p->nCutMux += Mf_ManTtIsMux( t );
assert( (int)pCutR->nLeaves <= nOldSupp );
// Mf_ManTruthCanonicize( &t, pCutR->nLeaves );
@@ -588,8 +589,8 @@ static inline int Mf_CutComputeTruth( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t *
//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
- if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
- Vec_IntPush( &p->vCnfSizes, Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) );
+ if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
+ Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)uTruth, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
@@ -612,8 +613,8 @@ static inline int Mf_CutComputeTruthMux6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut
assert( (int)(t & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, &t);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
- if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) )
- Vec_IntPush( &p->vCnfSizes, Abc_Tt6CnfSize(t, pCutR->nLeaves) );
+ if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) )
+ Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt6CnfSize(t, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)&t, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
@@ -642,8 +643,8 @@ static inline int Mf_CutComputeTruthMux( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_
assert( (uTruth[0] & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
- if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
- Vec_IntPush( &p->vCnfSizes, Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) );
+ if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
+ Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)uTruth, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
@@ -699,6 +700,8 @@ static inline void Mf_CutPrint( Mf_Man_t * p, Mf_Cut_t * pCut )
{
if ( p->pPars->fGenCnf )
printf( "CNF = %2d ", Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(pCut->iFunc)) );
+ if ( p->pPars->fGenLit )
+ printf( "Lit = %2d ", Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(pCut->iFunc)) );
Dau_DsdPrintFromTruth( Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc)), pCut->nLeaves );
}
else
@@ -998,7 +1001,7 @@ static inline int Mf_CutArea( Mf_Man_t * p, int nLeaves, int iFunc )
{
if ( nLeaves < 2 )
return 0;
- if ( p->pPars->fGenCnf )
+ if ( p->pPars->fGenCnf || p->pPars->fGenLit )
return Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(iFunc));
if ( p->pPars->fOptEdge )
return nLeaves + p->pPars->nAreaTuner;
@@ -1202,7 +1205,7 @@ int Mf_ManSetMapRefs( Mf_Man_t * p )
Mf_ObjMapRefInc( p, pCut[k] );
p->pPars->Edge += Mf_CutSize(pCut);
p->pPars->Area++;
- if ( p->pPars->fGenCnf )
+ if ( p->pPars->fGenCnf || p->pPars->fGenLit )
p->pPars->Clause += Mf_CutArea(p, Mf_CutSize(pCut), Mf_CutFunc(pCut));
}
// blend references
@@ -1394,7 +1397,7 @@ Mf_Man_t * Mf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
p->pLfObjs = ABC_CALLOC( Mf_Obj_t, Gia_ManObjNum(pGia) );
p->iCur = 2;
Vec_PtrGrow( &p->vPages, 256 );
- if ( pPars->fGenCnf )
+ if ( pPars->fGenCnf || pPars->fGenLit )
{
Vec_IntGrow( &p->vCnfSizes, 10000 );
Vec_IntPush( &p->vCnfSizes, 1 );
@@ -1410,7 +1413,7 @@ Mf_Man_t * Mf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
void Mf_ManFree( Mf_Man_t * p )
{
- assert( !p->pPars->fGenCnf || Vec_IntSize(&p->vCnfSizes) == Vec_MemEntryNum(p->vTtMem) );
+ assert( !p->pPars->fGenCnf || !p->pPars->fGenLit || Vec_IntSize(&p->vCnfSizes) == Vec_MemEntryNum(p->vTtMem) );
if ( p->pPars->fCutMin )
Vec_MemHashFree( p->vTtMem );
if ( p->pPars->fCutMin )
@@ -1453,6 +1456,7 @@ void Mf_ManSetDefaultPars( Jf_Par_t * pPars )
pPars->fCoarsen = 1;
pPars->fCutMin = 0;
pPars->fGenCnf = 0;
+ pPars->fGenLit = 0;
pPars->fPureAig = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
@@ -1469,6 +1473,8 @@ void Mf_ManPrintStats( Mf_Man_t * p, char * pTitle )
printf( "Edge =%9lu ", (long)p->pPars->Edge );
if ( p->pPars->fGenCnf )
printf( "CNF =%9lu ", (long)p->pPars->Clause );
+ if ( p->pPars->fGenLit )
+ printf( "FFL =%9lu ", (long)p->pPars->Clause );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
fflush( stdout );
}
@@ -1483,6 +1489,7 @@ void Mf_ManPrintInit( Mf_Man_t * p )
printf( "CutMin = %d ", p->pPars->fCutMin );
printf( "Coarse = %d ", p->pPars->fCoarsen );
printf( "CNF = %d ", p->pPars->fGenCnf );
+ printf( "FFL = %d ", p->pPars->fGenLit );
printf( "\n" );
printf( "Computing cuts...\r" );
fflush( stdout );
@@ -1656,7 +1663,7 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
{
Mf_Man_t * p;
Gia_Man_t * pNew, * pCls;
- if ( pPars->fGenCnf )
+ if ( pPars->fGenCnf || pPars->fGenLit )
pPars->fCutMin = 1;
if ( Gia_ManHasChoices(pGia) )
pPars->fCutMin = 1, pPars->fCoarsen = 0;
@@ -1685,8 +1692,8 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
pNew = Mf_ManDeriveMapping( p );
if ( p->pPars->fGenCnf )
pGia->pData = Mf_ManDeriveCnf( p, p->pPars->fCnfObjIds, p->pPars->fAddOrCla );
-// if ( p->pPars->fGenCnf )
-// Mf_ManProfileTruths( p );
+ //if ( p->pPars->fGenCnf || p->pPars->fGenLit )
+ // Mf_ManProfileTruths( p );
Gia_ManMappingVerify( pNew );
Mf_ManPrintQuit( p, pNew );
Mf_ManFree( p );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ab8e3659..71026b28 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -39541,7 +39541,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pNew; int c;
Mf_ManSetDefaultPars( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmcgvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmclgvwh" ) ) != EOF )
{
switch ( c )
{
@@ -39665,6 +39665,9 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fGenCnf ^= 1;
break;
+ case 'l':
+ pPars->fGenLit ^= 1;
+ break;
case 'g':
pPars->fPureAig ^= 1;
break;
@@ -39717,6 +39720,7 @@ usage:
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggles mapping for literals [default = %s]\n", pPars->fGenLit? "yes": "no" );
Abc_Print( -2, "\t-g : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index 47f06403..5436956a 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -568,6 +568,7 @@ extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
extern Kit_Graph_t * Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
+extern int Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
/*=== kitHop.c ==========================================================*/
//extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
//extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
diff --git a/src/bool/kit/kitGraph.c b/src/bool/kit/kitGraph.c
index 0e548575..9d7189a2 100644
--- a/src/bool/kit/kitGraph.c
+++ b/src/bool/kit/kitGraph.c
@@ -496,6 +496,31 @@ int * Kit_TruthTest( char * pFileName )
return pResult;
}
+/**Function*************************************************************
+
+ Synopsis [Derives the factored form from the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
+{
+ Kit_Graph_t * pGraph;
+ int RetValue, nLits;
+ RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 );
+ if ( RetValue == -1 || Vec_IntSize(vMemory) > (1<<16) )
+ return -1;
+ assert( RetValue == 0 || RetValue == 1 );
+ pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
+ nLits = 1 + Kit_GraphNodeNum( pGraph );
+ Kit_GraphFree( pGraph );
+ return nLits;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-28 21:43:56 +0000