luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc70831

This commit is contained in:
Alan Mishchenko 2007-08-31 08:01:00 -07:00
parent ddc6d1c168
commit 9f5ef0d618
15 changed files with 1464 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
abc.dsp
View File

@ -1542,6 +1542,22 @@ SOURCE=.\src\opt\lpk\lpk.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkAbcCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkAbcDsd.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkAbcFun.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkAbcMux.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkCore.c
# End Source File
# Begin Source File

23
src/aig/kit/kit.h
View File

@ -143,6 +143,7 @@ static inline int Kit_DsdLitRegular( int Lit ) { return Li
static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline int Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
static inline int Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit ) { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
@ -429,6 +430,25 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
}
static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
{
unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
if ( iVar < 5 )
{
for ( k = 0; k < nWords; k++ )
pTruth[k] = Masks[iVar];
}
else
{
for ( k = 0; k < nWords; k++ )
if ( k & (1 << (iVar-5)) )
pTruth[k] = ~(unsigned)0;
else
pTruth[k] = 0;
}
}
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
@ -453,12 +473,13 @@ extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars
extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
/*=== kitDsd.c ==========================================================*/
extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars );
extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes );
extern void Kit_DsdManFree( Kit_DsdMan_t * p );
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
extern void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
extern void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );

66
src/aig/kit/kitDsd.c
View File

@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
{
Kit_DsdMan_t * p;
p = ALLOC( Kit_DsdMan_t, 1 );
@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords );
p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
return p;
}
@ -461,6 +461,35 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
return pTruthRes;
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar )
{
unsigned * pTruthRes;
int i;
// if support is specified, request that supports are available
if ( uSupp )
Kit_DsdGetSupports( pNtk );
// assign elementary truth tables
assert( pNtk->nVars <= p->nVars );
for ( i = 0; i < (int)pNtk->nVars; i++ )
Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
// complement the truth table if needed
if ( Kit_DsdLitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
@ -476,7 +505,7 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
{
Kit_DsdMan_t * p;
unsigned * pTruth;
p = Kit_DsdManAlloc( pNtk->nVars );
p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
Kit_DsdManFree( p );
@ -499,6 +528,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
{
unsigned * pTruth;
Kit_DsdObj_t * pRoot;
Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar );
pRoot = Kit_DsdNtkRoot( pNtk );
pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+0 );
Kit_TruthCopy( pTruthCo, pTruth, p->nVars );
pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+1 );
Kit_TruthCopy( pTruthDec, pTruth, p->nVars );
}
/**Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
@ -1620,7 +1672,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
// printf( "Eval = %d.\n", Result );
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
@ -1645,7 +1697,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
{
Kit_DsdMan_t * p;
unsigned * pTruthC;
p = Kit_DsdManAlloc( nVars );
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
@ -1687,7 +1739,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
// Kit_DsdTestCofs( pNtk, pTruth );
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
@ -1757,7 +1809,7 @@ void Kit_DsdPrecompute4Vars()
printf( "\n" );
*/
p = Kit_DsdManAlloc( 4 );
p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
printf( "Verification failed.\n" );

18
src/base/abci/abc.c
View File

@ -5160,7 +5160,7 @@ usage:
Description []
SideEffects []
SeeAlso []
***********************************************************************/
@ -11278,6 +11278,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Only works for structrally hashed networks.\n" );
return 1;
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
}
// modify the current network
pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
if ( pNtkRes == NULL )
@ -11367,6 +11372,11 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
return 1;
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
}
if ( Abc_NtkIsStrash(pNtk) )
Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
@ -11457,7 +11467,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Only works for strashed networks.\n" );
return 1;
}
if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "Only works for sequential networks.\n" );
return 1;
}
Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
return 0;

4
src/base/abci/abcDar.c
View File

@ -834,8 +834,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
// conver to the manager
pMan = Abc_NtkToDar( pNtk, 0 );
// derive CNF
// pCnf = Cnf_Derive( pMan, 0 );
pCnf = Cnf_DeriveSimple( pMan, 0 );
pCnf = Cnf_Derive( pMan, 0 );
// pCnf = Cnf_DeriveSimple( pMan, 0 );
// convert into the SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );

6
src/base/abci/abcPart.c
View File

@ -366,7 +366,7 @@ timeFind += clock() - clk2;
Vec_PtrPush( vPartsAll, vPart );
Vec_PtrPush( vPartSuppsAll, vPartSupp );
Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) );
Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkCiNum(pNtk)) );
}
else
{
@ -380,7 +380,7 @@ timeFind += clock() - clk2;
// reinsert new support
Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) );
Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkCiNum(pNtk) );
}
}
@ -801,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
// perform partitioning
assert( Abc_NtkIsStrash(pNtk) );
// vParts = Abc_NtkPartitionNaive( pNtk, 20 );
vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 );
vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );

158
src/opt/lpk/lpkAbcCore.c Normal file
View File

@ -0,0 +1,158 @@
/**CFile****************************************************************
FileName [lpkAbcCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fast Boolean matching for LUT structures.]
Synopsis [The new core procedure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: lpkAbcCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Implements the function.]
Description [Returns the node implementing this function.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Lpk_FunImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
{
Abc_Obj_t * pObjNew;
int i;
pObjNew = Abc_NtkCreateNode( pNtk );
for ( i = 0; i < (int)p->nVars; i++ )
Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
Abc_ObjLevelNew( pObjNew );
// create the logic function
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
// allocate memory for the ISOP
Vec_Int_t * vCover = Vec_IntAlloc( 0 );
// transform truth table into the decomposition tree
Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover );
// derive the AIG for the decomposition tree
pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph );
Kit_GraphFree( pGraph );
Vec_IntFree( vCover );
}
return pObjNew;
}
/**Function*************************************************************
Synopsis [Implements the function.]
Description [Returns the node implementing this function.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Lpk_LptImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
{
Lpk_Fun_t * pFun;
Abc_Obj_t * pRes;
int i;
for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- )
{
pFun = Vec_PtrEntry( vLeaves, i );
pRes = Lpk_FunImplement( pNtk, vLeaves, pFun );
Vec_PtrWriteEntry( vLeaves, i, pRes );
Lpk_FunFree( pFun );
}
return pRes;
}
/**Function*************************************************************
Synopsis [Decomposes the function using recursive MUX decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_LpkDecompose_rec( Lpk_Fun_t * p )
{
Lpk_Fun_t * p2;
int VarPol;
assert( p->nAreaLim > 0 );
if ( p->nVars <= p->nLutK )
return 1;
// check if decomposition exists
VarPol = Lpk_FunAnalizeMux( p );
if ( VarPol == -1 )
return 0;
// split and call recursively
p2 = Lpk_FunSplitMux( p, VarPol );
if ( !Lpk_LpkDecompose_rec( p2 ) )
return 0;
return Lpk_LpkDecompose_rec( p );
}
/**Function*************************************************************
Synopsis [Decomposes the function using recursive MUX decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
{
Lpk_Fun_t * p;
Abc_Obj_t * pObjNew = NULL;
int i, nLeaves;
// create the starting function
nLeaves = Vec_PtrSize( vLeaves );
p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
Lpk_FunSuppMinimize( p );
// decompose the function
if ( Lpk_LpkDecompose_rec(p) )
pObjNew = Lpk_LptImplement( pNtk, vLeaves, nLeaves );
else
{
for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- )
Lpk_FunFree( Vec_PtrEntry(vLeaves, i) );
}
Vec_PtrShrink( vLeaves, nLeaves );
return pObjNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

395
src/opt/lpk/lpkAbcDsd.c Normal file
View File

@ -0,0 +1,395 @@
/**CFile****************************************************************
FileName [lpkAbcDsd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fast Boolean matching for LUT structures.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the variable whose cofs have min sum of supp sizes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
{
int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
VarBest = -1;
Lpk_SuppForEachVar( p->uSupp, Var )
{
nSuppMaxCur = 0;
nSuppTotalCur = 0;
for ( i = 0; i < nTruths; i++ )
{
Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
nSuppTotalCur += nSuppSize0 + nSuppSize1;
}
if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur ||
(nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) )
{
VarBest = Var;
nSuppMaxMin = nSuppMaxCur;
nSuppTotalMin = nSuppTotalCur;
}
}
// recompute cofactors for the best var
for ( i = 0; i < nTruths; i++ )
{
Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest );
Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest );
}
return VarBest;
}
/**Function*************************************************************
Synopsis [Recursively computes decomposable subsets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
{
unsigned i, iLitFanin, uSupport, uSuppCur;
Kit_DsdObj_t * pObj;
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return (1 << Kit_DsdLit2Var(iLit));
if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
{
unsigned uSupps[16], Limit, s;
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
uSupport |= uSupps[i];
}
// create all subsets, except empty and full
Limit = (1 << pObj->nFans) - 1;
for ( s = 1; s < Limit; s++ )
{
uSuppCur = 0;
for ( i = 0; i < pObj->nFans; i++ )
if ( s & (1 << i) )
uSuppCur |= uSupps[i];
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
assert( pObj->Type == KIT_DSD_PRIME );
// get the cumulative support of all fanins
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
uSupport |= uSuppCur;
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
/**Function*************************************************************
Synopsis [Computes the set of subsets of decomposable variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
{
Vec_Int_t * vSets;
unsigned uSupport, Entry;
int Number, i;
assert( p->nVars <= 16 );
vSets = Vec_IntAlloc( 100 );
Vec_IntPush( vSets, 0 );
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
return vSets;
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
{
uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
Vec_IntPush( vSets, uSupport );
return vSets;
}
uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets );
assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport );
// set the remaining variables
Vec_IntForEachEntry( vSets, Number, i )
{
Entry = Number;
Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
}
return vSets;
}
/**Function*************************************************************
Synopsis [Merges two bound sets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
{
Vec_Int_t * vSets;
int Entry0, Entry1, Entry;
int i, k;
vSets = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vSets0, Entry0, i )
Vec_IntForEachEntry( vSets1, Entry1, k )
{
Entry = Entry0 | Entry1;
if ( (Entry & (Entry >> 16)) )
continue;
Vec_IntPush( vSets, Entry );
}
return vSets;
}
/**Function*************************************************************
Synopsis [Allocates truth tables for cofactors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
{
int i;
assert( nCofDepth <= 4 );
ppTruths[0][0] = Lpk_FunTruth( p, 0 );
if ( nCofDepth >= 1 )
{
ppTruths[1][0] = Lpk_FunTruth( p, 1 );
ppTruths[1][1] = Lpk_FunTruth( p, 2 );
}
if ( nCofDepth >= 2 )
{
ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 );
for ( i = 1; i < 4; i++ )
ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i;
}
if ( nCofDepth >= 3 )
{
ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 );
for ( i = 1; i < 8; i++ )
ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i;
}
if ( nCofDepth >= 4 )
{
ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 );
for ( i = 1; i < 16; i++ )
ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i;
}
}
/**Function*************************************************************
Synopsis [Allocates truth tables for cofactors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
{
if ( nCofDepth >= 2 )
free( ppTruths[2][0] );
if ( nCofDepth >= 3 )
free( ppTruths[3][0] );
if ( nCofDepth >= 4 )
free( ppTruths[4][0] );
}
/**Function*************************************************************
Synopsis [Performs DSD-based decomposition of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth )
{
static Lpk_Res_t Res, * pRes = &Res;
unsigned * ppTruths[5][16];
Vec_Int_t * pvBSets[4][8];
Kit_DsdNtk_t * pNtkDec, * pTemp;
unsigned uBoundSet;
int i, k, nVarsBS, nVarsRem, Delay, Area;
Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
// find the best cofactors
memset( pRes, 0, sizeof(Lpk_Res_t) );
pRes->nCofVars = nCofDepth;
for ( i = 0; i < nCofDepth; i++ )
pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+1] );
// derive decomposed networks
for ( i = 0; i < (1<<nCofDepth); i++ )
{
pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars );
pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp );
pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth );
Kit_DsdNtkFree( pNtkDec );
}
// derive the set of feasible boundsets
for ( i = nCofDepth - 1; i >= 0; i-- )
for ( k = 0; k < (1<<i); k++ )
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] );
// compare the resulting boundsets
Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
{
if ( uBoundSet == 0 )
continue;
assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim )
continue;
if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
{
pRes->nBSVars = nVarsBS;
pRes->BSVars = uBoundSet;
pRes->nSuppSizeS = nVarsBS;
pRes->nSuppSizeL = nVarsRem;
pRes->DelayEst = Delay;
pRes->AreaEst = Area;
}
}
// free cofactor storage
Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
return pRes;
}
/**Function*************************************************************
Synopsis [Splits the function into two subfunctions using DSD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
{
Kit_DsdMan_t * pDsdMan;
Kit_DsdNtk_t * pNtkDec, * pTemp;
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
Lpk_Fun_t * pNew;
unsigned * ppTruths[5][16];
char pBSVars[5];
int i, k, nVars, nCofs;
// get the bound set variables
nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
// compute the cofactors
Lpk_FunAllocTruthTables( p, nCofVars, ppTruths );
for ( i = 0; i < nCofVars; i++ )
for ( k = 0; k < (1<<i); k++ )
{
Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->nVars, pCofVars[i] );
Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] );
}
// decompose each cofactor w.r.t. the bound set
nCofs = (1<<nCofVars);
pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 );
for ( k = 0; k < nCofs; k++ )
{
pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp );
Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
Kit_DsdNtkFree( pNtkDec );
}
Kit_DsdManFree( pDsdMan );
// compute the composition function
for ( i = nCofVars - 1; i >= 1; i-- )
for ( k = 0; k < (1<<i); k++ )
Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] );
// now the composition/decomposition functions are in pTruth0/pTruth1
// derive the new component
pNew = Lpk_FunDup( p, pTruth1 );
// update the old component
Kit_TruthCopy( pTruth, pTruth0, p->nVars );
p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
p->pFanins[pBSVars[0]] = pNew->Id;
p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
// support minimize both
Lpk_FunSuppMinimize( p );
Lpk_FunSuppMinimize( pNew );
// update delay and area requirements
pNew->nDelayLim = p->nDelayLim - 1;
pNew->nAreaLim = 1;
p->nAreaLim = p->nAreaLim - 1;
// free cofactor storage
Lpk_FunFreeTruthTables( p, nCofVars, ppTruths );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

204
src/opt/lpk/lpkAbcFun.c Normal file
View File

@ -0,0 +1,204 @@
/**CFile****************************************************************
FileName [lpkAbcFun.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fast Boolean matching for LUT structures.]
Synopsis [Procedures working on decomposed functions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: lpkAbcFun.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_FunAlloc( int nVars )
{
Lpk_Fun_t * p;
p = (Lpk_Fun_t *)malloc( sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
memset( p, 0, sizeof(Lpk_Fun_t) );
return p;
}
/**Function*************************************************************
Synopsis [Deletes the function]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunFree( Lpk_Fun_t * p )
{
free( p );
}
/**Function*************************************************************
Synopsis [Creates the starting function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
{
Lpk_Fun_t * p;
Abc_Obj_t * pNode;
int i;
p = Lpk_FunAlloc( Vec_PtrSize(vLeaves) );
p->Id = Vec_PtrSize(vLeaves);
p->vNodes = vLeaves;
p->nVars = Vec_PtrSize(vLeaves);
p->nLutK = nLutK;
p->nAreaLim = AreaLim;
p->nDelayLim = DelayLim;
p->uSupp = Kit_TruthSupport( pTruth, p->nVars );
Kit_TruthCopy( Lpk_FunTruth(p,0), pTruth, p->nVars );
Vec_PtrForEachEntry( vLeaves, pNode, i )
{
p->pFanins[i] = i;
p->pDelays[i] = pNode->Level;
}
Vec_PtrPush( p->vNodes, p );
return p;
}
/**Function*************************************************************
Synopsis [Creates the new function with the given truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
{
Lpk_Fun_t * pNew;
pNew = Lpk_FunAlloc( p->nVars );
pNew->Id = Vec_PtrSize(p->vNodes);
pNew->vNodes = p->vNodes;
pNew->nVars = p->nVars;
pNew->nLutK = p->nLutK;
pNew->nAreaLim = p->nAreaLim;
pNew->nDelayLim = p->nDelayLim;
pNew->uSupp = Kit_TruthSupport( pTruth, p->nVars );
Kit_TruthCopy( Lpk_FunTruth(pNew,0), pTruth, p->nVars );
memcpy( pNew->pFanins, p->pFanins, 16 );
memcpy( pNew->pDelays, p->pDelays, 16 );
Vec_PtrPush( p->vNodes, pNew );
return p;
}
/**Function*************************************************************
Synopsis [Minimizes support of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
{
int j, k, nVarsNew;
// compress the truth table
if ( p->uSupp == Kit_BitMask(p->nVars) )
return;
// minimize support
nVarsNew = Kit_WordCountOnes(p->uSupp);
Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
for ( j = k = 0; j < (int)p->nVars; j++ )
if ( p->uSupp & (1 << j) )
{
p->pFanins[k] = p->pFanins[j];
p->pDelays[k] = p->pDelays[j];
k++;
}
assert( k == nVarsNew );
p->nVars = k;
p->uSupp = Kit_BitMask(p->nVars);
}
/**Function*************************************************************
Synopsis [Get the delay of the bound set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_SuppDelay( unsigned uSupp, char * pDelays )
{
int Delay, Var;
Delay = 0;
Lpk_SuppForEachVar( uSupp, Var )
Delay = ABC_MAX( Delay, pDelays[Var] );
return Delay + 1;
}
/**Function*************************************************************
Synopsis [Converts support into variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_SuppToVars( unsigned uBoundSet, char * pVars )
{
int i, nVars = 0;
Lpk_SuppForEachVar( uBoundSet, i )
pVars[nVars++] = i;
return nVars;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

254
src/opt/lpk/lpkAbcMux.c Normal file
View File

@ -0,0 +1,254 @@
/**CFile****************************************************************
FileName [lpkAbcMux.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fast Boolean matching for LUT structures.]
Synopsis [Iterative MUX decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: lpkAbcMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes cofactors w.r.t. the given var.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar )
{
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar );
Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar );
}
/**Function*************************************************************
Synopsis [Computes cofactors w.r.t. each variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
{
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
int Var;
Lpk_SuppForEachVar( p->uSupp, Var )
{
Lpk_FunComputeCofs( p, Var );
puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
}
}
/**Function*************************************************************
Synopsis [Checks the possibility of MUX decomposition.]
Description [Returns the best variable to use for MUX decomposition.]
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_FunAnalizeMux( Lpk_Fun_t * p )
{
unsigned puSupps[32] = {0};
int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB;
int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest;
if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 )
return -1;
// get cofactor supports for each variable
Lpk_FunComputeCofSupps( p, puSupps );
// derive the delay and area of each MUX-decomposition
VarBest = -1;
Lpk_SuppForEachVar( p->uSupp, Var )
{
nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]);
nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]);
if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
{
// include cof var into 0-block
DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
Delay0 = ABC_MAX( DelayA, DelayB + 1 );
// include cof var into 1-block
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay1 = ABC_MAX( DelayA, DelayB + 1 );
// get the best delay
Delay = ABC_MIN( Delay0, Delay1 );
Area = 2;
Polarity = (int)(Delay1 == Delay);
}
else if ( nSuppSize0 <= (int)p->nLutK - 2 )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
Polarity = 0;
}
else if ( nSuppSize0 <= (int)p->nLutK )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
Polarity = 1;
}
else if ( nSuppSize1 <= (int)p->nLutK - 2 )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
Polarity = 1;
}
else if ( nSuppSize1 <= (int)p->nLutK )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
Polarity = 0;
}
else
{
// include cof var into 0-block
DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
Delay0 = ABC_MAX( DelayA, DelayB + 1 );
// include cof var into 1-block
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay1 = ABC_MAX( DelayA, DelayB + 1 );
// get the best delay
Delay = ABC_MIN( Delay0, Delay1 );
if ( Delay == Delay0 )
Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
else
Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
Polarity = (int)(Delay1 == Delay);
}
// find the best variable
if ( Delay > (int)p->nDelayLim )
continue;
if ( Area > (int)p->nAreaLim )
continue;
if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
{
VarBest = Var;
AreaBest = Area;
PolarityBest = Polarity;
nSuppSizeBest = nSuppSize0+nSuppSize1;
}
}
return (VarBest == -1)? -1 : (2*VarBest + Polarity);
}
/**Function*************************************************************
Synopsis [Transforms the function decomposed by the MUX decomposition.]
Description [Returns the best variable to use for MUX decomposition.]
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol )
{
Lpk_Fun_t * pNew;
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
int Var = VarPol / 2;
int Pol = VarPol % 2;
int iVarVac;
assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars );
assert( p->nAreaLim >= 2 );
Lpk_FunComputeCofs( p, Var );
if ( Pol == 0 )
{
// derive the new component
pNew = Lpk_FunDup( p, pTruth1 );
// update the old component
p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) );
assert( iVarVac < (int)p->nVars );
Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
// update the truth table
Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars );
p->pFanins[iVarVac] = pNew->Id;
p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
// support minimize both
Lpk_FunSuppMinimize( p );
Lpk_FunSuppMinimize( pNew );
// update delay and area requirements
pNew->nDelayLim = p->nDelayLim - 1;
if ( p->nVars <= p->nLutK )
{
pNew->nAreaLim = p->nAreaLim - 1;
p->nAreaLim = 1;
}
else if ( pNew->nVars <= pNew->nLutK )
{
pNew->nAreaLim = 1;
p->nAreaLim = p->nAreaLim - 1;
}
else if ( p->nVars < pNew->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
}
else // if ( pNew->nVars < p->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
}
}
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

90
src/opt/lpk/lpkCore.c
View File

@ -258,11 +258,6 @@ p->timeCuts += clock() - clk;
if ( p->pPars->fFirst && i == 1 )
break;
if ( p->pObj->Id == 8835 )
{
int x = 0;
}
// compute the truth table
clk = clock();
pTruth = Lpk_CutTruth( p, pCut );
@ -310,6 +305,91 @@ p->timeEval += clock() - clk;
return 1;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
{
static int Count = 0;
Vec_Ptr_t * vLeaves;
Abc_Obj_t * pObjNew;
Lpk_Cut_t * pCut;
unsigned * pTruth;
void * pDsd = NULL;
int i, k, clk;
// compute the cuts
clk = clock();
if ( !Lpk_NodeCuts( p ) )
{
p->timeCuts += clock() - clk;
return 0;
}
p->timeCuts += clock() - clk;
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
vLeaves = Vec_PtrAlloc( 32 );
// try the good cuts
p->nCutsTotal += p->nCuts;
p->nCutsUseful += p->nEvals;
for ( i = 0; i < p->nEvals; i++ )
{
// get the cut
pCut = p->pCuts + p->pEvals[i];
if ( p->pPars->fFirst && i == 1 )
break;
// collect nodes into the array
Vec_PtrClear( vLeaves );
for ( k = 0; k < (int)pCut->nLeaves; k++ )
Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) );
// compute the truth table
clk = clock();
pTruth = Lpk_CutTruth( p, pCut );
p->timeTruth += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
// char * pFileName;
int nSuppSize;
Kit_DsdNtk_t * pDsdNtk;
nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves );
// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves );
Kit_DsdPrint( stdout, pDsdNtk );
Kit_DsdNtkFree( pDsdNtk );
// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}
// update the network
clk = clock();
pObjNew = Lpk_LpkDecompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize,
(int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) );
p->timeEval += clock() - clk;
// perform replacement
if ( pObjNew )
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
}
Vec_PtrFree( vLeaves );
return 1;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one network.]

58
src/opt/lpk/lpkCut.c
View File

@ -410,14 +410,6 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
// initialize the set of leaves to the nodes in the cut
assert( p->nCuts < LPK_CUTS_MAX );
pCutNew = p->pCuts + p->nCuts;
/*
if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
{
int x = 0;
printf( "Start:\n" );
Lpk_NodePrintCut( p, pCut );
}
*/
pCutNew->nLeaves = 0;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
if ( pCut->pLeaves[i] != Node )
@ -443,47 +435,30 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1]
assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
}
/*
printf( " Trying cut: " );
Lpk_NodePrintCut( p, pCutNew, 1 );
printf( "\n" );
*/
// skip the contained cuts
Lpk_NodeCutSignature( pCutNew );
if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
return;
// update the set of internal nodes
assert( pCut->nNodes < LPK_SIZE_MAX );
memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
pCutNew->nNodes = pCut->nNodes;
pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
// add the marked node
pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
/*
if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
{
int x = 0;
printf( "Finish:\n" );
Lpk_NodePrintCut( p, pCutNew );
}
*/
pCutNew->nNodesDup = pCut->nNodesDup;
// check if the node is already there
for ( i = 0; i < (int)pCutNew->nNodes; i++ )
if ( pCutNew->pNodes[i] == Node )
break;
if ( i == (int)pCutNew->nNodes ) // new node
{
pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
pCutNew->nNodesDup += !Abc_NodeIsTravIdCurrent(pObj);
}
// the number of nodes does not exceed MFFC plus duplications
assert( pCutNew->nNodes <= p->nMffc + pCutNew->nNodesDup );
// add the cut to storage
assert( p->nCuts < LPK_CUTS_MAX );
p->nCuts++;
// assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
/*
printf( " Creating cut: " );
Lpk_NodePrintCut( p, pCutNew, 1 );
printf( "\n" );
*/
// if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) )
// printf( "Assertion in line 477 failed.\n" );
}
/**Function*************************************************************
@ -527,13 +502,6 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
// try to expand the fanins of this cut
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
if ( p->pObj->Id == 28 && i == 273 && k == 13 )
{
Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]);
int s = 0;
}
// create a new cut
Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
// quit if the number of cuts has exceeded the limit
@ -559,7 +527,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
continue;
// compute the minimum number of LUTs needed to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
pCut->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize );
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
if ( pCut->Weight <= 1.001 )
continue;

59
src/opt/lpk/lpkInt.h
View File

@ -117,6 +117,47 @@ struct Lpk_Man_t_
int timeTotal;
};
// preliminary decomposition result
typedef struct Lpk_Res_t_ Lpk_Res_t;
struct Lpk_Res_t_
{
int nBSVars;
unsigned BSVars;
int nCofVars;
char pCofVars[4];
int nSuppSizeS;
int nSuppSizeL;
int DelayEst;
int AreaEst;
};
// function to be decomposed
typedef struct Lpk_Fun_t_ Lpk_Fun_t;
struct Lpk_Fun_t_
{
Vec_Ptr_t * vNodes; // the array of all functions
unsigned int Id : 5; // the ID of this node
unsigned int nVars : 5; // the number of variables
unsigned int nLutK : 4; // the number of LUT inputs
unsigned int nAreaLim : 8; // the area limit (the largest allowed)
unsigned int nDelayLim : 10; // the delay limit (the largest allowed)
char pFanins[16]; // the fanins of this function
char pDelays[16]; // the delays of the inputs
unsigned uSupp; // the support of this component
unsigned pTruth[0]; // the truth table (contains room for three truth tables)
};
#define Lpk_SuppForEachVar( Supp, Var )\
for ( Var = 0; Var < 16; Var++ )\
if ( !(Supp & (1<<Var)) ) {} else
static inline int Lpk_LutNumVars( int nLutsLim, int nLutK ) { return nLutsLim * (nLutK - 1) + 1; }
static inline int Lpk_LutNumLuts( int nVarsMax, int nLutK ) { return (nVarsMax - 1) / (nLutK - 1) + (int)((nVarsMax - 1) % (nLutK - 1) > 0); }
static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num < 3 ); return p->pTruth + Kit_TruthWordNum(p->nVars) * Num; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -136,6 +177,24 @@ struct Lpk_Man_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== lpkAbcCore.c ============================================================*/
extern Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
/*=== lpkAbcFun.c ============================================================*/
extern Lpk_Fun_t * Lpk_FunAlloc( int nVars );
extern void Lpk_FunFree( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
extern Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth );
extern void Lpk_FunSuppMinimize( Lpk_Fun_t * p );
extern int Lpk_SuppDelay( unsigned uSupp, char * pDelays );
extern int Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
/*=== lpkAbcDsd.c ============================================================*/
extern Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth );
extern Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
/*=== lpkAbcMux.c ============================================================*/
extern int Lpk_FunAnalizeMux( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol );
/*=== lpkCut.c =========================================================*/
extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
extern int Lpk_NodeCuts( Lpk_Man_t * p );

2
src/opt/lpk/lpkMan.c
View File

@ -54,7 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
return p;
}

202
src/sat/bsat/satSolver.c
View File

@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satSolver.h"
//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
#define WATCHFLAG 1
//=================================================================================================
// Debug:
@ -90,9 +91,11 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
static clause* clause_from_lit2(lit l) { return (clause*)(unsigned long)l; }
static lit clause_read_lit2(clause* c) { return (lit)(unsigned long)c; }
//=================================================================================================
// Simple helpers:
@ -108,6 +111,15 @@ static inline void vecp_remove(vecp* v, void* e)
for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
vecp_resize(v,vecp_size(v)-1);
}
static inline void vecp_remove2(vecp* v, void* e)
{
void** ws = vecp_begin(v);
int j = 0;
for (; ws[j] != e ; j++);
assert(j < vecp_size(v));
for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2];
vecp_resize(v,vecp_size(v)-2);
}
//=================================================================================================
// Variable order functions:
@ -304,8 +316,26 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
//vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
//vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
if ( WATCHFLAG )
{
if ( size == 2 )
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit(begin[1]));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit(begin[0]));
}
else
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1]));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0]));
}
}
else
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
}
return c;
}
@ -321,8 +351,24 @@ static void clause_remove(sat_solver* s, clause* c)
//vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
assert(lits[0] < s->size*2);
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if ( WATCHFLAG )
{
if ( clause_size(c) == 2 )
{
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1]));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0]));
}
else
{
vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
}
}
else
{
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
}
if (clause_learnt(c)){
s->stats.learnts--;
@ -703,6 +749,31 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
}
void sat_solver_check(sat_solver* s)
{
int j, k;
lit Lit, First, *lits;
vecp* ws;
clause **begin, **end, **i;
for ( j = 0; j < s->size; j++ )
for ( k = 0; k < 2; k++ )
{
Lit = toLitCond( j, k );
ws = sat_solver_read_wlist(s,Lit);
begin = (clause**)vecp_begin(ws);
end = begin + vecp_size(ws);
for (i = begin; i < end; i++)
{
if (clause_is_lit(*i))
continue;
lits = clause_begin(*i);
First = clause_read_lit2(*(i+1));
assert( First == lits[0] || First == lits[1] );
i++;
}
}
}
clause* sat_solver_propagate(sat_solver* s)
{
lbool* values = s->assigns;
@ -716,15 +787,19 @@ clause* sat_solver_propagate(sat_solver* s)
clause **begin = (clause**)vecp_begin(ws);
clause **end = begin + vecp_size(ws);
clause **i, **j;
// sat_solver_check(s);
s->stats.propagations++;
s->simpdb_props--;
//printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
for (i = j = begin; i < end; ){
if (clause_is_lit(*i)){
for (i = j = begin; i < end; i++)
{
if (clause_is_lit(*i))
{
*j++ = *i;
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p)))
{
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
@ -733,13 +808,27 @@ clause* sat_solver_propagate(sat_solver* s)
while (i < end)
*j++ = *i++;
}
}else{
lit false_lit;
}
else
{
lit false_lit, first;
lbool sig;
if ( WATCHFLAG )
{
first = clause_read_lit2(*(i+1));
sig = !lit_sign(first); sig += sig - 1;
if (values[lit_var(first)] == sig)
{
*j++ = *i++;
*j++ = *i;
continue;
}
}
lits = clause_begin(*i);
// Make sure the false literal is data[1]:
// Make sure the false literal is in data[1]:
false_lit = lit_neg(p);
if (lits[0] == false_lit){
lits[0] = lits[1];
@ -748,35 +837,95 @@ clause* sat_solver_propagate(sat_solver* s)
assert(lits[1] == false_lit);
//printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig){
*j++ = *i;
}else{
if ( WATCHFLAG )
{
/*
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig)
{
*j++ = *i++;
*j++ = *i;
continue;
}
else
*/
{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
for (k = lits + 2; k < stop; k++){
// assert( lits[0] == first );
for (k = lits + 2; k < stop; k++)
{
lbool sig = lit_sign(*k); sig += sig - 1;
if (values[lit_var(*k)] != sig){
if (values[lit_var(*k)] != sig)
{
lits[1] = *k;
*k = false_lit;
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
goto next; }
// vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++);
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0]));
break;
}
}
if ( k < stop )
continue;
*j++ = *i;
// Clause is unit under assignment:
if (!enqueue(s,lits[0], *i)){
if (!enqueue(s,lits[0], *i))
{
confl = *i++;
*j++ = clause_from_lit2(lits[0]); i++; //
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
else
{
*j++ = clause_from_lit2(lits[0]); i++; //
}
}
}
else
{
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig)
{
*j++ = *i;
}
else
{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
for (k = lits + 2; k < stop; k++)
{
lbool sig = lit_sign(*k); sig += sig - 1;
if (values[lit_var(*k)] != sig)
{
lits[1] = *k;
*k = false_lit;
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
break;
}
}
if ( k < stop )
continue;
*j++ = *i;
// Clause is unit under assignment:
if (!enqueue(s,lits[0], *i))
{
confl = *i++;
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
}
}
}
next:
i++;
}
s->stats.inspects += j - (clause**)vecp_begin(ws);
@ -795,7 +944,7 @@ void sat_solver_reducedb(sat_solver* s)
double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)vecp_begin(&s->learnts);
clause** reasons = s->reasons;
//printf( "Trying to reduce DB\n" );
sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
@ -888,8 +1037,10 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
}
if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
{
// Simplify the set of problem clauses:
sat_solver_simplify(s);
}
if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
@ -1120,6 +1271,7 @@ bool sat_solver_simplify(sat_solver* s)
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
//printf( "Trying to simplify\n" );
reasons = s->reasons;
for (type = 0; type < 2; type++){