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

Experiments with don't-cares.

This commit is contained in:
Alan Mishchenko 2017-03-26 20:32:46 -07:00
parent d0ea4853ec
commit 036be3a541
11 changed files with 853 additions and 305 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -1079,6 +1079,10 @@ SOURCE=.\src\base\acb\acbMfs.c
# End Source File
# Begin Source File
SOURCE=.\src\base\acb\acbPar.h
# End Source File
# Begin Source File
SOURCE=.\src\base\acb\acbUtil.c
# End Source File
# End Group

2
src/base/abc/abcSop.c
View File

@ -378,6 +378,8 @@ char * Abc_SopCreateFromTruth( Mem_Flex_t * pMan, int nVars, unsigned * pTruth )
{
char * pSop, * pCube;
int nMints, Counter, i, k;
if ( nVars == 0 )
return pTruth[0] ? Abc_SopCreateConst1(pMan) : Abc_SopCreateConst0(pMan);
// count the number of true minterms
Counter = 0;
nMints = (1 << nVars);

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

@ -62,6 +62,8 @@
#include "map/mpm/mpm.h"
#include "opt/fret/fretime.h"
#include "opt/nwk/nwkMerge.h"
#include "base/acb/acbPar.h"
#ifndef _WIN32
#include <unistd.h>
@ -121,6 +123,7 @@ static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGlitch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -777,6 +780,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfse", Abc_CommandMfse, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "glitch", Abc_CommandGlitch, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
@ -5654,6 +5658,137 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Acb_Par_t Pars, * pPars = &Pars; int c;
Acb_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MDOFLCavwh" ) ) != EOF )
{
switch ( c )
{
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTabooMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTabooMax < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nDivMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nDivMax < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTfoLevMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFanoutMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < -ABC_INFINITY || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
Abc_Print( -1, "This command can only be applied to a logic network.\n" );
return 1;
}
return 0;
usage:
Abc_Print( -2, "usage: mfse [-MDOFLC <num>] [-avwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-M <num> : the max number of fanin nodes to skip (num >= 1) [default = %d]\n", pPars->nTabooMax );
Abc_Print( -2, "\t-D <num> : the max number of divisors [default = %d]\n", pPars->nDivMax );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-a : toggle minimizing area [default = %s]\n", pPars->fArea? "area": "delay" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************

118
src/base/acb/acb.h
View File

@ -244,6 +244,7 @@ static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { r
static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; }
static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; }
static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); }
static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); }
static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; }
static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; }
@ -251,6 +252,7 @@ static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { a
static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntGetEntry(&p->vObjFunc, i); }
static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntGetEntry(&p->vObjWeight, i); }
static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdGetEntry(&p->vObjTruth, i); }
static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); }
static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntGetEntry(&p->vObjName, i); }
static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); }
static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0; }
@ -397,6 +399,16 @@ static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // shoul
assert( pFanins[ 1 + pFanins[0] ] == -1 );
pFanins[ 1 + pFanins[0] ] = iNtk;
}
static inline void Acb_ObjRemoveFanins( Acb_Ntk_t * p, int iObj )
{
int i, * pFanins = Acb_ObjFanins( p, iObj );
for ( i = 1; i <= pFanins[0]; i++ )
{
assert( pFanins[i] > 0 );
pFanins[i] = -1;
}
pFanins[0] = 0;
}
static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, int nFons )
{
int i, nFansReal, CioId = -1, iObj = Vec_StrSize(&p->vObjType);
@ -925,110 +937,10 @@ static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose
}
/**Function*************************************************************
Synopsis [Name handling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
/*
static inline void Acb_NtkAddMissingFonNames( Acb_Ntk_t * p, char * pPref )
{
int iFon, NameId, Index;
// populate map
Acb_ManCleanMap( p->pDesign );
Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
if ( NameId )
Acb_ManSetMap( p->pDesign, NameId, iFon );
// check remaining ones
Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
{
if ( NameId )
continue;
NameId = Acb_NtkNewStrId(p, "%s%d", pPref, iFon);
for ( Index = 1; Acb_ManGetMap(p->pDesign, NameId); Index++ )
NameId = Acb_NtkNewStrId(p, "%s%d_%d", pPref, iFon, Index);
Acb_FonSetName( p, iFon, NameId );
Acb_ManSetMap( p->pDesign, NameId, iFon );
}
}
static inline void Acb_NtkCreateFonNames( Acb_Ntk_t * p, char * pPref )
{
int i, iObj, iFon;//, NameId;
Acb_NtkCleanFonNames( p );
Acb_NtkForEachPiFon( p, iObj, iFon, i )
if ( !Acb_FonName(p, iFon) )
Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
Acb_NtkForEachPoDriverFon( p, iObj, iFon, i )
if ( Acb_FonIsReal(iFon) && !Acb_FonName(p, iFon) )
Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
// Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
// if ( NameId == 0 )
// Vec_IntWriteEntry( &p->vFonName, iFon, Acb_NtkNewStrId(p, "%s%d", pPref, iFon) );
Acb_NtkAddMissingFonNames( p, pPref );
}
static inline void Acb_NtkMissingFonNames( Acb_Ntk_t * p, char * pPref )
{
int i, iObj, iFon;//, NameId;
Acb_NtkForEachPiFon( p, iObj, iFon, i )
if ( !Acb_FonName(p, iFon) )
Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
Acb_NtkForEachPoDriverFon( p, iObj, iFon, i )
if ( Acb_FonIsReal(iFon) && !Acb_FonName(p, iFon) )
Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
// Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
// if ( NameId == 0 )
// Acb_FonSetName( p, iFon, Acb_NtkNewStrId(p, "%s%d", pPref, iFon) );
Acb_NtkAddMissingFonNames( p, pPref );
}
*/
/*=== acbBlast.c =============================================================*/
extern Gia_Man_t * Acb_ManBlast( Acb_Man_t * p, int fBarBufs, int fSeq, int fVerbose );
extern Acb_Man_t * Acb_ManInsertGia( Acb_Man_t * p, Gia_Man_t * pGia );
extern Acb_Man_t * Acb_ManInsertAbc( Acb_Man_t * p, void * pAbc );
/*=== acbCba.c ===============================================================*/
extern Acb_Man_t * Acb_ManReadCba( char * pFileName );
extern void Acb_ManWriteCba( char * pFileName, Acb_Man_t * p );
/*=== acbCom.c ===============================================================*/
/*=== acbNtk.c ===============================================================*/
extern void Acb_NtkPrintStatsFull( Acb_Ntk_t * p, int fDistrib, int fVerbose );
extern void Acb_NtkPrintNodes( Acb_Ntk_t * p, int Type );
extern void Acb_NtkPrintDistribOld( Acb_Ntk_t * p );
extern void Acb_ManPrintDistrib( Acb_Man_t * p );
//extern void Acb_ManPrepareTypeNames( Acb_Man_t * p );
extern void Acb_NtkObjOrder( Acb_Ntk_t * p, Vec_Int_t * vObjs, Vec_Int_t * vNameIds );
extern int Acb_NtkCiFonNum( Acb_Ntk_t * p );
extern int Acb_NtkCoFinNum( Acb_Ntk_t * p );
extern int Acb_NtkCheckComboLoop( Acb_Ntk_t * p );
extern int Acb_ManIsTopoOrder( Acb_Man_t * p );
extern Vec_Int_t * Acb_NtkCollectDfs( Acb_Ntk_t * p );
extern Acb_Man_t * Acb_ManCollapse( Acb_Man_t * p );
extern Acb_Man_t * Acb_ManExtractGroup( Acb_Man_t * p, Vec_Int_t * vObjs );
extern Acb_Man_t * Acb_ManDeriveFromGia( Acb_Man_t * p, Gia_Man_t * pGia, int fUseXor );
extern Acb_Man_t * Acb_ManInsertGroup( Acb_Man_t * p, Vec_Int_t * vObjs, Acb_Ntk_t * pSyn );
/*=== acbReadBlif.c ==========================================================*/
extern Acb_Man_t * Prs_ManBuildCbaBlif( char * pFileName, Vec_Ptr_t * vDes );
extern void Prs_ManReadBlifTest( char * pFileName );
extern Acb_Man_t * Acb_ManReadBlif( char * pFileName );
/*=== acbReadVer.c ===========================================================*/
extern Acb_Man_t * Prs_ManBuildCbaVerilog( char * pFileName, Vec_Ptr_t * vDes );
extern void Prs_ManReadVerilogTest( char * pFileName );
extern Acb_Man_t * Acb_ManReadVerilog( char * pFileName );
/*=== acbWriteBlif.c =========================================================*/
extern void Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
extern void Acb_ManWriteBlif( char * pFileName, Acb_Man_t * p );
/*=== acbWriteVer.c ==========================================================*/
extern void Acb_ManCreatePrimMap( char ** pMap );
extern char * Acb_ManGetSliceName( Acb_Ntk_t * p, int iFon, int RangeId );
extern void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
extern void Acb_ManWriteVerilog( char * pFileName, Acb_Man_t * p, int fInlineConcat );
/*=== acbUtil.c =============================================================*/
extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
ABC_NAMESPACE_HEADER_END

90
src/base/acb/acbAbc.c
View File

@ -21,6 +21,7 @@
#include "acb.h"
#include "base/abc/abc.h"
#include "aig/miniaig/ndr.h"
#include "acbPar.h"
ABC_NAMESPACE_IMPL_START
@ -69,6 +70,43 @@ Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
return pNtk;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Acb_NtkToAbc( Abc_Ntk_t * pNtk, Acb_Ntk_t * p )
{
int i, k, iObj, iFanin;
Abc_Ntk_t * pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
Mem_Flex_t * pMan = (Mem_Flex_t *)pNtkNew->pManFunc;
Acb_NtkCleanObjCopies( p );
Acb_NtkForEachCi( p, iObj, i )
Acb_ObjSetCopy( p, iObj, Abc_ObjId(Abc_NtkCi(pNtkNew, i)) );
Acb_NtkForEachNode( p, iObj )
{
Abc_Obj_t * pObjNew = Abc_NtkCreateNode( pNtkNew );
Acb_ObjForEachFanin( p, iObj, iFanin, k )
Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Acb_ObjCopy(p, iFanin)) );
pObjNew->pData = Abc_SopCreateFromTruth( pMan, Acb_ObjFaninNum(p, iObj), (unsigned *)Acb_ObjTruthP(p, iObj) );
}
Acb_NtkForEachCoDriver( p, iFanin, i )
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_NtkObj(pNtkNew, Acb_ObjCopy(p, iFanin)) );
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Acb_NtkToAbc: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
/**Function*************************************************************
Synopsis []
@ -138,6 +176,58 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
return pNtk;
}
/**Function*************************************************************
Synopsis [Setup parameter structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_ParSetDefault( Acb_Par_t * pPars )
{
memset( pPars, 0, sizeof(Acb_Par_t) );
pPars->nLutSize = 4; // LUT size
pPars->nTfoLevMax = 3; // the maximum fanout levels
pPars->nTfiLevMax = 3; // the maximum fanin levels
pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nDivMax = 16; // the maximum divisor count
pPars->nTabooMax = 4; // the minimum MFFC size
pPars->nGrowthLevel = 0; // the maximum allowed growth in level
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->nNodesMax = 0; // the maximum number of nodes to try
pPars->iNodeOne = 0; // one particular node to try
pPars->fArea = 0; // performs optimization for area
pPars->fMoreEffort = 0; // enables using more effort
pPars->fVerbose = 0; // enable basic stats
pPars->fVeryVerbose = 0; // enable detailed stats
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars )
{
extern void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars );
Abc_Ntk_t * pNtkNew;
Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk );
Acb_NtkOpt( p, pPars );
pNtkNew = Acb_NtkToAbc( pNtk, p );
Acb_ManFree( p->pDesign );
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

634
src/base/acb/acbMfs.c
View File

@ -21,6 +21,9 @@
#include "acb.h"
#include "bool/kit/kit.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"
#include "misc/util/utilTruth.h"
#include "acbPar.h"
ABC_NAMESPACE_IMPL_START
@ -34,7 +37,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis []
Synopsis [Derive CNF for nodes in the window.]
Description []
@ -43,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Acb_Truth2Cnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
int Acb_DeriveCnfFromTruth( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
{
Vec_StrClear( vCnf );
if ( Truth == 0 || ~Truth == 0 )
@ -82,58 +85,32 @@ int Acb_Truth2Cnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
return nCubes;
}
}
Vec_Wec_t * Acb_NtkDeriveCnf( Acb_Ntk_t * p )
Vec_Wec_t * Acb_DeriveCnfForWindow( Acb_Ntk_t * p, Vec_Int_t * vWin, int PivotVar )
{
Vec_Wec_t * vCnfs = Vec_WecStart( Acb_NtkObjNumMax(p) );
Vec_Str_t * vCnf = Vec_StrAlloc( 100 ); int iObj;
Acb_NtkForEachNode( p, iObj )
Vec_Wec_t * vCnfs = &p->vCnfs;
Vec_Str_t * vCnfBase, * vCnf = NULL; int i, iObj;
assert( Vec_WecSize(vCnfs) == Acb_NtkObjNumMax(p) );
Vec_IntForEachEntry( vWin, iObj, i )
{
int nCubes = Acb_Truth2Cnf( Acb_ObjTruth(p, iObj), Acb_ObjFaninNum(p, iObj), &p->vCover, vCnf );
Vec_Str_t * vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj );
if ( Abc_LitIsCompl(iObj) && i < PivotVar )
continue;
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj );
if ( vCnfBase != NULL )
continue;
if ( vCnf == NULL )
vCnf = Vec_StrAlloc( 1000 );
Acb_DeriveCnfFromTruth( Acb_ObjTruth(p, iObj), Acb_ObjFaninNum(p, iObj), &p->vCover, vCnf );
Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
vCnfBase->nSize = Vec_StrSize(vCnf);
}
Vec_StrFree( vCnf );
Vec_StrFreeP( &vCnf );
return vCnfs;
}
void Acb_CnfTranslate( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vSatVars, int iPivotVar )
{
Vec_Int_t * vClause;
signed char Entry;
int i, Lit;
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
Vec_StrForEachEntry( vCnf, Entry, i )
{
if ( (int)Entry == -1 )
{
vClause = Vec_WecPushLevel( vRes );
continue;
}
Lit = Abc_Lit2LitV( Vec_IntArray(vSatVars), (int)Entry );
Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
Vec_IntPush( vClause, Lit );
}
}
int Acb_ObjCreateCnf( sat_solver * pSat, Acb_Ntk_t * p, int iObj, Vec_Int_t * vSatVars, int iPivotVar )
{
Vec_Int_t * vClause; int k, RetValue;
Acb_CnfTranslate( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, iObj), vSatVars, iPivotVar );
Vec_WecForEachLevel( &p->vClauses, vClause, k )
{
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vClause), Vec_IntLimit(vClause) );
if ( RetValue == 0 )
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Constructs SAT solver for the window.]
Synopsis [Constructs CNF for the window.]
Description [The window for the pivot node is represented as a DFS ordered array
of objects (vWinObjs) whose indexes are used as SAT variable IDs (stored in p->vCopies).
@ -148,6 +125,22 @@ int Acb_ObjCreateCnf( sat_solver * pSat, Acb_Ntk_t * p, int iObj, Vec_Int_t * vS
SeeAlso []
***********************************************************************/
void Acb_TranslateCnf( Vec_Int_t * vClas, Vec_Int_t * vLits, Vec_Str_t * vCnf, Vec_Int_t * vSatVars, int iPivotVar )
{
signed char Entry;
int i, Lit;
Vec_StrForEachEntry( vCnf, Entry, i )
{
if ( (int)Entry == -1 )
{
Vec_IntPush( vClas, Vec_IntSize(vLits) );
continue;
}
Lit = Abc_Lit2LitV( Vec_IntArray(vSatVars), (int)Entry );
Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
Vec_IntPush( vLits, Lit );
}
}
int Acb_NtkCountRoots( Vec_Int_t * vWinObjs, int PivotVar )
{
int i, iObjLit, nRoots = 0;
@ -155,31 +148,27 @@ int Acb_NtkCountRoots( Vec_Int_t * vWinObjs, int PivotVar )
nRoots += Abc_LitIsCompl(iObjLit);
return nRoots;
}
sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot, Vec_Int_t * vWinObjs, int fQbf )
Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
{
Cnf_Dat_t * pCnf;
Vec_Int_t * vFaninVars = Vec_IntAlloc( 8 );
int PivotVar = Vec_IntFind(vWinObjs, Abc_Var2Lit(Pivot, 0));
int nRoots = Acb_NtkCountRoots(vWinObjs, PivotVar);
int TfoStart = PivotVar + 1;
int nTfoSize = Vec_IntSize(vWinObjs) - TfoStart;
int LastVar = Vec_IntSize(vWinObjs) + TfoStart + nRoots;
int i, k, iLit = 1, RetValue, iObj, iObjLit, iFanin, * pFanins;
//Vec_IntPrint( vWinObjs );
int nVarsAll = Vec_IntSize(vWinObjs) + nTfoSize + nRoots;
int i, k, iObj, iObjLit, iFanin, * pFanins, Entry;
Vec_Wec_t * vCnfs = Acb_DeriveCnfForWindow( p, vWinObjs, PivotVar );
Vec_Int_t * vClas = Vec_IntAlloc( 100 );
Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
// mark new SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i )
Acb_ObjSetCopy( p, i, iObj );
// create SAT solver
if ( pSat == NULL )
pSat = sat_solver_new();
else
sat_solver_restart( pSat );
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + nTfoSize + nRoots + 1 );
// create constant 0 clause
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
// add clauses for all nodes
Vec_IntForEachEntryStop( vWinObjs, iObjLit, i, TfoStart )
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntForEachEntry( vWinObjs, iObjLit, i )
{
if ( Abc_LitIsCompl(iObjLit) )
if ( Abc_LitIsCompl(iObjLit) && i < PivotVar )
continue;
iObj = Abc_Lit2Var(iObjLit);
assert( !Acb_ObjIsCio(p, iObj) );
@ -189,8 +178,7 @@ sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot,
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) );
// derive CNF for the node
RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, -1 );
assert( RetValue );
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, -1 );
}
// add second clauses for the TFO
Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, TfoStart )
@ -200,11 +188,10 @@ sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot,
// collect SAT variables
Vec_IntClear( vFaninVars );
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( vFaninVars, (fQbf && iFanin == Pivot) ? LastVar : Acb_ObjCopy(p, iFanin) );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) + (iFanin > PivotVar) * nTfoSize );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) + nTfoSize );
// derive CNF for the node
RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, fQbf ? -1 : PivotVar );
assert( RetValue );
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, PivotVar );
}
if ( nRoots > 0 )
{
@ -215,31 +202,91 @@ sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot,
{
if ( !Abc_LitIsCompl(iObjLit) )
continue;
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
sat_solver_add_xor( pSat, Acb_ObjCopy(p, iObj), Acb_ObjCopy(p, iObj) + nTfoSize, nVars++, 0 );
}
// make OR clause for the last nRoots variables
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
if ( RetValue == 0 )
{
Vec_IntFree( vFaninVars );
sat_solver_delete( pSat );
return NULL;
}
assert( sat_solver_nvars(pSat) == nVars + 1 );
}
else if ( fQbf )
{
int n, pLits[2];
for ( n = 0; n < 2; n++ )
{
pLits[0] = Abc_Var2Lit( PivotVar, n );
pLits[1] = Abc_Var2Lit( LastVar, n );
RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
assert( RetValue );
iObj = Abc_Lit2Var(iObjLit);
// add clauses
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars++, 0) );
}
Vec_IntAppend( vLits, vFaninVars );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
assert( nRoots == Vec_IntSize(vFaninVars) );
assert( nVars == nVarsAll );
}
Vec_IntFree( vFaninVars );
// undo SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i )
Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 );
// create CNF structure
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVarsAll;
pCnf->nClauses = Vec_IntSize(vClas)-1;
pCnf->nLiterals = Vec_IntSize(vLits);
pCnf->pClauses = ABC_ALLOC( int *, Vec_IntSize(vClas) );
pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
Vec_IntForEachEntry( vClas, Entry, i )
pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
// cleanup
Vec_IntFree( vClas );
Vec_IntFree( vLits );
return pCnf;
}
/**Function*************************************************************
Synopsis [Creates SAT solver containing several copies of the window.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes )
{
int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : nTimes;
Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar );
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 );
assert( nTimes == 1 || nTimes == 2 || nTimes == 6 );
for ( n = 0; n < nTimes; n++ )
{
if ( n & 1 )
Cnf_DataLiftAndFlipLits( pCnf, -pCnf->nVars, vFlips );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
Vec_IntFree( vFlips );
sat_solver_delete( pSat );
return NULL;
}
}
if ( n & 1 )
Cnf_DataLiftAndFlipLits( pCnf, pCnf->nVars, vFlips );
if ( n < nTimes - 1 )
Cnf_DataLift( pCnf, pCnf->nVars );
else if ( n ) // if ( n == nTimes - 1 )
Cnf_DataLift( pCnf, -(nTimes - 1) * pCnf->nVars );
}
Vec_IntFree( vFlips );
// add conditional buffers
for ( n = 0; n < nRounds; n++ )
{
int BaseA = n * pCnf->nVars;
int BaseB = ((n + 1) % nTimes) * pCnf->nVars;
int BaseC = nTimes * pCnf->nVars + n * nDivs;
for ( i = 0; i < nDivs; i++ )
sat_solver_add_buffer_enable( pSat, BaseA + i, BaseB + i, BaseC + i, 0 );
}
// finalize
RetValue = sat_solver_simplify( pSat );
if ( RetValue == 0 )
@ -250,64 +297,6 @@ sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot,
return pSat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkUnmarkWindow( Acb_Ntk_t * p, Vec_Int_t * vWin )
{
int i, iObj;
Vec_IntForEachEntry( vWin, iObj, i )
Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 );
}
/**Function*************************************************************
Synopsis [Collects divisors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Acb_ObjIsCritFanin( Acb_Ntk_t * p, int i, int f ) { return Acb_ObjLevelR(p, i) + Acb_ObjLevelD(p, f) == p->LevelMax; }
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int nTfiLevMin )
{
int i, k, iObj, iFanin, iFanin2, * pFanins, * pFanins2, Lev, Level = Acb_ObjLevelD(p, Pivot);
// include non-critical pivot fanins AND fanins of critical pivot fanins
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, i )
{
if ( !Acb_ObjIsCritFanin(p, Pivot, iFanin) ) // non-critical fanin
Vec_IntPush( vDivs, iFanin );
else // critical fanin
Acb_ObjForEachFaninFast( p, iFanin, pFanins2, iFanin2, k )
Vec_IntPushUnique( vDivs, iFanin2 );
}
// continue for a few more levels
for ( Lev = Level-2; Lev >= nTfiLevMin; Lev-- )
{
Vec_IntForEachEntry( vDivs, iObj, i )
if ( Acb_ObjLevelD(p, iObj) == Lev )
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPushUnique( vDivs, iFanin );
}
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
}
/**Function*************************************************************
@ -406,18 +395,18 @@ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t
Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots );
Vec_IntPush( vTfo, Diff );
}
void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots )
void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Pivot, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots )
{
int Res = Acb_ObjLabelTfo( p, Root, nTfoLevMax, nFanMax );
int Res = Acb_ObjLabelTfo( p, Pivot, nTfoLevMax, nFanMax );
Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 100 );
Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 );
if ( Res ) // none or root
return;
Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0)
Acb_ObjDeriveTfo_rec( p, Root, vTfo, vRoots );
assert( Vec_IntEntryLast(vTfo) == Root );
Acb_ObjDeriveTfo_rec( p, Pivot, vTfo, vRoots );
assert( Vec_IntEntryLast(vTfo) == Pivot );
Vec_IntPop( vTfo );
assert( Vec_IntEntryLast(vRoots) != Root );
assert( Vec_IntEntryLast(vRoots) != Pivot );
Vec_IntReverseOrder( vTfo );
Vec_IntReverseOrder( vRoots );
}
@ -439,12 +428,14 @@ Vec_Int_t * Acb_NtkCollectTfoSideInputs( Acb_Ntk_t * p, int Pivot, Vec_Int_t * v
Vec_Int_t * vSide = Vec_IntAlloc( 100 );
int i, k, Node, iFanin, * pFanins;
Acb_NtkIncTravId( p );
Vec_IntPush( vTfo, Pivot );
Vec_IntForEachEntry( vTfo, Node, i )
Acb_ObjSetTravIdCur( p, Node ), assert( Node != Pivot );
Acb_ObjSetTravIdCur( p, Node );
Vec_IntForEachEntry( vTfo, Node, i )
Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur(p, iFanin) && iFanin != Pivot )
Vec_IntPush( vSide, iFanin );
Vec_IntPop( vTfo );
return vSide;
}
@ -481,11 +472,14 @@ void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew )
Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew );
Vec_IntPush( vTfiNew, iObj );
}
Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vSide )
Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide )
{
Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 );
int i, Node;
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vDivs, Node, i )
Acb_NtkCollectNewTfi1_rec( p, Node, vTfiNew );
assert( Vec_IntSize(vTfiNew) == Vec_IntSize(vDivs) );
Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew );
assert( Vec_IntEntryLast(vTfiNew) == Pivot );
Vec_IntPop( vTfiNew );
@ -510,6 +504,7 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve
{
Vec_Int_t * vWin = Vec_IntAlloc( 100 );
int i, k, iObj, iFanin, * pFanins;
assert( Vec_IntEntryLast(vTfi) == Pivot );
// mark leaves
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vTfi, iObj, i )
@ -532,6 +527,73 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve
return vWin;
}
/**Function*************************************************************
Synopsis [Collects divisors in a non-topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax )
{
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Vec_Int_t * vFront = Vec_IntAlloc( 100 );
int i, k, iFanin, * pFanins;
// mark taboo nodes
Acb_NtkIncTravId( p );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjSetTravIdCur( p, Pivot );
for ( i = 0; i < nTaboo; i++ )
{
assert( !Acb_ObjIsCio(p, pTaboo[i]) );
if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) )
assert( 0 );
}
// collect non-taboo fanins of pivot but do not use them as frontier
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
Vec_IntPush( vDivs, iFanin );
// collect non-tabook fanins of taboo nodes and use them as frontier
for ( i = 0; i < nTaboo; i++ )
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
// select divisors incrementally
while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax )
{
// select the topmost
int iObj, iObjMax = -1, LevelMax = -1;
Vec_IntForEachEntry( vFront, iObj, k )
if ( LevelMax < Acb_ObjLevelD(p, iObj) )
LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj));
assert( iObjMax > 0 );
Vec_IntRemove( vFront, iObjMax );
// expand the topmost
Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
}
Vec_IntFree( vFront );
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
}
/**Function*************************************************************
Synopsis []
@ -543,29 +605,30 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax, Vec_Int_t ** pvDivs )
Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax, int nTfoLevs, int nFanMax, int * pnDivs )
{
int nTfiLevMin = Acb_ObjLevelD(p, Pivot) - nTfiLevs;
int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs;
Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi;
// collect divisors by traversing limited TFI
vDivs = Acb_NtkDivisors( p, Pivot, nTfiLevMin );
vDivs = Acb_NtkDivisors( p, Pivot, pTaboo, nTaboo, nDivsMax );
// mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect TFO and roots
Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots );
// collect side inputs of the TFO
vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo );
// mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect new TFI
vTfi = Acb_NtkCollectNewTfi( p, Pivot, vSide );
vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide );
Vec_IntFree( vSide );
Vec_IntFree( vDivs );
// collect all nodes
vWin = Acb_NtkCollectWindow( p, Pivot, vTfi, vTfo, vRoots );
// cleanup
Vec_IntFree( vTfi );
Vec_IntFree( vTfo );
Vec_IntFree( vRoots );
Vec_IntFree( vSide );
*pvDivs = vDivs;
return vWin;
}
@ -597,6 +660,155 @@ int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int
return Vec_IntSize(vDivs);
}
/**Function*************************************************************
Synopsis [Computes function of the node]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars )
{
int fExpand = 1;
word uCube, uTruth = 0;
Vec_Int_t * vTempLits = Vec_IntAlloc( 100 );
int status, i, iVar, iLit, nFinal, * pFinal, pLits[2];
assert( FreeVar < sat_solver_nvars(pSat) );
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
while ( 1 )
{
// find onset minterm
status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
if ( status == l_False )
{
Vec_IntFree( vTempLits );
return uTruth;
}
assert( status == l_True );
if ( fExpand )
{
// collect divisor literals
Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[0]) ); // F = 0
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTempLits, sat_solver_var_literal(pSat, iVar) );
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits), 0, 0, 0, 0 );
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal );
Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
uCube = ~(word)0;
for ( i = 0; i < nFinal; i++ )
if ( pFinal[i] != pLits[0] )
Vec_IntPush( vTempLits, pFinal[i] );
}
else
{
// collect divisor literals
Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) );// NOT(iNewLit)
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTempLits, Abc_LitNot(sat_solver_var_literal(pSat, iVar)) );
}
Vec_IntForEachEntry( vTempLits, iLit, i )
{
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(iLit) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
status = sat_solver_addclause( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits) );
if ( status == 0 )
{
Vec_IntFree( vTempLits );
return uTruth;
}
}
assert( 0 );
return ~(word)0;
}
/**Function*************************************************************
Synopsis [Collects the taboo nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Acb_ObjIsCritFanin( Acb_Ntk_t * p, int i, int f ) { return Acb_ObjLevelR(p, i) + Acb_ObjLevelD(p, f) == p->LevelMax; }
static inline void Acb_ObjUpdateFanoutCount( Acb_Ntk_t * p, int iObj, int AddOn )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Acb_ObjFanoutVec(p, iFanin)->nSize += AddOn;
}
int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo )
{
int i, k, iFanin, * pFanins, nTaboo = 0;
if ( nTabooMax == 0 ) // delay optimization
{
// collect delay critical fanins of the pivot node
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjIsCi(p, iFanin) && Acb_ObjIsCritFanin( p, Pivot, iFanin ) )
pTaboo[ nTaboo++ ] = iFanin;
}
else // area optimization
{
// check if the node has any area critical fanins
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjIsCi(p, iFanin) && Acb_ObjFanoutNum(p, iFanin) == 1 )
break;
if ( k < Acb_ObjFaninNum(p, Pivot) ) // there is fanin
{
// mark pivot
Acb_NtkIncTravId( p );
Acb_ObjSetTravIdCur( p, Pivot );
Acb_ObjUpdateFanoutCount( p, Pivot, -1 );
// add the first taboo node
assert( Acb_ObjFanoutNum(p, iFanin) == 0 );
pTaboo[ nTaboo++ ] = iFanin;
Acb_ObjSetTravIdCur( p, iFanin );
Acb_ObjUpdateFanoutCount( p, iFanin, -1 );
while ( nTaboo < nTabooMax )
{
// select the first unrefed fanin
for ( i = 0; i < nTaboo; i++ )
{
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjIsCi(p, iFanin) && !Acb_ObjIsTravIdCur(p, iFanin) && Acb_ObjFanoutNum(p, iFanin) == 0 )
{
pTaboo[ nTaboo++ ] = iFanin;
Acb_ObjSetTravIdCur( p, iFanin );
Acb_ObjUpdateFanoutCount( p, iFanin, -1 );
break;
}
if ( k < Acb_ObjFaninNum(p, pTaboo[i]) )
break;
}
if ( i == nTaboo ) // no change
break;
}
// reference nodes back
Acb_ObjUpdateFanoutCount( p, Pivot, 1 );
for ( i = 0; i < nTaboo; i++ )
Acb_ObjUpdateFanoutCount( p, pTaboo[i], 1 );
}
}
return nTaboo;
}
/**Function*************************************************************
Synopsis []
@ -608,25 +820,113 @@ int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int
SeeAlso []
***********************************************************************/
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax )
static inline void Vec_IntVars2Lits( Vec_Int_t * p, int Shift, int fCompl )
{
Vec_Int_t * vSupp = &p->vArray0;
Vec_Int_t * vDivs, * vWin = Acb_NtkWindow( p, Pivot, nTfiLevs, nTfoLevs, nFanMax, &vDivs );
sat_solver * pSat = Acb_NtkWindow2Solver( pSat, p, Pivot, vWin, 0 );
int nSuppNew, Level = Acb_ObjLevelD( p, Pivot );
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Abc_Var2Lit( p->pArray[i] + Shift, fCompl );
}
static inline void Vec_IntLits2Vars( Vec_Int_t * p, int Shift )
{
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) - Shift;
}
static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
{
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Vec_IntEntry(vMap, p->pArray[i]);
}
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize )
{
Cnf_Dat_t * pCnf;
Vec_Int_t * vWin, * vSupp;
sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
int c, nSuppNew, PivotVar, nDivs = 0;
int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo );
if ( nTaboo == 0 )
return;
assert( nTabooMax == 0 || nTaboo <= nTabooMax );
assert( nTaboo <= 16 );
// compute divisor and window for these nodes
vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs );
PivotVar = Vec_IntFind(vWin, Abc_Var2Lit(Pivot, 0));
// derive CNF and SAT solvers
pCnf = Acb_NtkWindow2Cnf( p, vWin, Pivot );
pSat1 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 1 );
// check constants
for ( c = 0; c < 2; c++ )
{
int Lit = Abc_Var2Lit( PivotVar, c );
int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 );
if ( status == l_False )
{
Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL );
goto cleanup;
}
assert( status == l_True );
}
pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 );
//pSat6 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 6 );
// try solving the original support
Vec_IntClear( vSupp );
Vec_IntAppend( vSupp, vDivs );
nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
vSupp = Vec_IntStartNatural( nDivs );
Vec_IntVars2Lits( vSupp, 2*pCnf->nVars, 0 );
nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
Vec_IntShrink( vSupp, nSuppNew );
Vec_IntLits2Vars( vSupp, -2*pCnf->nVars );
// try solving by level
if ( nSuppNew <= nLutSize )
{
int FreeVar = sat_solver_nvars( pSat1 ) - 1;
word uTruth;
Acb_NtkUnmarkWindow( p, vWin );
Vec_IntVars2Lits( vSupp, pCnf->nVars, 0 );
uTruth = Acb_ComputeFunction( pSat1, PivotVar, FreeVar, vSupp );
Vec_IntLits2Vars( vSupp, -pCnf->nVars );
// create support in terms of nodes
Vec_IntRemap( vSupp, vWin );
Vec_IntLits2Vars( vSupp, 0 );
Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp );
goto cleanup;
}
// cleanup
cleanup:
if ( pSat1 ) sat_solver_delete( pSat1 );
if ( pSat2 ) sat_solver_delete( pSat2 );
if ( pSat3 ) sat_solver_delete( pSat3 );
Cnf_DataFree( pCnf );
Vec_IntFree( vWin );
Vec_IntFree( vDivs );
Vec_IntFree( vSupp );
}
void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars )
{
int iObj;
if ( pPars->fArea )
{
Acb_NtkForEachNode( p, iObj )
Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize );
}
else
{
Acb_NtkUpdateTiming( p, -1 );
while ( 1 )
{
int iObj = 0;
Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize );
}
}
}
////////////////////////////////////////////////////////////////////////

70
src/base/acb/acbPar.h Normal file
View File

@ -0,0 +1,70 @@
/**CFile****************************************************************
FileName [acbPar.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Hierarchical word-level netlist.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 21, 2015.]
Revision [$Id: acbPar.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__base__acb__acbPar_h
#define ABC__base__acb__acbPar_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Acb_Par_t_ Acb_Par_t;
struct Acb_Par_t_
{
int nLutSize; // LUT size
int nTfoLevMax; // the maximum fanout levels
int nTfiLevMax; // the maximum fanin levels
int nFanoutMax; // the maximum number of fanouts
int nDivMax; // the maximum divisor count
int nTabooMax; // the minimum MFFC size
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int nNodesMax; // the maximum number of nodes to try
int iNodeOne; // one particular node to try
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
/*=== acbAbc.c =============================================================*/
extern void Acb_ParSetDefault( Acb_Par_t * pPars );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

68
src/base/acb/acbUtil.c
View File

@ -42,13 +42,24 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
void Acb_ObjAddFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_ObjRemoveFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{
int k, iObj, iFanin, * pFanins;
int iObj;
Vec_WecInit( &p->vFanouts, Acb_NtkObjNumMax(p) );
Acb_NtkForEachObj( p, iObj )
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
Acb_ObjAddFanout( p, iObj );
}
/**Function*************************************************************
@ -263,12 +274,11 @@ int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
int Acb_NtkComputePaths( Acb_Ntk_t * p )
{
int LevelD = Acb_NtkComputeLevelD( p, NULL );
int LevelR = Acb_NtkComputeLevelR( p, NULL );
int PathD = Acb_NtkComputePathsD( p, NULL );
int PathR = Acb_NtkComputePathsR( p, NULL );
assert( PathD == PathR );
return PathR;
Acb_NtkComputeLevelD( p, NULL );
Acb_NtkComputeLevelR( p, NULL );
Acb_NtkComputePathsD( p, NULL );
Acb_NtkComputePathsR( p, NULL );
return p->nPaths;
}
void Abc_NtkComputePaths( Abc_Ntk_t * p )
@ -310,10 +320,10 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
// assuming that level of the new nodes is up to date
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
int nLevelD = Acb_NtkComputeLevelD( p, vTfo );
int nLevelR = Acb_NtkComputeLevelR( p, vTfi );
int nPathD = Acb_NtkComputePathsD( p, vTfo );
int nPathR = Acb_NtkComputePathsR( p, vTfi );
Acb_NtkComputeLevelD( p, vTfo );
Acb_NtkComputeLevelR( p, vTfi );
Acb_NtkComputePathsD( p, vTfo );
Acb_NtkComputePathsR( p, vTfi );
Vec_IntForEachEntry( vTfi, Entry, i )
Acb_ObjUpdateTiming( p, Entry );
Vec_IntForEachEntry( vTfo, Entry, i )
@ -321,16 +331,40 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
}
else
{
int LevelD = Acb_NtkComputeLevelD( p, NULL );
int LevelR = Acb_NtkComputeLevelR( p, NULL );
int PathD = Acb_NtkComputePathsD( p, NULL );
int PathR = Acb_NtkComputePathsR( p, NULL );
Acb_NtkComputeLevelD( p, NULL );
Acb_NtkComputeLevelR( p, NULL );
Acb_NtkComputePathsD( p, NULL );
Acb_NtkComputePathsR( p, NULL );
Acb_NtkForEachNode( p, Entry )
Acb_ObjUpdateTiming( p, Entry );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{
int i, iFanin;
Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth );
Acb_ObjRemoveFanout( p, Pivot );
Acb_ObjRemoveFanins( p, Pivot );
Vec_IntForEachEntry( vSupp, iFanin, i )
Acb_ObjAddFanin( p, Pivot, iFanin );
Acb_ObjAddFanout( p, Pivot );
Acb_NtkUpdateTiming( p, Pivot );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/proof/acec/acec2Mult.c
View File

@ -855,7 +855,7 @@ int Sdb_StoDiffExactlyOne3( Vec_Wec_t * vCuts, int Limit, int * pCut, int * pCou
}
Vec_Int_t * Sdb_StoFindAll( Vec_Wec_t * vCuts )
{
int i, k, Entry, iNew = -1;
int i, k, Entry;
Vec_Int_t * vCut, * vAll = Vec_IntAlloc( 100 );
Vec_WecForEachLevel( vCuts, vCut, i )
Vec_IntForEachEntry( vCut, Entry, k )

3
src/sat/cnf/cnf.h
View File

@ -156,7 +156,8 @@ extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses,
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p );
extern Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar );
extern void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits );
extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists );
extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );

32
src/sat/cnf/cnfMan.c
View File

@ -193,7 +193,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
/**Function*************************************************************
Synopsis [Writes CNF into a file.]
Synopsis []
Description []
@ -215,26 +215,26 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
for ( v = 0; v < p->nLiterals; v++ )
p->pClauses[0][v] += 2*nVarsPlus;
}
/**Function*************************************************************
Synopsis [Writes CNF into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p )
Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar )
{
p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] );
Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int v;
assert( p->pMan == NULL );
for ( v = 0; v < p->nLiterals; v++ )
if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar )
Vec_IntPush( vLits, v );
return vLits;
}
void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits )
{
int i, iLit;
assert( p->pMan == NULL );
Vec_IntForEachEntry( vLits, iLit, i )
p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2*nVarsPlus;
}
/**Function*************************************************************
Synopsis [Writes CNF into a file.]
Synopsis []
Description []