summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaMf.c37
2 files changed, 23 insertions, 15 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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:55:59 +0000