summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaSatLut.c399
-rw-r--r--src/base/abci/abc.c19
-rw-r--r--src/sat/bsat/satSolver.c9
3 files changed, 269 insertions, 158 deletions
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index 44b5e2e1..23d1b407 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -33,49 +33,193 @@ 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.]
Description []
@@ -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 )
+{
+ 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;
+ 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 );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 771f2028..ff101930 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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 );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1a10ff88..58f2ed21 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 06:36:31 +0000