/**CFile****************************************************************
FileName [sbd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MAX_M 8 // max inputs
#define MAX_N 30 // max nodes
#define MAX_K 6 // max lutsize
#define MAX_D 8 // max delays
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// new AIG manager
typedef struct Sbd_Pro_t_ Sbd_Pro_t;
struct Sbd_Pro_t_
{
int nLuts; // LUT count
int nSize; // LUT size
int nDivs; // divisor count
int nVars; // intermediate variables (nLuts * nSize)
int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs)
int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters
int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters
int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables
int pDivs[SBD_DIV_MAX]; // divisor variables (external)
};
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
{
Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
int i, k, d, v, n, iVar = 0;
assert( nLuts >= 1 && nLuts <= 2 );
memset( p, 0, sizeof(Sbd_Pro_t) );
p->nLuts = nLuts;
p->nSize = nSize;
p->nDivs = nDivs;
p->nVars = nLuts * nSize;
p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
// set parameters
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < (1 << nSize); k++ )
p->pPars1[i][k] = iVar++;
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
p->pPars2[i][k][d] = iVar++;
// set intermediate variables
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < nSize; k++ )
p->pVars[i][k] = iVar++;
// set top variables
for ( i = 1; i < nLuts; i++ )
p->pVars[i][nSize] = p->pVars[i-1][0];
// set divisor variables
for ( d = 0; d < nDivs; d++ )
p->pDivs[d] = iVar++;
assert( iVar == p->nPars + p->nVars + p->nDivs );
// input compatiblity clauses
for ( i = 0; i < nLuts; i++ )
for ( k = (i > 0); k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
for ( n = 0; n < nDivs; n++ )
{
if ( n < d )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
Vec_IntPush( vCnf, -1 );
}
else if ( k < nSize-1 )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
Vec_IntPush( vCnf, -1 );
}
}
// create LUT clauses
for ( i = 0; i < nLuts; i++ )
for ( k = 0; k < (1 << nSize); k++ )
for ( n = 0; n < 2; n++ )
{
for ( v = 0; v < nSize; v++ )
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
Vec_IntPush( vCnf, -1 );
}
// create input clauses
for ( i = 0; i < nLuts; i++ )
for ( k = (i > 0); k < nSize; k++ )
for ( d = 0; d < nDivs; d++ )
for ( n = 0; n < 2; n++ )
{
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
Vec_IntPush( vCnf, -1 );
}
return vCnf;
}
// add clauses to the don't-care computation solver
void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
{
int pLits[8], nLits, i, k, iLit, RetValue;
int ThisTopVar = p->pVars[0][p->nSize];
int FirstDivVar = p->nPars + p->nVars;
// add clauses
for ( i = 0; i < Vec_IntSize(vCnf); i++ )
{
assert( Vec_IntEntry(vCnf, i) != -1 );
for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
if ( Vec_IntEntry(vCnf, i) == -1 )
break;
nLits = 0;
Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
if ( Abc_Lit2Var(iLit) == ThisTopVar )
pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
else
pLits[nLits++] = iLit + 2 * iStartVar;
}
assert( nLits <= 8 );
RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
assert( RetValue );
}
}
// add clauses to the functionality evaluation solver
void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
{
Vec_Int_t * vLevel;
int pLits[8], nLits, i, k, iLit, RetValue;
int ThisTopVar = p->pVars[0][p->nSize];
int FirstDivVar = p->nPars + p->nVars;
int FirstIntVar = p->nPars;
// add clauses
Vec_WecForEachLevel( vCnf, vLevel, i )
{
nLits = 0;
Vec_IntForEachEntry( vLevel, iLit, k ) {
if ( Abc_Lit2Var(iLit) == ThisTopVar )
{
if ( Abc_LitIsCompl(iLit) == iTopVarValue )
break;
continue;
}
else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
{
if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
break;
continue;
}
else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
pLits[nLits++] = iLit + 2 * iStartVar;
else
pLits[nLits++] = iLit;
}
if ( k < Vec_IntSize(vLevel) )
continue;
assert( nLits <= 8 );
RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
assert( RetValue );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize
{
sat_solver * pSat = NULL;
Vec_Int_t * vTemp = Vec_IntAlloc(100);
// assign vars
int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+N; i++ )
for ( k = 0; k < K; k++ )
pVars[n][i][k] = -1;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
pVars[n][i][k] = nVars++;
printf( "Number of topo vars = %d.\n", nVars );
*pnVars = nVars;
// add constraints
pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
// each node is used
for ( i = 0; i < M+N-1; i++ )
{
Vec_IntClear( vTemp );
for ( n = 0; n < N; n++ )
for ( k = 0; k < K; k++ )
if ( pVars[n][i][k] >= 0 )
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
printf( "Added %d node connectivity constraints.\n", i );
// each fanin of each node is connected exactly once
Count = 0;
for ( n = 0; n < N; n++ )
for ( k = 0; k < K; k++ )
{
// connected
Vec_IntClear( vTemp );
for ( i = 0; i < M+n; i++ )
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
// exactly once
for ( i = 0; i < M+n; i++ )
for ( j = i+1; j < M+n; j++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
}
printf( "Added %d fanin connectivity constraints.\n", Count );
// node fanins are unique
Count = 0;
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
for ( j = i; j < M+n; j++ )
for ( k2 = k+1; k2 < K; k2++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
printf( "Added %d fanin exclusivity constraints.\n", Count );
// nodes are ordered
Count = 0;
for ( n = 1; n < N; n++ )
for ( i = 0; i < M+n-1; i++ )
{
// first of n cannot be smaller than first of n-1 (but can be equal)
for ( j = i+1; j < M+n-1; j++ )
{
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
// if first nodes of n and n-1 are equal, second nodes are ordered
Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) );
for ( j = 0; j < i; j++ )
for ( j2 = j+1; j2 < i; j2++ )
{
Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Vec_IntShrink( vTemp, 2 );
Count++;
}
}
printf( "Added %d node ordering constraints.\n", Count );
// exclude fanins of two-input nodes
Count = 0;
if ( K == 2 )
for ( n = 1; n < N; n++ )
for ( i = M; i < M+n; i++ )
for ( j = 0; j < i; j++ )
for ( k = 0; k < K; k++ )
{
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
Count++;
}
printf( "Added %d two-node non-triviality constraints.\n", Count );
// assign delay vars
assert( Req < MAX_D-1 );
for ( i = 0; i < M+N; i++ )
for ( d = 0; d < MAX_D; d++ )
pVars2[i][d] = nVars++;
printf( "Number of total vars = %d.\n", nVars );
// set input delays
for ( i = 0; i < M; i++ )
{
assert( pDelays[i] < MAX_D-2 );
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
// set output delay
for ( k = Req; k < MAX_D; k++ )
{
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
// set internal nodes
for ( n = 0; n < N; n++ )
for ( i = 0; i < M+n; i++ )
for ( k = 0; k < K; k++ )
for ( d = 0; d < MAX_D-1; d++ )
{
Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) );
Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
assert( RetValue );
}
Vec_IntFree( vTemp );
return pSat;
}
void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
{
int n, i, k;
printf( "Solution:\n" );
printf( " | " );
for ( n = 0; n < N; n++ )
printf( "%2d ", M+n );
printf( "\n" );
for ( i = M+N-2; i >= 0; i-- )
{
printf( "%2d %c | ", i, i < M ? 'i' : ' ' );
for ( n = 0; n < N; n++ )
{
for ( k = K-1; k >= 0; k-- )
if ( pVars[n][i][k] == -1 )
printf( " " );
else
printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
printf( " " );
}
printf( "\n" );
}
}
void Sbd_SolverTopoTest()
{
int M = 8; // 6; // inputs
int N = 3; // 16; // nodes
int K = 4; // 2; // lutsize
int status, v, nVars, nIter, nSols = 0;
int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840
int pDelays[MAX_M] = {1,0,0,0,1};
abctime clk = Abc_Clock();
Vec_Int_t * vLits = Vec_IntAlloc(100);
sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars );
for ( nIter = 0; nIter < 1000000; nIter++ )
{
// find onset minterm
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_Undef )
break;
if ( status == l_False )
break;
assert( status == l_True );
nSols++;
// print solution
if ( nIter < 5 )
Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
// remember variable values
Vec_IntClear( vLits );
for ( v = 0; v < nVars; v++ )
if ( sat_solver_var_value(pSat, v) )
Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
// add breaking clause
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
if ( status == 0 )
break;
//if ( nIter == 5 )
// break;
}
sat_solver_delete( pSat );
Vec_IntFree( vLits );
printf( "Found %d solutions. ", nSols );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis [Synthesize random topology.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] )
{
int Used[MAX_M+MAX_N] = {0};
int nUnused = M;
int n, iFan0, iFan1;
srand( time(NULL) );
for ( n = 0; nUnused < N - n; n++ )
{
iFan0 = iFan1 = 0;
while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) )
;
pLuts[n][0] = iFan0;
pLuts[n][1] = iFan1;
if ( Used[iFan0] == 0 )
{
Used[iFan0] = 1;
nUnused--;
}
if ( Used[iFan1] == 0 )
{
Used[iFan1] = 1;
nUnused--;
}
nUnused++;
}
if ( nUnused == N - n )
{
// undo the first one
for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
if ( Used[iFan0] )
{
Used[iFan0] = 0;
nUnused++;
break;
}
}
assert( nUnused == N - n + 1 );
for ( ; n < N; n++ )
{
for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
if ( Used[iFan0] == 0 )
{
Used[iFan0] = 1;
break;
}
assert( iFan0 < M+n );
for ( iFan1 = 0; iFan1 < M+n; iFan1++ )
if ( Used[iFan1] == 0 )
{
Used[iFan1] = 1;
break;
}
assert( iFan1 < M+n );
pLuts[n][0] = iFan0;
pLuts[n][1] = iFan1;
}
printf( "{\n" );
for ( n = 0; n < N; n++ )
printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n );
printf( "};\n" );
}
/**Function*************************************************************
Synopsis [Compute truth table for the given parameter settings.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] )
{
int i, k, v, nLutPars = (1 << K) - 1;
word Truths[MAX_M+MAX_N];
assert( M <= 6 && N <= MAX_N );
for ( i = 0; i < M; i++ )
Truths[i] = s_Truths6[i];
for ( i = 0; i < N; i++ )
{
word Truth = 0, Mint;
for ( k = 1; k <= nLutPars; k++ )
{
if ( !pValues[i*nLutPars+k-1] )
continue;
Mint = ~(word)0;
for ( v = 0; v < K; v++ )
Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] : ~Truths[pLuts[i][v]];
Truth |= Mint;
}
Truths[M+i] = Truth;
}
return Truths[M+N-1];
}
word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl )
{
int i, k, v, nLutPars = (1 << K) - 1;
int nWords = Abc_TtWordNum( M );
word * pRes = pTruthsElem + (M+N-1)*nWords;
assert( M <= MAX_M && N <= MAX_N );
for ( i = 0; i < N; i++ )
{
word * pMint, * pTruth = pTruthsElem + (M+i)*nWords;
Abc_TtClear( pTruth, nWords );
for ( k = 1; k <= nLutPars; k++ )
{
if ( !pValues[i*nLutPars+k-1] )
continue;
pMint = pTruthsElem + (M+N)*nWords;
Abc_TtFill( pMint, nWords );
for ( v = 0; v < K; v++ )
{
word * pFanin = pTruthsElem + pLuts[i][v]*nWords;
Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 );
}
Abc_TtOr( pTruth, pTruth, pMint, nWords );
}
}
if ( fCompl )
Abc_TtNot( pRes, nWords );
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues )
{
int fVerbose = 0;
abctime clk = Abc_Clock();
abctime clk2, clkOther = 0;
sat_solver * pSat = NULL;
int nWords = Abc_TtWordNum(M);
int pLits[MAX_K+2], pLits2[MAX_K+2], nLits;
int nLutPars = (1 << K) - 1, nVars = N * nLutPars;
int i, k, m, status, iMint, Iter, fCompl = (int)(pTruthInit[0] & 1);
// create truth tables
word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) );
Abc_TtElemInit2( pTruths, M );
// create solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
// start with the last minterm
// iMint = (1 << M) - 1;
iMint = 1;
for ( Iter = 0; Iter < (1 << M); Iter++ )
{
// assign the first intermediate variable
int nVarStart = sat_solver_nvars(pSat);
sat_solver_setnvars( pSat, nVarStart + N - 1 );
// add clauses for nodes
//if ( fVerbose )
printf( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) );
for ( i = 0; i < N; i++ )
for ( m = 0; m <= nLutPars; m++ )
{
if ( fVerbose )
printf( "i = %d. m = %d.\n", i, m );
// selector variables
nLits = 0;
for ( k = 0; k < K; k++ )
{
if ( pLuts[i][k] >= M )
{
assert( pLuts[i][k] - M < N - 1 );
pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 );
nLits++;
}
else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) )
break;
}
if ( k < K )
continue;
// add parameter
if ( m )
{
pLits[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 1 );
pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 );
nLits++;
}
// node variable
if ( i != N - 1 )
{
pLits[nLits] = Abc_Var2Lit( nVarStart + i, 0 );
pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 );
nLits++;
}
// add clauses
if ( i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) != fCompl )
{
status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
if ( status == 0 )
{
fCompl = -1;
goto finish;
}
}
if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == fCompl) && m > 0 )
{
status = sat_solver_addclause( pSat, pLits, pLits + nLits );
if ( status == 0 )
{
fCompl = -1;
goto finish;
}
}
}
// run SAT solver
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status == l_Undef )
break;
if ( status == l_False )
{
fCompl = -1;
goto finish;
}
assert( status == l_True );
// collect values
for ( i = 0; i < nVars; i++ )
pValues[i] = sat_solver_var_value(pSat, i);
clk2 = Abc_Clock();
pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl );
clkOther += Abc_Clock() - clk2;
if ( fVerbose )
{
for ( i = 0; i < nVars; i++ )
printf( "%d=%d ", i, pValues[i] );
printf( " " );
for ( i = nVars; i < sat_solver_nvars(pSat); i++ )
printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pTruthInit, (1 << M) ); printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" );
}
if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) )
break;
// get new minterm
iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M );
}
finish:
printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) );
sat_solver_delete( pSat );
ABC_FREE( pTruths );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time", clkOther );
return fCompl;
}
void Sbd_SolverFuncTest()
{
// int M = 4; // 6; // inputs
// int N = 3; // 16; // nodes
// int K = 2; // 2; // lutsize
// word Truth = ~((word)3 << 8);
// int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
/*
int M = 6; // 6; // inputs
int N = 19; // 16; // nodes
int K = 2; // 2; // lutsize
word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 };
int pLuts[MAX_N][MAX_K] = {
{3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9},
{0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14},
{10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13},
{20, 7}, {19, 21}, {4, 16}, {23, 22}
};
*/
/*
int M = 6; // 6; // inputs
int N = 5; // 16; // nodes
int K = 4; // 2; // lutsize
word Truth = ABC_CONST(0x9ef7a8d9c7193a0f);
int pLuts[MAX_N][MAX_K] = {
{0, 1, 2, 3}, // 6
{1, 2, 3, 4}, // 7
{2, 3, 4, 5}, // 8
{0, 1, 4, 5}, // 9
{6, 7, 8, 9} // 10
};
*/
/*
int M = 8; // 6; // inputs
int N = 7; // 16; // nodes
int K = 2; // 2; // lutsize
// word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) };
// word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 };
word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) };
int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
*/
int M = 8; // 6; // inputs
int N = 7; // 16; // nodes
int K = 2; // 2; // lutsize
word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) };
int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
int pValues[MAX_N*((1<<MAX_K)-1)];
int Res, i, k, nLutPars = (1 << K) - 1;
//Sbd_SolverSynth( M, N, K, pLuts );
Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, pValues );
if ( Res == -1 )
{
printf( "Solution does not exist.\n" );
return;
}
printf( "Result (compl = %d):\n", Res );
for ( i = 0; i < N; i++ )
{
for ( k = nLutPars-1; k >= 0; k-- )
printf( "%d", pValues[i*nLutPars+k] );
printf( "0\n" );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END