mirror of https://github.com/YosysHQ/abc.git
549 lines
21 KiB
C
549 lines
21 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [ifSat.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [FPGA mapping based on priority cuts.]
|
|
|
|
Synopsis [SAT-based evaluation.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - November 21, 2006.]
|
|
|
|
Revision [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "if.h"
|
|
#include "sat/bsat/satSolver.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Builds SAT instance for the given structure.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void * If_ManSatBuildXY( int nLutSize )
|
|
{
|
|
int nMintsL = (1 << nLutSize);
|
|
int nMintsF = (1 << (2 * nLutSize - 1));
|
|
int nVars = 2 * nMintsL + nMintsF;
|
|
int iVarP0 = 0; // LUT0 parameters (total nMintsL)
|
|
int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
|
|
int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF)
|
|
sat_solver * p = sat_solver_new();
|
|
sat_solver_setnvars( p, nVars );
|
|
for ( m = 0; m < nMintsF; m++ )
|
|
sat_solver_add_mux( p,
|
|
iVarM + m,
|
|
iVarP0 + m % nMintsL,
|
|
iVarP1 + 2 * (m / nMintsL) + 1,
|
|
iVarP1 + 2 * (m / nMintsL),
|
|
0, 0, 0, 0 );
|
|
return p;
|
|
}
|
|
void * If_ManSatBuildXYZ( int nLutSize )
|
|
{
|
|
int nMintsL = (1 << nLutSize);
|
|
int nMintsF = (1 << (3 * nLutSize - 2));
|
|
int nVars = 3 * nMintsL + nMintsF;
|
|
int iVarP0 = 0; // LUT0 parameters (total nMintsL)
|
|
int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
|
|
int iVarP2 = 2 * nMintsL; // LUT2 parameters (total nMintsL)
|
|
int m,iVarM = 3 * nMintsL; // MUX vars (total nMintsF)
|
|
sat_solver * p = sat_solver_new();
|
|
sat_solver_setnvars( p, nVars );
|
|
for ( m = 0; m < nMintsF; m++ )
|
|
sat_solver_add_mux41( p,
|
|
iVarM + m,
|
|
iVarP0 + m % nMintsL,
|
|
iVarP1 + (m >> nLutSize) % nMintsL,
|
|
iVarP2 + 4 * (m >> (2 * nLutSize)) + 0,
|
|
iVarP2 + 4 * (m >> (2 * nLutSize)) + 1,
|
|
iVarP2 + 4 * (m >> (2 * nLutSize)) + 2,
|
|
iVarP2 + 4 * (m >> (2 * nLutSize)) + 3 );
|
|
return p;
|
|
}
|
|
void If_ManSatUnbuild( void * p )
|
|
{
|
|
if ( p )
|
|
sat_solver_delete( (sat_solver *)p );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Verification for 6-input function.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static word If_ManSat6ComposeLut4( int t, word f[4], int k )
|
|
{
|
|
int m, v, nMints = (1 << k);
|
|
word c, r = 0;
|
|
assert( k <= 4 );
|
|
for ( m = 0; m < nMints; m++ )
|
|
{
|
|
if ( !((t >> m) & 1) )
|
|
continue;
|
|
c = ~(word)0;
|
|
for ( v = 0; v < k; v++ )
|
|
c &= ((m >> v) & 1) ? f[v] : ~f[v];
|
|
r |= c;
|
|
}
|
|
return r;
|
|
}
|
|
word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet )
|
|
{
|
|
word r, q, f[4];
|
|
int i, k = 0;
|
|
// bound set vars
|
|
for ( i = 0; i < nSSet; i++ )
|
|
f[k++] = s_Truths6[pSSet[i]];
|
|
for ( i = 0; i < nBSet; i++ )
|
|
f[k++] = s_Truths6[pBSet[i]];
|
|
q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k );
|
|
// free set vars
|
|
k = 0;
|
|
f[k++] = q;
|
|
for ( i = 0; i < nSSet; i++ )
|
|
f[k++] = s_Truths6[pSSet[i]];
|
|
for ( i = 0; i < nFSet; i++ )
|
|
f[k++] = s_Truths6[pFSet[i]];
|
|
r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k );
|
|
return r;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns config string for the given truth table.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
|
|
{
|
|
sat_solver * p = (sat_solver *)pSat;
|
|
int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE];
|
|
int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE];
|
|
int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE];
|
|
int nMintsL = (1 << nLutSize);
|
|
int nMintsF = (1 << (2 * nLutSize - 1));
|
|
int v, Value, m, mNew, nMintsFNew, nMintsLNew;
|
|
word Res;
|
|
// collect variable sets
|
|
Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
|
|
assert( nBSet + nSSet + nFSet == nVars );
|
|
// check variable bounds
|
|
assert( nSSet + nBSet <= nLutSize );
|
|
assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 );
|
|
nMintsFNew = (1 << (nLutSize + nSSet + nFSet));
|
|
// remap minterms
|
|
Vec_IntFill( vLits, nMintsF, -1 );
|
|
for ( m = 0; m < (1 << nVars); m++ )
|
|
{
|
|
mNew = iBSet = iSSet = iFSet = 0;
|
|
for ( v = 0; v < nVars; v++ )
|
|
{
|
|
Value = ((uSet >> (v << 1)) & 3);
|
|
if ( Value == 0 ) // FS
|
|
{
|
|
if ( ((m >> v) & 1) )
|
|
mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v;
|
|
iFSet++;
|
|
}
|
|
else if ( Value == 1 ) // BS
|
|
{
|
|
if ( ((m >> v) & 1) )
|
|
mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v;
|
|
iBSet++;
|
|
}
|
|
else if ( Value == 3 ) // SS
|
|
{
|
|
if ( ((m >> v) & 1) )
|
|
{
|
|
mNew |= 1 << iSSet;
|
|
mNew |= 1 << (nLutSize + iSSet);
|
|
pSSet[iSSet] = v;
|
|
}
|
|
iSSet++;
|
|
}
|
|
else assert( Value == 0 );
|
|
}
|
|
assert( iBSet == nBSet && iFSet == nFSet );
|
|
assert( Vec_IntEntry(vLits, mNew) == -1 );
|
|
Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
|
|
}
|
|
// find assumptions
|
|
v = 0;
|
|
Vec_IntForEachEntry( vLits, Value, m )
|
|
{
|
|
// printf( "%d", (Value >= 0) ? Value : 2 );
|
|
if ( Value >= 0 )
|
|
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
|
|
}
|
|
Vec_IntShrink( vLits, v );
|
|
// printf( " %d\n", Vec_IntSize(vLits) );
|
|
// run SAT solver
|
|
Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
|
|
if ( Value != l_True )
|
|
return 0;
|
|
if ( pTBound && pTFree )
|
|
{
|
|
// collect config
|
|
assert( nSSet + nBSet <= nLutSize );
|
|
*pTBound = 0;
|
|
nMintsLNew = (1 << (nSSet + nBSet));
|
|
for ( m = 0; m < nMintsLNew; m++ )
|
|
if ( sat_solver_var_value(p, m) )
|
|
Abc_TtSetBit( pTBound, m );
|
|
*pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet );
|
|
// collect configs
|
|
assert( nSSet + nFSet + 1 <= nLutSize );
|
|
*pTFree = 0;
|
|
nMintsLNew = (1 << (1 + nSSet + nFSet));
|
|
for ( m = 0; m < nMintsLNew; m++ )
|
|
if ( sat_solver_var_value(p, nMintsL+m) )
|
|
Abc_TtSetBit( pTFree, m );
|
|
*pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
|
|
if ( nVars != 6 || nLutSize != 4 )
|
|
return 1;
|
|
// verify the result
|
|
Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
|
|
if ( pTruth[0] != Res )
|
|
{
|
|
Dau_DsdPrintFromTruth( pTruth, nVars );
|
|
Dau_DsdPrintFromTruth( &Res, nVars );
|
|
Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
|
|
Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
|
|
printf( "Verification failed!\n" );
|
|
}
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns config string for the given truth table.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
|
|
{
|
|
unsigned uSet = 0;
|
|
int nTotal = 2 * nLutSize - 1;
|
|
int nShared = nTotal - nVars;
|
|
int i[6], s[4];
|
|
assert( nLutSize >= 2 && nLutSize <= 6 );
|
|
assert( nLutSize < nVars && nVars <= nTotal );
|
|
assert( nShared >= 0 && nShared < nLutSize - 1 );
|
|
if ( nLutSize == 2 )
|
|
{
|
|
assert( nShared == 0 );
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1]));
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
|
|
return uSet;
|
|
}
|
|
}
|
|
else if ( nLutSize == 3 )
|
|
{
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
|
|
return uSet;
|
|
}
|
|
if ( nShared < 1 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]]));
|
|
}
|
|
}
|
|
else if ( nLutSize == 4 )
|
|
{
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
|
|
return uSet;
|
|
}
|
|
if ( nShared < 1 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]]));
|
|
}
|
|
if ( nShared < 2 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
|
|
{
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
|
|
}
|
|
}
|
|
}
|
|
else if ( nLutSize == 5 )
|
|
{
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
|
|
return uSet;
|
|
}
|
|
if ( nShared < 1 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]]));
|
|
}
|
|
if ( nShared < 2 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
|
|
}
|
|
if ( nShared < 3 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
|
|
}
|
|
}
|
|
else if ( nLutSize == 6 )
|
|
{
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
|
|
return uSet;
|
|
}
|
|
if ( nShared < 1 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]]));
|
|
}
|
|
if ( nShared < 2 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
|
|
}
|
|
if ( nShared < 3 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
|
|
}
|
|
if ( nShared < 4 )
|
|
return 0;
|
|
for ( i[0] = 0; i[0] < nVars; i[0]++ )
|
|
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
|
|
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
|
|
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
|
|
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
|
|
for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
|
|
{
|
|
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
|
|
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
|
|
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
|
|
for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
|
|
for ( s[3] = s[1]+1; s[3] < nLutSize; s[3]++ )
|
|
if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]])), NULL, NULL, vLits) )
|
|
return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]]));
|
|
}
|
|
}
|
|
return 0;
|
|
}
|
|
unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
|
|
{
|
|
unsigned uSet = If_ManSatCheckXYall_int( pSat, nLutSize, pTruth, nVars, vLits );
|
|
// Dau_DecPrintSet( uSet, nVars, 1 );
|
|
return uSet;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Test procedure.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void If_ManSatTest2()
|
|
{
|
|
int nVars = 6;
|
|
int nLutSize = 4;
|
|
sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
|
|
// char * pDsd = "(abcdefg)";
|
|
// char * pDsd = "([a!bc]d!e)";
|
|
char * pDsd = "0123456789ABCDEF{abcdef}";
|
|
word * pTruth = Dau_DsdToTruth( pDsd, nVars );
|
|
word uBound, uFree;
|
|
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
|
|
// unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
|
|
// unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
|
|
unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
|
|
int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
|
|
assert( RetValue );
|
|
|
|
// Abc_TtPrintBinary( pTruth, nVars );
|
|
// Abc_TtPrintBinary( &uBound, nLutSize );
|
|
// Abc_TtPrintBinary( &uFree, nLutSize );
|
|
|
|
Dau_DsdPrintFromTruth( pTruth, nVars );
|
|
Dau_DsdPrintFromTruth( &uBound, nLutSize );
|
|
Dau_DsdPrintFromTruth( &uFree, nLutSize );
|
|
sat_solver_delete(p);
|
|
Vec_IntFree( vLits );
|
|
}
|
|
void If_ManSatTest3()
|
|
{
|
|
int nVars = 6;
|
|
int nLutSize = 4;
|
|
sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
|
|
// char * pDsd = "(abcdefg)";
|
|
// char * pDsd = "([a!bc]d!e)";
|
|
char * pDsd = "0123456789ABCDEF{abcdef}";
|
|
word * pTruth = Dau_DsdToTruth( pDsd, nVars );
|
|
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
|
|
// unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
|
|
// unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
|
|
unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
|
|
uSet = If_ManSatCheckXYall( p, nLutSize, pTruth, nVars, vLits );
|
|
Dau_DecPrintSet( uSet, nVars, 1 );
|
|
|
|
sat_solver_delete(p);
|
|
Vec_IntFree( vLits );
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|