summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp16
-rw-r--r--src/aig/kit/kit.h23
-rw-r--r--src/aig/kit/kitDsd.c66
-rw-r--r--src/base/abci/abc.c18
-rw-r--r--src/base/abci/abcDar.c4
-rw-r--r--src/base/abci/abcPart.c6
-rw-r--r--src/opt/lpk/lpkAbcCore.c158
-rw-r--r--src/opt/lpk/lpkAbcDsd.c395
-rw-r--r--src/opt/lpk/lpkAbcFun.c204
-rw-r--r--src/opt/lpk/lpkAbcMux.c254
-rw-r--r--src/opt/lpk/lpkCore.c90
-rw-r--r--src/opt/lpk/lpkCut.c58
-rw-r--r--src/opt/lpk/lpkInt.h59
-rw-r--r--src/opt/lpk/lpkMan.c2
-rw-r--r--src/sat/bsat/satSolver.c202
15 files changed, 1464 insertions, 91 deletions
diff --git a/abc.dsp b/abc.dsp
index c4f6e05f..a38cb10f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -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
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2f7bbef4..c08bead2 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -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 );
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 06377cba..354ab6ef 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -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;
}
@@ -472,11 +472,40 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
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.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
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 );
@@ -501,6 +530,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru
/**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.]
Description []
@@ -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" );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3902830d..f740ee18 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 40a52ce8..f8f7d20e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -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 );
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index f0989b23..23e9d28d 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -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" );
diff --git a/src/opt/lpk/lpkAbcCore.c b/src/opt/lpk/lpkAbcCore.c
new file mode 100644
index 00000000..53b2668d
--- /dev/null
+++ b/src/opt/lpk/lpkAbcCore.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
new file mode 100644
index 00000000..893844e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcFun.c b/src/opt/lpk/lpkAbcFun.c
new file mode 100644
index 00000000..f7d2f402
--- /dev/null
+++ b/src/opt/lpk/lpkAbcFun.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
new file mode 100644
index 00000000..1525a7e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcMux.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index a1da45b5..2158f8f7 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -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 );
@@ -312,6 +307,91 @@ p->timeEval += clock() - clk;
/**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.]
Description []
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 27a0317c..d0908a6a 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -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;
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 683e7b92..d04032ef 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -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 );
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index c11a0a33..5be198d7 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -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;
}
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 512c5751..19ff6f8b 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -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++){
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 00:33:01 +0000