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

Improvements to delay-optimization in &satlut.

This commit is contained in:
Alan Mishchenko 2016-04-04 12:51:05 -07:00
parent 4a954c1b23
commit 720082753f
3 changed files with 269 additions and 158 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

399
src/aig/gia/giaSatLut.c
View File

@ -33,47 +33,191 @@ ABC_NAMESPACE_IMPL_START
typedef struct Sbl_Man_t_ Sbl_Man_t;
struct Sbl_Man_t_
{
sat_solver * pSat; // SAT solver
Vec_Int_t * vCardVars; // candinality variables
int LogN; // max vars
int FirstVar; // first variable to be used
int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
int nInputs; // the number of inputs
int nEdges; // the number of edges
sat_solver * pSat; // SAT solver
Vec_Int_t * vCardVars; // candinality variables
int nVars; // max vars
int LogN; // base-2 log of max vars
int Power2; // power-2 of LogN
int FirstVar; // first variable to be used
int nRuns; // the number of runs
// parameters
int nBTLimit; // conflicts
int DelayMax; // external delay
int nEdges; // the number of edges
int fDelay; // delay mode
int fReverse; // reverse windowing
int fVeryVerbose; // verbose
int fVerbose; // verbose
// window
Gia_Man_t * pGia;
Vec_Int_t * vLeaves; // leaf nodes
Vec_Int_t * vAnds; // AND-gates
Vec_Int_t * vNodes; // internal LUTs
Vec_Int_t * vRoots; // driver nodes (a subset of vAnds)
Vec_Int_t * vRootVars; // driver nodes (as SAT variables)
Gia_Man_t * pGia;
Vec_Int_t * vLeaves; // leaf nodes
Vec_Int_t * vAnds; // AND-gates
Vec_Int_t * vNodes; // internal LUTs
Vec_Int_t * vRoots; // driver nodes (a subset of vAnds)
Vec_Int_t * vRootVars; // driver nodes (as SAT variables)
// timing
Vec_Int_t * vArrs; // arrival times
Vec_Int_t * vReqs; // required times
Vec_Wec_t * vWindow; // fanins of each node in the window
Vec_Int_t * vPath; // critical path (as SAT variables)
Vec_Int_t * vEdges; // fanin edges
Vec_Int_t * vArrs; // arrival times
Vec_Int_t * vReqs; // required times
Vec_Wec_t * vWindow; // fanins of each node in the window
Vec_Int_t * vPath; // critical path (as SAT variables)
Vec_Int_t * vEdges; // fanin edges
// cuts
Vec_Wrd_t * vCutsI; // input bit patterns
Vec_Wrd_t * vCutsN; // node bit patterns
Vec_Int_t * vCutsNum; // cut counts for each obj
Vec_Int_t * vCutsStart; // starting cuts for each obj
Vec_Int_t * vCutsObj; // object to which this cut belongs
Vec_Wrd_t * vTempI; // temporary cuts
Vec_Wrd_t * vTempN; // temporary cuts
Vec_Int_t * vSolInit; // initial solution
Vec_Int_t * vSolCur; // current solution
Vec_Int_t * vSolBest; // best solution
Vec_Wrd_t * vCutsI; // input bit patterns
Vec_Wrd_t * vCutsN; // node bit patterns
Vec_Int_t * vCutsNum; // cut counts for each obj
Vec_Int_t * vCutsStart; // starting cuts for each obj
Vec_Int_t * vCutsObj; // object to which this cut belongs
Vec_Wrd_t * vTempI; // temporary cuts
Vec_Wrd_t * vTempN; // temporary cuts
Vec_Int_t * vSolInit; // initial solution
Vec_Int_t * vSolCur; // current solution
Vec_Int_t * vSolBest; // best solution
// temporary
Vec_Int_t * vLits; // literals
Vec_Int_t * vAssump; // literals
Vec_Int_t * vPolar; // variables polarity
Vec_Int_t * vLits; // literals
Vec_Int_t * vAssump; // literals
Vec_Int_t * vPolar; // variables polarity
// statistics
abctime timeWin; // windowing
abctime timeCut; // cut computation
abctime timeSat; // SAT runtime
abctime timeSatSat; // satisfiable time
abctime timeSatUns; // unsatisfiable time
abctime timeSatUnd; // undecided time
abctime timeTime; // timing time
abctime timeStart; // starting time
abctime timeTotal; // all runtime
abctime timeOther; // other time
};
extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int Number )
{
Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
p->nVars = Number;
p->LogN = Abc_Base2Log(Number);
p->Power2 = 1 << p->LogN;
p->pSat = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
p->FirstVar = sat_solver_nvars( p->pSat );
sat_solver_bookmark( p->pSat );
// window
p->pGia = pGia;
p->vLeaves = Vec_IntAlloc( p->nVars );
p->vAnds = Vec_IntAlloc( p->nVars );
p->vNodes = Vec_IntAlloc( p->nVars );
p->vRoots = Vec_IntAlloc( p->nVars );
p->vRootVars = Vec_IntAlloc( p->nVars );
// timing
p->vArrs = Vec_IntAlloc( 0 );
p->vReqs = Vec_IntAlloc( 0 );
p->vWindow = Vec_WecAlloc( 128 );
p->vPath = Vec_IntAlloc( 32 );
p->vEdges = Vec_IntAlloc( 32 );
// cuts
p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns
p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns
p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj
p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj
p->vCutsObj = Vec_IntAlloc( 1000 );
p->vSolInit = Vec_IntAlloc( 64 );
p->vSolCur = Vec_IntAlloc( 64 );
p->vSolBest = Vec_IntAlloc( 64 );
p->vTempI = Vec_WrdAlloc( 32 );
p->vTempN = Vec_WrdAlloc( 32 );
// internal
p->vLits = Vec_IntAlloc( 64 );
p->vAssump = Vec_IntAlloc( 64 );
p->vPolar = Vec_IntAlloc( 1000 );
// other
Gia_ManFillValue( pGia );
return p;
}
void Sbl_ManClean( Sbl_Man_t * p )
{
p->timeStart = Abc_Clock();
sat_solver_rollback( p->pSat );
sat_solver_bookmark( p->pSat );
// internal
Vec_IntClear( p->vLeaves );
Vec_IntClear( p->vAnds );
Vec_IntClear( p->vNodes );
Vec_IntClear( p->vRoots );
Vec_IntClear( p->vRootVars );
// timing
Vec_IntClear( p->vArrs );
Vec_IntClear( p->vReqs );
Vec_WecClear( p->vWindow );
Vec_IntClear( p->vPath );
Vec_IntClear( p->vEdges );
// cuts
Vec_WrdClear( p->vCutsI );
Vec_WrdClear( p->vCutsN );
Vec_IntClear( p->vCutsNum );
Vec_IntClear( p->vCutsStart );
Vec_IntClear( p->vCutsObj );
Vec_IntClear( p->vSolInit );
Vec_IntClear( p->vSolCur );
Vec_IntClear( p->vSolBest );
Vec_WrdClear( p->vTempI );
Vec_WrdClear( p->vTempN );
// temporary
Vec_IntClear( p->vLits );
Vec_IntClear( p->vAssump );
Vec_IntClear( p->vPolar );
// other
Gia_ManFillValue( p->pGia );
p->nRuns++;
}
void Sbl_ManStop( Sbl_Man_t * p )
{
sat_solver_delete( p->pSat );
Vec_IntFree( p->vCardVars );
// internal
Vec_IntFree( p->vLeaves );
Vec_IntFree( p->vAnds );
Vec_IntFree( p->vNodes );
Vec_IntFree( p->vRoots );
Vec_IntFree( p->vRootVars );
// timing
Vec_IntFree( p->vArrs );
Vec_IntFree( p->vReqs );
Vec_WecFree( p->vWindow );
Vec_IntFree( p->vPath );
Vec_IntFree( p->vEdges );
// cuts
Vec_WrdFree( p->vCutsI );
Vec_WrdFree( p->vCutsN );
Vec_IntFree( p->vCutsNum );
Vec_IntFree( p->vCutsStart );
Vec_IntFree( p->vCutsObj );
Vec_IntFree( p->vSolInit );
Vec_IntFree( p->vSolCur );
Vec_IntFree( p->vSolBest );
Vec_WrdFree( p->vTempI );
Vec_WrdFree( p->vTempN );
// temporary
Vec_IntFree( p->vLits );
Vec_IntFree( p->vAssump );
Vec_IntFree( p->vPolar );
// other
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Timing computation.]
@ -211,6 +355,7 @@ int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
}
int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
{
abctime clk = Abc_Clock();
Vec_Int_t * vFanins;
int i, iLut = -1, iAnd, Delay, Required, Edges;
Vec_IntClear( p->vPath );
@ -233,6 +378,7 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
if ( Delay > Required ) // updated timing exceeded original timing
break;
}
p->timeTime += Abc_Clock() - clk;
if ( i == Vec_IntSize(p->vRoots) )
return 1;
// derive the critical path
@ -332,7 +478,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
SeeAlso []
***********************************************************************/
static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
static int Sbl_ManPrintCut( word CutI, word CutN )
{
int b, Count = 0;
printf( "{ " );
@ -348,7 +494,7 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
}
static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c )
{
return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c), Vec_IntSize(p->vLeaves) );
return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c) );
}
static inline int Sbl_CutIsFeasible( word CutI, word CutN )
{
@ -411,11 +557,11 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
int i;
//printf( "\nLooking for:\n" );
//Sbl_ManPrintCut( CutI, CutN, p->nInputs );
//Sbl_ManPrintCut( CutI, CutN );
//printf( "\n" );
for ( i = Start0; i < Limit0; i++ )
{
//Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
//Sbl_ManPrintCut( pCutsI[i], pCutsN[i] );
if ( pCutsI[i] == CutI && pCutsN[i] == CutN )
return i;
}
@ -423,9 +569,10 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
}
int Sbl_ManComputeCuts( Sbl_Man_t * p )
{
abctime clk = Abc_Clock();
Gia_Obj_t * pObj; Vec_Int_t * vFanins;
int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds);
assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 );
assert( Vec_IntSize(p->vLeaves) <= p->nVars && Vec_IntSize(p->vAnds) <= p->nVars );
// assign leaf cuts
Vec_IntClear( p->vCutsStart );
Vec_IntClear( p->vCutsObj );
@ -510,6 +657,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
pObj->Value = ~0;
Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
pObj->Value = ~0;
p->timeCut += Abc_Clock() - clk;
return Vec_WrdSize(p->vCutsI);
}
int Sbl_ManCreateCnf( Sbl_Man_t * p )
@ -573,80 +721,6 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p )
SeeAlso []
***********************************************************************/
Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
{
Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars );
p->LogN = LogN;
p->FirstVar = sat_solver_nvars( p->pSat );
// window
p->pGia = pGia;
p->vLeaves = Vec_IntAlloc( 64 );
p->vAnds = Vec_IntAlloc( 64 );
p->vNodes = Vec_IntAlloc( 64 );
p->vRoots = Vec_IntAlloc( 64 );
p->vRootVars = Vec_IntAlloc( 64 );
// timing
p->vArrs = Vec_IntAlloc( 0 );
p->vReqs = Vec_IntAlloc( 0 );
p->vWindow = Vec_WecAlloc( 128 );
p->vPath = Vec_IntAlloc( 32 );
p->vEdges = Vec_IntAlloc( 32 );
// cuts
p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns
p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns
p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj
p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj
p->vCutsObj = Vec_IntAlloc( 1000 );
p->vSolInit = Vec_IntAlloc( 64 );
p->vSolCur = Vec_IntAlloc( 64 );
p->vSolBest = Vec_IntAlloc( 64 );
p->vTempI = Vec_WrdAlloc( 32 );
p->vTempN = Vec_WrdAlloc( 32 );
// internal
p->vLits = Vec_IntAlloc( 64 );
p->vAssump = Vec_IntAlloc( 64 );
p->vPolar = Vec_IntAlloc( 1000 );
// other
Gia_ManFillValue( pGia );
return p;
}
void Sbl_ManStop( Sbl_Man_t * p )
{
sat_solver_delete( p->pSat );
Vec_IntFree( p->vCardVars );
// internal
Vec_IntFree( p->vLeaves );
Vec_IntFree( p->vAnds );
Vec_IntFree( p->vNodes );
Vec_IntFree( p->vRoots );
Vec_IntFree( p->vRootVars );
// timing
Vec_IntFree( p->vArrs );
Vec_IntFree( p->vReqs );
Vec_WecFree( p->vWindow );
Vec_IntFree( p->vPath );
Vec_IntFree( p->vEdges );
// cuts
Vec_WrdFree( p->vCutsI );
Vec_WrdFree( p->vCutsN );
Vec_IntFree( p->vCutsNum );
Vec_IntFree( p->vCutsStart );
Vec_IntFree( p->vCutsObj );
Vec_IntFree( p->vSolInit );
Vec_IntFree( p->vSolCur );
Vec_IntFree( p->vSolBest );
Vec_WrdFree( p->vTempI );
Vec_WrdFree( p->vTempN );
// temporary
Vec_IntFree( p->vLits );
Vec_IntFree( p->vAssump );
Vec_IntFree( p->vPolar );
// other
ABC_FREE( p );
}
void Sbl_ManWindow( Sbl_Man_t * p )
{
@ -667,8 +741,10 @@ void Sbl_ManWindow( Sbl_Man_t * p )
int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
{
abctime clk = Abc_Clock();
Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds );
p->timeWin += Abc_Clock() - clk;
if ( Count == 0 )
return 0;
Vec_IntClear( p->vRoots ); Vec_IntAppend( p->vRoots, vRoots );
@ -684,41 +760,34 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
return Count;
}
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int nEdges, int fDelay, int fVeryVerbose, int fVerbose )
int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
{
int fKeepTrying = 1;
abctime clk = Abc_Clock(), clk2;
int i, LogN = 6, nVars = 1 << LogN, status, Root;
Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
int StartSol, Count, nConfTotal = 0, nIters = 0;
int i, status, Root, Count, StartSol, nConfTotal = 0, nIters = 0;
p->nEdges = nEdges;
fVerbose |= fVeryVerbose;
Vec_IntClear( p->vSolBest );
Sbl_ManClean( p );
// compute one window
Count = Sbl_ManWindow2( p, iPivot );
if ( Count == 0 )
{
printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 );
Sbl_ManStop( p );
return 0;
}
if ( fVerbose )
if ( p->fVerbose )
printf( "\nObj = %6d : Leaf = %2d. LUT = %2d. AND = %2d. Root = %2d.\n",
iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) );
if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 )
if ( Vec_IntSize(p->vLeaves) > p->nVars || Vec_IntSize(p->vAnds) > p->nVars )
{
printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) );
Sbl_ManStop( p );
return 0;
}
if ( Vec_IntSize(p->vAnds) < 10 )
{
if ( fVerbose )
if ( p->fVerbose )
printf( "Skipping.\n" );
Sbl_ManStop( p );
return 0;
}
@ -727,10 +796,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
// derive SAT instance
Sbl_ManCreateCnf( p );
if ( fVeryVerbose )
if ( p->fVeryVerbose )
Vec_IntPrint( p->vSolInit );
if ( fVeryVerbose )
if ( p->fVeryVerbose )
printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n",
sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds),
sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
@ -740,7 +809,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
Vec_IntClear( p->vAssump );
Vec_IntPush( p->vAssump, -1 );
// unused variables
for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ )
for ( i = Vec_IntSize(p->vAnds); i < p->Power2; i++ )
Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
// root variables
Vec_IntForEachEntry( p->vRootVars, Root, i )
@ -752,7 +821,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
while ( fKeepTrying && StartSol-fKeepTrying > 0 )
{
int nConfBef, nConfAft;
if ( fVerbose )
if ( p->fVerbose )
printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
// for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ )
// Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
@ -760,20 +829,27 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
// solve the problem
clk2 = Abc_Clock();
nConfBef = (int)p->pSat->stats.conflicts;
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 );
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), p->nBTLimit, 0, 0, 0 );
p->timeSat += Abc_Clock() - clk2;
nConfAft = (int)p->pSat->stats.conflicts;
nConfTotal += nConfAft - nConfBef;
nIters++;
if ( status == l_True )
p->timeSatSat += Abc_Clock() - clk2;
else if ( status == l_False )
p->timeSatUns += Abc_Clock() - clk2;
else
p->timeSatUnd += Abc_Clock() - clk2;
if ( status == l_Undef )
break;
if ( status == l_True )
{
int Count = 0, LitCount = 0;
if ( fVeryVerbose )
if ( p->fVeryVerbose )
{
printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n",
Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds),
Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars );
Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), p->nVars );
for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
printf( "%d", sat_solver_var_value(p->pSat, i) );
printf( "\n" );
@ -793,15 +869,15 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
if ( sat_solver_var_value(p->pSat, i) )
{
if ( fVeryVerbose )
if ( p->fVeryVerbose )
printf( "Cut %3d : Node = %3d Node = %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
if ( fVeryVerbose )
if ( p->fVeryVerbose )
LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
Vec_IntPush( p->vSolCur, i-p->FirstVar );
}
if ( fVeryVerbose )
if ( p->fVeryVerbose )
printf( "LitCount = %d.\n", LitCount );
if ( fVeryVerbose )
if ( p->fVeryVerbose )
Vec_IntPrint( p->vRootVars );
//Vec_IntPrint( p->vRoots );
//Vec_IntPrint( p->vAnds );
@ -812,10 +888,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
// check the timing
if ( status == l_True )
{
if ( fDelay && !Sbl_ManEvaluateMapping(p, DelayMax) )
if ( p->fDelay && !Sbl_ManEvaluateMapping(p, p->DelayMax) )
{
int iLit, value;
if ( fVerbose )
if ( p->fVerbose )
{
printf( "Critical path of length (%d) is detected: ", Vec_IntSize(p->vPath) );
Vec_IntForEachEntry( p->vPath, iLit, i )
@ -835,7 +911,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
}
else
fKeepTrying = 0;
if ( fVerbose )
if ( p->fVerbose )
{
if ( status == l_False )
printf( "UNSAT " );
@ -856,31 +932,54 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
// update solution
if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
{
int nDelay, nEdges;
nDelay = Sbl_ManCreateTiming( p, DelayMax, &nEdges );
int nDelayCur, nEdgesCur;
nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax, &nEdgesCur );
Sbl_ManUpdateMapping( p );
printf( "Object %5d : Saved %d nodes (Conf =%8d) Iter =%3d Delay = %d Edges = %4d\n",
iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelay, nEdges );
Sbl_ManStop( p );
iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur );
p->timeTotal += Abc_Clock() - p->timeStart;
return 2;
}
Sbl_ManStop( p );
p->timeTotal += Abc_Clock() - p->timeStart;
return 1;
}
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
void Sbl_ManPrintRuntime( Sbl_Man_t * p )
{
int iLut;
p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeSat - p->timeTime;
ABC_PRTP( "Win ", p->timeWin , p->timeTotal );
ABC_PRTP( "Cut ", p->timeCut , p->timeTotal );
ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal );
ABC_PRTP( " Unsat", p->timeSatUns, p->timeTotal );
ABC_PRTP( " Undec", p->timeSatUnd, p->timeTotal );
ABC_PRTP( "Timing", p->timeTime , p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL ", p->timeTotal, p->timeTotal );
printf( "Total runs = %d.\n", p->nRuns );
}
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
{
int iLut, nImproveCount = 0;
Sbl_Man_t * p = Sbl_ManAlloc( pGia, nNumber );
p->nBTLimit = nBTLimit; // conflicts
p->DelayMax = DelayMax; // external delay
p->nEdges = nEdges; // the number of edges
p->fDelay = fDelay; // delay mode
p->fReverse = fReverse; // reverse windowing
p->fVeryVerbose = fVeryVerbose; // verbose
p->fVerbose = fVerbose | fVeryVerbose;
Gia_ManComputeOneWinStart( pGia, fReverse );
Gia_ManForEachLut2( pGia, iLut )
{
// if ( iLut > 259 )
// break;
if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, nEdges, fDelay, fVeryVerbose, fVerbose ) != 2 )
if ( Sbl_ManTestSat( p, iLut ) != 2 )
continue;
// break;
if ( ++nImproveCount == nImproves )
break;
}
Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
Sbl_ManPrintRuntime( p );
Sbl_ManStop( p );
}
////////////////////////////////////////////////////////////////////////

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

@ -34827,11 +34827,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
int c, nNumber = 64, nBTLimit = 500, DelayMax = 0, nEdges = 0;
extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
int c, nNumber = 64, nImproves = 0, nBTLimit = 500, DelayMax = 0, nEdges = 0;
int fDelay = 0, fReverse = 0, fVeryVerbose = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NCDQdrwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NICDQdrwvh" ) ) != EOF )
{
switch ( c )
{
@ -34843,11 +34843,15 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
}
nNumber = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nNumber < 2 )
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Illigal number of AIG nodes.\n" );
Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
nImproves = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'C':
if ( globalUtilOptind >= argc )
@ -34907,13 +34911,14 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 )
Abc_Print( 0, "Current AIG is mapped into %d-LUTs (only 4-LUT mapping is currently supported).\n", Gia_ManLutSizeMax(pAbc->pGia) );
else
Gia_ManLutSat( pAbc->pGia, nNumber, nBTLimit, DelayMax, nEdges, fDelay, fReverse, fVeryVerbose, fVerbose );
Gia_ManLutSat( pAbc->pGia, nNumber, nImproves, nBTLimit, DelayMax, nEdges, fDelay, fReverse, fVeryVerbose, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &satlut [-NCDQ num] [-drwvh]\n" );
Abc_Print( -2, "usage: &satlut [-NICDQ num] [-drwvh]\n" );
Abc_Print( -2, "\t performs SAT-based remapping of the 4-LUT network\n" );
Abc_Print( -2, "\t-N num : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber );
Abc_Print( -2, "\t-I num : the limit on the number of improved windows [default = %d]\n", nImproves );
Abc_Print( -2, "\t-C num : the limit on the number of conflicts [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-D num : the user-specified required times at the outputs [default = %d]\n", DelayMax );
Abc_Print( -2, "\t-Q num : the maximum number of edges [default = %d]\n", nEdges );

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

@ -1452,8 +1452,15 @@ void sat_solver_rollback( sat_solver* s )
{
cla* pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( Sat_MemClauseUsed(pMem, pArray[k]) )
{
if ( clause_is_lit(pArray[k]) )
{
if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 )
pArray[j++] = pArray[k];
}
else if ( Sat_MemClauseUsed(pMem, pArray[k]) )
pArray[j++] = pArray[k];
}
veci_resize(&s->wlists[i],j);
}
// reset watcher lists