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

Updates to delay optimization project.

This commit is contained in:
Alan Mishchenko 2016-12-27 18:08:39 +07:00
parent ac3216cf23
commit 398c4ec92c
4 changed files with 254 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

158
src/opt/sbd/sbdCore.c
View File

@ -777,15 +777,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
} }
} }
void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows ) void Sbd_ManMatrPrint( Sbd_Man_t * p, word Cover[], int nCol, int nRows )
{ {
int i, k; int i, k;
for ( i = 0; i <= nCol; i++ ) for ( i = 0; i <= nCol; i++ )
{ {
printf( "%2d : ", i ); printf( "%2d : ", i );
printf( "%d ", i == nCol ? Vec_IntEntry(p->vLutLevs, p->Pivot) : Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
for ( k = 0; k < nRows; k++ ) for ( k = 0; k < nRows; k++ )
for ( k = 0; k < nRows; k++ ) printf( "%d", (int)((Cover[i] >> k) & 1) );
printf( "%d", (int)((Cover[i] >> k) & 1) );
printf( "\n"); printf( "\n");
} }
printf( "\n"); printf( "\n");
@ -801,18 +801,18 @@ static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
} }
} }
static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube ) static inline int Sbd_ManAddCube1( int nRowLimit, word Cover[], int nRows, word Cube )
{ {
int n, m; int n, m;
if ( 0 ) if ( 0 )
{ {
printf( "Adding cube: " ); printf( "Adding cube: " );
for ( n = 0; n < 64; n++ ) for ( n = 0; n < nRowLimit; n++ )
printf( "%d", (int)((Cube >> n) & 1) ); printf( "%d", (int)((Cube >> n) & 1) );
printf( "\n" ); printf( "\n" );
} }
// do not add contained Cube // do not add contained Cube
assert( nRows <= 64 ); assert( nRows <= nRowLimit );
for ( n = 0; n < nRows; n++ ) for ( n = 0; n < nRows; n++ )
if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
return nRows; return nRows;
@ -820,7 +820,7 @@ static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
for ( n = m = 0; n < nRows; n++ ) for ( n = m = 0; n < nRows; n++ )
if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained
Cover[m++] = Cover[n]; Cover[m++] = Cover[n];
if ( m < 64 ) if ( m < nRowLimit )
Cover[m++] = Cube; Cover[m++] = Cube;
for ( n = m; n < nRows; n++ ) for ( n = m; n < nRows; n++ )
Cover[n] = 0; Cover[n] = 0;
@ -855,7 +855,7 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
return nRows; return nRows;
} }
static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs ) static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[], int nDivs )
{ {
int c0, c1, c2, c3; int c0, c1, c2, c3;
word Target = Cover[nDivs]; word Target = Cover[nDivs];
@ -1052,7 +1052,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{ {
Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]); Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
assert( Cube ); assert( Cube );
nRows = Sbd_ManAddCube1( Cover, nRows, Cube ); nRows = Sbd_ManAddCube1( 64, Cover, nRows, Cube );
} }
Sbd_ManCoverReverseOrder( Cover ); Sbd_ManCoverReverseOrder( Cover );
@ -1072,7 +1072,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ ) for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Sbd_ManMatrPrint( Cover, nDivs, nRows ); Sbd_ManMatrPrint( p, Cover, nDivs, nRows );
clk = Abc_Clock(); clk = Abc_Clock();
if ( !Sbd_ManFindCands( p, Cover, nDivs ) ) if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
@ -1141,10 +1141,123 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
return RetValue; return RetValue;
} }
int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
int nLuts, int nSels, int nVarsDivs[SBD_LUTS_MAX],
int pVarsDivs[SBD_LUTS_MAX][SBD_SIZE_MAX], word Truths[SBD_LUTS_MAX] )
{ {
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
abctime clk = Abc_Clock();
word Onset[64] = {0}, Offset[64] = {0}, Cube;
word CoverRows[256] = {0}, CoverCols[64] = {{0}};
int nIters, nItersMax = 32;
int i, k, nRows = 0;
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
int nDivs = Vec_IntSize( p->vDivVars );
int nConsts = 4;
int RetValue;
if ( p->pSat )
sat_solver_delete( p->pSat );
p->pSat = NULL;
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
assert( nConsts <= 8 );
RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
if ( RetValue >= 0 )
{
if ( p->pPars->fVerbose )
printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
p->nConsts++;
return RetValue;
}
// create rows of the table
nRows = 0;
for ( i = 0; i < nConsts; i++ )
for ( k = 0; k < nConsts; k++ )
{
Cube = Onset[i] ^ Offset[k];
assert( Cube );
nRows = Sbd_ManAddCube1( 256, CoverRows, nRows, Cube );
}
assert( nRows <= 64 );
// create columns of the table
for ( i = 0; i < nRows; i++ )
for ( k = 0; k <= nDivs; k++ )
if ( (CoverRows[i] >> k) & 1 )
Abc_TtXorBit(&CoverCols[k], i);
// solve the covering problem
for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
{
if ( p->pPars->fVerbose )
Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
clk = Abc_Clock();
if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) )
{
if ( p->pPars->fVerbose )
printf( "Cannot find a feasible cover.\n" );
//clkEnu += Abc_Clock() - clk;
//clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
//p->timeSat += clkSat;
//p->timeCov += clkAll;
//p->timeEnu += clkEnu;
return 0;
}
//clkEnu += Abc_Clock() - clk;
if ( p->pPars->fVerbose )
printf( "Candidate support: " ),
Vec_IntPrint( p->vDivSet );
clk = Abc_Clock();
*pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
//clkSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
else if ( *pTruth == SBD_SAT_SAT )
{
if ( p->pPars->fVerbose )
{
int i;
printf( "Node %d: SAT.\n", Pivot );
for ( i = 0; i < nDivs; i++ )
printf( "%d", Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
printf( "\n" );
for ( i = 0; i < nDivs; i++ )
printf( "%d", i % 10 );
printf( "\n" );
for ( i = 0; i < nDivs; i++ )
printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
printf( "\n" );
for ( i = 0; i < nDivs; i++ )
printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
printf( "\n" );
}
// add row to the covering table
for ( i = 0; i < nDivs; i++ )
if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
CoverCols[i] |= ((word)1 << nRows);
CoverCols[nDivs] |= ((word)1 << nRows);
nRows++;
}
else
{
if ( p->pPars->fVerbose )
{
printf( "Node %d: UNSAT. ", Pivot );
Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
}
return 1;
}
}
return 0; return 0;
} }
@ -1465,7 +1578,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
if ( Sbd_ManMergeCuts( p, Pivot ) ) if ( Sbd_ManMergeCuts( p, Pivot ) )
return; return;
// if ( Pivot != 13 ) // if ( Pivot != 70 )
// return; // return;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
@ -1481,7 +1594,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue ); Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
//printf( " --> Pivot %4d. Constant %d.\n", Pivot, RetValue ); //printf( " --> Pivot %4d. Constant %d.\n", Pivot, RetValue );
} }
else if ( Sbd_ManExplore( p, Pivot, &Truth ) ) else if ( Sbd_ManExplore2( p, Pivot, &Truth ) )
{ {
Sbd_ManImplement( p, Pivot, Truth ); Sbd_ManImplement( p, Pivot, Truth );
//printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) ); //printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
@ -1493,26 +1606,23 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
Gia_Man_t * p, Vec_Int_t * vMirrors, Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots, Vec_Int_t * vTfo, Vec_Int_t * vRoots,
Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0, word Truths[SBD_LUTS_MAX] Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0
); );
Sbd_Str_t Strs[2] = { // Sbd_Str_t Strs[2] = { {1, 4, {0, 1, 2, 8}}, {1, 4, {3, 4, 5, 6}} };
{1, 4, {0, 1, 2, 7}}, // Sbd_Str_t Strs[2] = { {1, 4, {1, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}} };
{1, 4, {3, 4, 5, 6}} Sbd_Str_t Strs[3] = { {1, 4, {8, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}}, {0, 4, {0, 1, 2, 3}} };
};
word Truths[SBD_LUTS_MAX];
Vec_Int_t * vDivSet = Vec_IntAlloc( 8 ); Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
int i, RetValue; int i, RetValue;
for ( i = 0; i < 7; i++ ) for ( i = 0; i < 6; i++ )
Vec_IntPush( vDivSet, i+1 ); Vec_IntPush( vDivSet, i+1 );
RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,
Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
vDivSet, 2, Strs, Truths ); vDivSet, 3, Strs );
if ( RetValue ) if ( RetValue )
{ {
printf( "Solving succeded.\n" ); printf( "Solving succeded.\n" );

1
src/opt/sbd/sbdInt.h
View File

@ -66,6 +66,7 @@ struct Sbd_Str_t_
int fLut; // LUT or SEL int fLut; // LUT or SEL
int nVarIns; // input count int nVarIns; // input count
int VarIns[SBD_DIV_MAX]; // input vars int VarIns[SBD_DIV_MAX]; // input vars
word Res; // result of solving
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

108
src/opt/sbd/sbdLut.c
View File

@ -19,6 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "sbdInt.h" #include "sbdInt.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
@ -46,17 +47,18 @@ int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 )
{ {
Sbd_Str_t * pStr; int nPars = 0; Sbd_Str_t * pStr; int nPars = 0;
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
nPars += (pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns); nPars += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
return nPars; return nPars;
} }
// add clauses for the structure // add clauses for the structure
void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
{ {
// variable order: inputs, structure outputs, parameters // variable order: inputs, structure outputs, parameters
Sbd_Str_t * pStr; Sbd_Str_t * pStr;
int VarOut = nVars; int VarOut = nVars;
int VarPar = nVars + nStrs; int VarPar = nVars + nStrs;
int m, k, n, status, pLits[SBD_SIZE_MAX+2]; int m, k, n, status, pLits[SBD_SIZE_MAX+2];
//printf( "Start par = %d. ", VarPar );
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ ) for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ )
{ {
if ( pStr->fLut ) if ( pStr->fLut )
@ -72,12 +74,14 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars
pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n ); pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n );
pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n ); pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n );
status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 ); status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 );
assert( status ); if ( !status )
return 0;
} }
} }
} }
else else
{ {
assert( pStr->nVarIns <= SBD_DIV_MAX );
for ( k = 0; k < pStr->nVarIns; k++, VarPar++ ) for ( k = 0; k < pStr->nVarIns; k++, VarPar++ )
{ {
for ( n = 0; n < 2; n++ ) for ( n = 0; n < 2; n++ )
@ -86,22 +90,32 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars
pLits[1] = Abc_Var2Lit( pVars[VarOut], n ); pLits[1] = Abc_Var2Lit( pVars[VarOut], n );
pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n ); pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n );
status = sat_solver_addclause( pSat, pLits, pLits + 3 ); status = sat_solver_addclause( pSat, pLits, pLits + 3 );
assert( status ); if ( !status )
return 0;
} }
} }
} }
} }
//printf( "Stop par = %d.\n", VarPar );
return 1;
} }
void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
{ {
Sbd_Str_t * pStr; Sbd_Str_t * pStr;
int VarPar = nVars + nStrs; int VarPar = nVars + nStrs;
int m, m2, pLits[2], status; int m, m2, status, pLits[SBD_DIV_MAX];
// make sure selector parameters are mutually exclusive // make sure selector parameters are mutually exclusive
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarPar = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns ) for ( pStr = pStr0; pStr < pStr0 + nStrs; VarPar += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns, pStr++ )
{ {
if ( pStr->fLut ) if ( pStr->fLut )
continue; continue;
// one variable should be selected
assert( pStr->nVarIns <= SBD_DIV_MAX );
for ( m = 0; m < pStr->nVarIns; m++ )
pLits[m] = Abc_Var2Lit( pVars[VarPar + m], 0 );
status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns );
assert( status );
// two variables cannot be selected
for ( m = 0; m < pStr->nVarIns; m++ ) for ( m = 0; m < pStr->nVarIns; m++ )
for ( m2 = m+1; m2 < pStr->nVarIns; m2++ ) for ( m2 = m+1; m2 < pStr->nVarIns; m2++ )
{ {
@ -120,15 +134,44 @@ void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
{ {
nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns; nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", pStr-pStr0 ); printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", (int)(pStr-pStr0) );
for ( m = 0; m < nIters; m++ ) for ( m = 0; m < nIters; m++, iLit++ )
printf( "%d", Abc_LitIsCompl(Vec_IntEntry(vLits, iLit++)) ); printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) );
printf( "\n" ); printf( " {" );
for ( m = 0; m < pStr->nVarIns; m++ )
printf( " %d", pStr->VarIns[m] );
printf( " }\n" );
} }
assert( iLit == Vec_IntSize(vLits) ); assert( iLit == Vec_IntSize(vLits) );
} }
void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits, word Truths[SBD_LUTS_MAX] ) void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
{ {
Sbd_Str_t * pStr;
int m, nIters, iLit = 0;
for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
{
pStr->Res = 0;
if ( pStr->fLut )
{
nIters = 1 << pStr->nVarIns;
for ( m = 0; m < nIters; m++, iLit++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
Abc_TtSetBit( &pStr->Res, m );
Abc_TtStretch6( &pStr->Res, pStr->nVarIns, 6 );
}
else
{
nIters = 0;
for ( m = 0; m < pStr->nVarIns; m++, iLit++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
{
pStr->Res = pStr->VarIns[m];
nIters++;
}
assert( nIters == 1 );
}
}
assert( iLit == Vec_IntSize(vLits) );
} }
/**Function************************************************************* /**Function*************************************************************
@ -145,38 +188,39 @@ void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits
int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
Vec_Int_t * vTfo, Vec_Int_t * vRoots, Vec_Int_t * vTfo, Vec_Int_t * vRoots,
Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0, word Truths[SBD_LUTS_MAX] ) // divisors, structures Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 ) // divisors, structures
{ {
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
int fVerbose = 1;
Vec_Int_t * vLits = Vec_IntAlloc( 100 ); Vec_Int_t * vLits = Vec_IntAlloc( 100 );
sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 ); sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
sat_solver * pSatQbf = sat_solver_new(); sat_solver * pSatQbf = sat_solver_new();
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
int nVars = Vec_IntSize( vDivSet ); int nVars = Vec_IntSize( vDivSet );
int nPars = Sbd_ProblemCountParams( nStrs, pStr0 ); int nPars = Sbd_ProblemCountParams( nStrs, pStr0 );
int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots); int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
int VarCecPar = VarCecOut + 1; int VarCecPar = VarCecOut + nStrs;
int VarCecFree = VarCecPar + nPars;
int VarQbfPar = 0; int VarQbfPar = 0;
int VarQbfFree = nPars; int VarQbfFree = nPars;
int pVarsCec[256]; int pVarsCec[256];
int pVarsQbf[256]; int pVarsQbf[256];
int i, iVar, iLit; int i, iVar, iLit, nIters;
int RetValue = 0; int RetValue = 0;
assert( Vec_IntSize(vDivSet) <= SBD_SIZE_MAX ); assert( Vec_IntSize(vDivSet) <= SBD_DIV_MAX );
assert( nVars + nStrs + nPars <= 256 ); assert( nVars + nStrs + nPars <= 256 );
// collect CEC variables // collect CEC variables
Vec_IntForEachEntry( vDivSet, iVar, i ) Vec_IntForEachEntry( vDivSet, iVar, i )
pVarsCec[i] = iVar; pVarsCec[i] = iVar;
pVarsCec[nVars] = VarCecOut; for ( i = 0; i < nStrs; i++ )
for ( i = 1; i < nStrs; i++ ) pVarsCec[nVars + i] = VarCecOut + i;
pVarsCec[nVars + i] = VarCecFree++;
for ( i = 0; i < nPars; i++ ) for ( i = 0; i < nPars; i++ )
pVarsCec[nVars + nStrs + i] = VarCecPar + i; pVarsCec[nVars + nStrs + i] = VarCecPar + i;
@ -197,13 +241,24 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
Vec_IntClear( vLits ); Vec_IntClear( vLits );
for ( i = 0; i < nPars; i++ ) for ( i = 0; i < nPars; i++ )
Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) ); Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
while ( 1 ) for ( nIters = 0; nIters < (1 << nVars); nIters++ )
{ {
// check if these parameters solve the problem // check if these parameters solve the problem
int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 ); int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
if ( status == l_False ) // solution found if ( status == l_False ) // solution found
break; break;
assert( status == l_True ); assert( status == l_True );
// Vec_IntForEachEntry( vWinObjs, iVar, i )
// printf( "Node = %4d. SatVar = %4d. Value = %d.\n", iVar, i, sat_solver_var_value(pSatCec, i) );
if ( fVerbose )
{
printf( "Iter %3d : ", nIters );
for ( i = 0; i < nPars; i++ )
printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) );
printf( " " );
}
Vec_IntClear( vLits ); Vec_IntClear( vLits );
// create new QBF variables // create new QBF variables
for ( i = 0; i < nVars + nStrs; i++ ) for ( i = 0; i < nVars + nStrs; i++ )
@ -211,15 +266,20 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
// set their values // set their values
Vec_IntForEachEntry( vDivSet, iVar, i ) Vec_IntForEachEntry( vDivSet, iVar, i )
{ {
iLit = Abc_Var2Lit( pVarsQbf[i], sat_solver_var_value(pSatCec, iVar) ); iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) );
status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
assert( status ); assert( status );
if ( fVerbose )
printf( "%d", sat_solver_var_value(pSatCec, iVar) );
} }
iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) ); iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
assert( status ); assert( status );
if ( fVerbose )
printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) );
// add clauses to the QBF problem // add clauses to the QBF problem
Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ); if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) )
break; // solution does not exist
// check if solution still exists // check if solution still exists
status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 ); status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_False ) // solution does not exist if ( status == l_False ) // solution does not exist
@ -228,12 +288,12 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
// find the new values of parameters // find the new values of parameters
assert( Vec_IntSize(vLits) == 0 ); assert( Vec_IntSize(vLits) == 0 );
for ( i = 0; i < nPars; i++ ) for ( i = 0; i < nPars; i++ )
Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, sat_solver_var_value(pSatQbf, VarQbfPar + i)) ); Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, !sat_solver_var_value(pSatQbf, VarQbfPar + i)) );
} }
if ( Vec_IntSize(vLits) > 0 ) if ( Vec_IntSize(vLits) > 0 )
{ {
Sbd_ProblemPrintSolution( nStrs, pStr0, vLits ); Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
Sbd_ProblemCollectSolution( nStrs, pStr0, vLits, Truths ); Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
RetValue = 1; RetValue = 1;
} }
else else

35
src/opt/sbd/sbdWin.c
View File

@ -141,6 +141,17 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
} }
assert( sat_solver_nvars(pSat) == nVars + nAddVars ); assert( sat_solver_nvars(pSat) == nVars + nAddVars );
} }
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 );
}
}
// finalize // finalize
RetValue = sat_solver_simplify( pSat ); RetValue = sat_solver_simplify( pSat );
if ( RetValue == 0 ) if ( RetValue == 0 )
@ -418,6 +429,30 @@ int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar,
return -1; return -1;
} }
int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )
{
int nBTLimit = 0;
int n, i, k, status, iLit, iVar;
word * pPats[2] = {pOnset, pOffset};
assert( Vec_IntSize(vDivVars) < 64 );
for ( n = 0; n < 2; n++ )
for ( i = 0; i < nConsts; i++ )
{
sat_solver_random_polarity( pSat );
iLit = Abc_Var2Lit( PivotVar, n );
status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -2;
if ( status == l_False )
return n;
pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
Vec_IntForEachEntry( vDivVars, iVar, k )
if ( sat_solver_var_value(pSat, iVar) )
Abc_TtXorBit(&pPats[n][i], k);
}
return -1;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///