/**CFile****************************************************************
FileName [bmcMaj3.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Majority gate synthesis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcMaj3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MAJ3_OBJS 32 // nVars + nNodes
typedef struct Maj3_Man_t_ Maj3_Man_t;
struct Maj3_Man_t_
{
int nVars; // inputs
int nNodes; // internal nodes
int nObjs; // total objects (nVars inputs, nNodes internal nodes)
int nWords; // the truth table size in 64-bit words
int iVar; // the next available SAT variable
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Int_t * vLevels; // distriction of nodes by levels
int VarMarks[MAJ3_OBJS][MAJ3_OBJS]; // variable marks
int ObjVals[MAJ3_OBJS]; // object values
int pLits[2][MAJ3_OBJS]; // neg, pos literals
int nLits[3]; // neg, pos, fixed literal
bmcg_sat_solver * pSat; // SAT solver
};
static inline word * Maj3_ManTruth( Maj3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Maj3_ManValue( int iMint, int nVars )
{
int k, Count = 0;
for ( k = 0; k < nVars; k++ )
Count += (iMint >> k) & 1;
return (int)(Count > nVars/2);
}
Vec_Wrd_t * Maj3_ManTruthTables( Maj3_Man_t * p )
{
Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
for ( i = 0; i < p->nVars; i++ )
Abc_TtIthVar( Maj3_ManTruth(p, i), i, p->nVars );
for ( i = 0; i < nMints; i++ )
if ( Maj3_ManValue(i, p->nVars) )
Abc_TtSetBit( Maj3_ManTruth(p, p->nObjs), i );
//Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
return vInfo;
}
void Maj3_ManFirstAndLevel( Vec_Int_t * vLevels, int Firsts[MAJ3_OBJS], int Levels[MAJ3_OBJS], int nVars, int nObjs )
{
int i, k, Entry, Obj = 0;
Firsts[0] = Obj;
for ( k = 0; k < nVars; k++ )
Levels[Obj++] = 0;
Vec_IntReverseOrder( vLevels );
Vec_IntForEachEntry( vLevels, Entry, i )
{
Firsts[i+1] = Obj;
for ( k = 0; k < Entry; k++ )
Levels[Obj++] = i+1;
}
Vec_IntReverseOrder( vLevels );
assert( Obj == nObjs );
}
int Maj3_ManMarkup( Maj3_Man_t * p )
{
int nSatVars = 2; // SAT variable counter
int nLevels = Vec_IntSize(p->vLevels);
int nSecond = Vec_IntEntry(p->vLevels, 1);
int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
assert( Vec_IntEntry(p->vLevels, 0) == 1 );
assert( p->nObjs <= MAJ3_OBJS );
assert( p->nNodes == Vec_IntSum(p->vLevels) );
Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
// create map
for ( i = 0; i < p->nObjs; i++ )
for ( k = 0; k < p->nObjs; k++ )
p->VarMarks[i][k] = -1;
for ( k = 0; k < 3; k++ ) // first node
p->VarMarks[p->nVars][k] = 1;
for ( k = 0; k < nSecond; k++ ) // top node
p->VarMarks[p->nObjs-1][p->nObjs-2-k] = 1;
for ( k = 2; k < nLevels; k++ ) // cascade
p->VarMarks[Firsts[k]][Firsts[k-1]] = 1;
for ( i = p->nVars+1; i < (nSecond == 3 ? p->nObjs-1 : p->nObjs); i++ )
for ( k = 0; k < Firsts[Levels[i]]; k++ )
if ( p->VarMarks[i][k] == -1 )
p->VarMarks[i][k] = nSatVars++;
//printf( "The number of variables is %d.\n", nSatVars );
return nSatVars;
}
void Maj3_ManVarMapPrint( Maj3_Man_t * p )
{
int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
// print
printf( "Variable map for problem with %d inputs, %d nodes and %d levels: ", p->nVars, p->nNodes, Vec_IntSize(p->vLevels) );
Vec_IntPrint( p->vLevels );
printf( " " );
printf( " " );
for ( i = 0; i < p->nObjs; i++ )
printf( "%3d ", i );
printf( "\n" );
for ( i = p->nObjs-1; i >= p->nVars; i-- )
{
printf( " %2d ", i );
printf( " %2d ", Levels[i] );
for ( k = 0; k < p->nObjs; k++ )
if ( p->VarMarks[i][k] == -1 )
printf( " . " );
else if ( p->VarMarks[i][k] == 1 )
printf( " + " );
else
printf( "%3d%c ", p->VarMarks[i][k], bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k]) ? '+' : ' ' );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Maj3_ManFindFanin( Maj3_Man_t * p, int i, int * pFanins )
{
int f, nFanins = 0;
p->nLits[0] = p->nLits[1] = p->nLits[2] = 0;
for ( f = 0; f < i; f++ )
{
if ( p->VarMarks[i][f] < 0 )
continue;
assert( p->VarMarks[i][f] > 0 );
if ( p->VarMarks[i][f] == 1 ) // fixed
{
p->nLits[2]++;
pFanins[nFanins++] = f;
}
else if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][f]) ) // pos
{
p->pLits[1][p->nLits[1]++] = Abc_Var2Lit(p->VarMarks[i][f], 1);
pFanins[nFanins++] = f;
}
else // neg
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(p->VarMarks[i][f], 0);
}
return nFanins;
}
static inline void Maj3_ManPrintSolution( Maj3_Man_t * p )
{
int i, k, iVar, nFanins, pFanins[MAJ3_OBJS];
printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
// for ( i = p->nVars; i < p->nObjs; i++ )
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
printf( "%02d = MAJ(", i );
nFanins = Maj3_ManFindFanin( p, i, pFanins );
assert( nFanins == 3 );
for ( k = 0; k < 3; k++ )
{
iVar = pFanins[k];
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %02d", iVar );
}
printf( " )\n" );
}
}
static inline int Maj3_ManEval( Maj3_Man_t * p )
{
int fUseMiddle = 1;
static int Flag = 0;
int i, k, iMint, pFanins[3]; word * pFaninsW[3];
for ( i = p->nVars; i < p->nObjs; i++ )
{
int nFanins = Maj3_ManFindFanin( p, i, pFanins );
assert( nFanins == 3 );
for ( k = 0; k < 3; k++ )
pFaninsW[k] = Maj3_ManTruth( p, pFanins[k] );
Abc_TtMaj( Maj3_ManTruth(p, i), pFaninsW[0], pFaninsW[1], pFaninsW[2], p->nWords );
}
if ( fUseMiddle )
{
iMint = -1;
for ( i = 0; i < (1 << p->nVars); i++ )
{
int nOnes = Abc_TtBitCount16(i);
if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
continue;
if ( Abc_TtGetBit(Maj3_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj3_ManTruth(p, p->nObjs-1), i) )
continue;
iMint = i;
break;
}
}
else
{
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj3_ManTruth(p, p->nObjs-1), Maj3_ManTruth(p, p->nObjs), p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Maj3_ManTruth(p, p->nObjs-1), Maj3_ManTruth(p, p->nObjs), p->nVars );
}
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Maj3_PrintClause( int * pLits, int nLits )
{
int i;
for ( i = 0; i < nLits; i++ )
printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
printf( "\n" );
}
int Maj3_ManAddCnfStart( Maj3_Man_t * p )
{
int i, k, status, nLits, pLits[MAJ3_OBJS];
// nodes have at least one fanin
//printf( "Fanin clauses:\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
// check if it is already connected
int Count = 0;
for ( k = 0; k < p->nObjs; k++ )
Count += p->VarMarks[i][k] == 1;
assert( Count <= 3 );
if ( Count == 3 )
continue;
// collect connections
nLits = 0;
for ( k = 0; k < p->nObjs; k++ )
if ( p->VarMarks[i][k] > 1 )
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
//Maj3_PrintClause( pLits, nLits );
assert( nLits > 0 );
if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
assert(0);
}
// nodes have at least one fanout
//printf( "Fanout clauses:\n" );
for ( k = 0; k < p->nObjs-1; k++ )
{
// check if it is already connected
int Count = 0;
for ( i = 0; i < p->nObjs; i++ )
Count += p->VarMarks[i][k] == 1;
assert( Count <= 3 );
if ( Count > 0 )
continue;
// collect connections
nLits = 0;
for ( i = 0; i < p->nObjs; i++ )
if ( p->VarMarks[i][k] > 1 )
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
//Maj3_PrintClause( pLits, nLits );
//assert( nLits > 0 );
if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
assert(0);
}
status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
assert( status == GLUCOSE_SAT );
Maj3_ManVarMapPrint( p );
return 1;
}
int Maj3_ManAddCnf( Maj3_Man_t * p, int iMint )
{
// input values
int i, k, j, n, * pVals = p->ObjVals;
for ( i = 0; i < p->nVars; i++ )
pVals[i] = (iMint >> i) & 1;
// first node value
pVals[p->nVars] = (pVals[0] && pVals[1]) || (pVals[0] && pVals[2]) || (pVals[1] && pVals[2]);
// last node value
pVals[p->nObjs-1] = Maj3_ManValue(iMint, p->nVars);
// intermediate node values
for ( i = p->nVars + 1; i < p->nObjs - 1; i++ )
pVals[i] = p->iVar++;
//printf( "Adding clauses for minterm %d.\n", iMint );
bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
for ( n = 0; n < 2; n++ )
for ( i = p->nVars + 1; i < p->nObjs; i++ )
{
//printf( "\nNode %d. Phase %d.\n", i, n );
for ( k = 0; k < p->nObjs; k++ ) if ( p->VarMarks[i][k] >= 1 )
{
// add first input
int pLits[5], nLits = 0;
if ( pVals[k] == !n )
continue;
if ( pVals[k] > 1 )
pLits[nLits++] = Abc_Var2Lit( pVals[k], n );
if ( p->VarMarks[i][k] > 1 )
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 1 );
for ( j = k+1; j < p->nObjs; j++ ) if ( p->VarMarks[i][j] >= 1 )
{
// add second input
int nLits2 = nLits;
if ( pVals[j] == !n )
continue;
if ( pVals[j] > 1 )
pLits[nLits2++] = Abc_Var2Lit( pVals[j], n );
if ( p->VarMarks[i][j] > 1 )
pLits[nLits2++] = Abc_Var2Lit( p->VarMarks[i][j], 1 );
// add output
if ( pVals[i] == n )
continue;
if ( pVals[i] > 1 )
pLits[nLits2++] = Abc_Var2Lit( pVals[i], !n );
assert( nLits2 > 0 && nLits2 <= 5 );
//Maj3_PrintClause( pLits, nLits2 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits2 ) )
return 0;
}
}
}
return 1;
}
int Maj3_ManAddConstraintsLazy( Maj3_Man_t * p )
{
int i, pFanins[MAJ3_OBJS], nConstr = 0;
//Maj3_ManVarMapPrint( p );
for ( i = p->nVars+1; i < p->nObjs; i++ )
{
int nFanins = Maj3_ManFindFanin( p, i, pFanins );
if ( nFanins == 3 )
continue;
//printf( "Node %d has %d fanins.\n", i, nFanins );
nConstr++;
if ( nFanins < 3 )
{
assert( p->nLits[0] > 0 );
//Maj3_PrintClause( p->pLits[0], p->nLits[0] );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return -1;
}
else if ( nFanins > 3 )
{
int nLits = Abc_MinInt(4 - p->nLits[2], p->nLits[1]);
assert( nLits > 0 );
//Maj3_PrintClause( p->pLits[1], nLits );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], nLits ) )
return -1;
}
}
return nConstr;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Maj3_Man_t * Maj3_ManAlloc( int nVars, int nNodes, Vec_Int_t * vLevels )
{
Maj3_Man_t * p = ABC_CALLOC( Maj3_Man_t, 1 );
p->vLevels = vLevels;
p->nVars = nVars;
p->nNodes = nNodes;
p->nObjs = nVars + nNodes;
p->nWords = Abc_TtWordNum(nVars);
p->iVar = Maj3_ManMarkup( p );
p->vInfo = Maj3_ManTruthTables( p );
p->pSat = bmcg_sat_solver_start();
bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
Maj3_ManAddCnfStart( p );
return p;
}
void Maj3_ManFree( Maj3_Man_t * p )
{
bmcg_sat_solver_stop( p->pSat );
Vec_WrdFree( p->vInfo );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Maj3_ManExactSynthesis( int nVars, int nNodes, int fVerbose, Vec_Int_t * vLevels )
{
Maj3_Man_t * p; abctime clkTotal = Abc_Clock();
int i, status, nLazy, nLazyAll = 0, iMint = 0;
printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", nVars, nNodes );
p = Maj3_ManAlloc( nVars, nNodes, vLevels );
for ( i = 0; iMint != -1; i++ )
{
abctime clk = Abc_Clock();
if ( !Maj3_ManAddCnf( p, iMint ) )
break;
while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
{
nLazy = Maj3_ManAddConstraintsLazy( p );
if ( nLazy == -1 )
{
printf( "Became UNSAT after adding lazy constraints.\n" );
status = GLUCOSE_UNSAT;
break;
}
//printf( "Added %d lazy constraints.\n\n", nLazy );
if ( nLazy == 0 )
break;
nLazyAll += nLazy;
}
if ( fVerbose )
{
printf( "Iter %3d : ", i );
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
printf( " Var =%5d ", p->iVar );
printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
printf( "Lazy =%9d ", nLazyAll );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( status == GLUCOSE_UNSAT )
{
printf( "The problem has no solution.\n" );
break;
}
iMint = Maj3_ManEval( p );
}
if ( iMint == -1 )
Maj3_ManPrintSolution( p );
Maj3_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return iMint == -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Maj3_ManTest()
{
/*
int nVars = 5;
int nNodes = 4;
int fVerbose = 1;
int Levels[MAJ3_OBJS] = { 1, 2, 1 };
Vec_Int_t vLevels = { 3, 3, Levels };
*/
int nVars = 7;
int nNodes = 7;
int fVerbose = 1;
int Levels[MAJ3_OBJS] = { 1, 2, 2, 2 };
Vec_Int_t vLevels = { 4, 4, Levels };
/*
int nVars = 9;
int nNodes = 10;
int fVerbose = 1;
int Levels[MAJ3_OBJS] = { 1, 2, 3, 2, 2 };
Vec_Int_t vLevels = { 5, 5, Levels };
*/
/*
int nVars = 9;
int nNodes = 10;
int fVerbose = 1;
int Levels[MAJ3_OBJS] = { 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 };
Vec_Int_t vLevels = { 10, 10, Levels };
*/
// Maj3_Man_t * p = Maj3_ManAlloc( nVars, nNodes, &vLevels );
// Maj3_ManFree( p );
Maj3_ManExactSynthesis( nVars, nNodes, fVerbose, &vLevels );
return 0;
}
typedef struct Zyx_Man_t_ Zyx_Man_t;
struct Zyx_Man_t_
{
Bmc_EsPar_t * pPars; // parameters
word * pTruth; // truth table
int nObjs; // total objects (nVars inputs, nNodes internal nodes)
int nWords; // the truth table size in 64-bit words
int LutMask; // 1 << nLutSize
int TopoBase; // (1 << nLutSize) * nObjs
int MintBase; // TopoBase + nObjs * nObjs
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Int_t * vVarValues; // variable values
Vec_Int_t * vMidMints; // middle minterms
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
Vec_Int_t * vPairs; // sym var pairs
int nUsed[2];
int pFanins[MAJ3_OBJS][MAJ3_OBJS]; // fanins
int pLits[2][2*MAJ3_OBJS]; // neg/pos literals
int nLits[2]; // neg/pos literal
int Counts[1024];
bmcg_sat_solver * pSat; // SAT solver
abctime clkEval;
};
static inline word * Zyx_ManTruth( Zyx_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
static inline int Zyx_FuncVar( Zyx_Man_t * p, int i, int m ) { return (p->LutMask + 1) * (i - p->pPars->nVars) + m; }
static inline int Zyx_TopoVar( Zyx_Man_t * p, int i, int f ) { return p->TopoBase + p->nObjs * (i - p->pPars->nVars) + f; }
static inline int Zyx_MintVar( Zyx_Man_t * p, int m, int i ) { return p->MintBase + p->nObjs * m + i; }
//static inline int Zyx_MintVar2( Zyx_Man_t * p, int m, int i, int f ) { assert(i >= p->pPars->nVars); return p->MintBase + m * p->pPars->nNodes * (p->pPars->nLutSize + 1) + (i - p->pPars->nVars) * (p->pPars->nLutSize + 1) + f; }
static inline int Zyx_ManIsUsed2( Zyx_Man_t * p, int m, int n, int i, int j )
{
int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j;
p->nUsed[0]++;
assert( i < n && j < n && i < j );
if ( Vec_BitEntry(p->vUsed2, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed2, Pos, 1 );
return 0;
}
static inline int Zyx_ManIsUsed3( Zyx_Man_t * p, int m, int n, int i, int j, int k )
{
int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k;
p->nUsed[0]++;
assert( i < n && j < n && k < n && i < j && j < k );
if ( Vec_BitEntry(p->vUsed3, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed3, Pos, 1 );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Zyx_SetConstVar( Zyx_Man_t * p, int Var, int Value )
{
int iLit = Abc_Var2Lit( Var, !Value );
int status = bmcg_sat_solver_addclause( p->pSat, &iLit, 1 );
assert( status );
assert( Vec_IntEntry(p->vVarValues, Var) == -1 );
Vec_IntWriteEntry( p->vVarValues, Var, Value );
//printf( "Setting var %d to value %d.\n", Var, Value );
}
void Zyx_ManSetupVars( Zyx_Man_t * p )
{
int i, k, m;
word * pSpec = p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : p->pTruth;
// set unused functionality vars to 0
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
Zyx_SetConstVar( p, Zyx_FuncVar(p, i, 0), 0 );
// set unused topology vars
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
for ( k = i; k < p->nObjs; k++ )
Zyx_SetConstVar( p, Zyx_TopoVar(p, i, k), 0 );
// connect topmost node
Zyx_SetConstVar( p, Zyx_TopoVar(p, p->nObjs-1, p->nObjs-2), 1 );
// connect first node
if ( p->pPars->fMajority )
for ( k = 0; k < p->pPars->nVars; k++ )
Zyx_SetConstVar( p, Zyx_TopoVar(p, p->pPars->nVars, k), k < 3 );
// set minterm vars
for ( m = 0; m < (1 << p->pPars->nVars); m++ )
{
for ( i = 0; i < p->pPars->nVars; i++ )
Zyx_SetConstVar( p, Zyx_MintVar(p, m, i), (m >> i) & 1 );
Zyx_SetConstVar( p, Zyx_MintVar(p, m, p->nObjs-1), Abc_TtGetBit(pSpec, m) );
}
}
int Zyx_ManAddCnfStart( Zyx_Man_t * p )
{
// nodes have fanins
int i, k, pLits[MAJ3_OBJS];
//printf( "Adding initial clauses:\n" );
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
int nLits = 0;
for ( k = 0; k < i; k++ )
pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
assert( nLits > 0 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
return 0;
}
// nodes have fanouts
for ( k = 0; k < p->nObjs-1; k++ )
{
int nLits = 0;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
assert( nLits > 0 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
return 0;
}
// two input functions
if ( p->pPars->nLutSize != 2 )
return 1;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
for ( k = 0; k < 3; k++ )
{
pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), k==1 );
pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), k==2 );
pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), k!=0 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
return 0;
}
if ( p->pPars->fOnlyAnd )
{
pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), 1 );
pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), 1 );
pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), 0 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
return 0;
}
}
return 1;
}
void Zyx_ManPrintVarMap( Zyx_Man_t * p, int fSat )
{
int i, k, nTopoVars = 0;
printf( " " );
for ( k = 0; k < p->nObjs-1; k++ )
printf( "%3d ", k );
printf( "\n" );
for ( i = p->nObjs-1; i >= p->pPars->nVars; i-- )
{
printf( "%3d ", i );
for ( k = 0; k < p->nObjs-1; k++ )
{
int iVar = Zyx_TopoVar(p, i, k);
if ( Vec_IntEntry(p->vVarValues, iVar) == -1 )
printf( "%3d%c ", iVar, (fSat && bmcg_sat_solver_read_cex_varvalue(p->pSat, iVar)) ? '*' : ' ' ), nTopoVars++;
else
printf( "%3d ", Vec_IntEntry(p->vVarValues, iVar) );
}
printf( "\n" );
}
if ( fSat ) return;
printf( "Using %d active functionality vars and %d active topology vars (out of %d SAT vars).\n",
p->pPars->fMajority ? 0 : p->pPars->nNodes * p->LutMask, nTopoVars, bmcg_sat_solver_varnum(p->pSat) );
}
void Zyx_PrintClause( int * pLits, int nLits )
{
int i;
for ( i = 0; i < nLits; i++ )
printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Zyx_ManValue( int iMint, int nVars )
{
int k, Count = 0;
for ( k = 0; k < nVars; k++ )
Count += (iMint >> k) & 1;
return (int)(Count > nVars/2);
}
Vec_Wrd_t * Zyx_ManTruthTables( Zyx_Man_t * p, word * pTruth )
{
Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
int i, nMints = Abc_MaxInt( 64, 1 << p->pPars->nVars );
assert( p->pPars->fMajority == (pTruth == NULL) );
for ( i = 0; i < p->pPars->nVars; i++ )
Abc_TtIthVar( Zyx_ManTruth(p, i), i, p->pPars->nVars );
if ( p->pPars->fMajority )
{
for ( i = 0; i < nMints; i++ )
if ( Zyx_ManValue(i, p->pPars->nVars) )
Abc_TtSetBit( Zyx_ManTruth(p, p->nObjs), i );
for ( i = 0; i < nMints; i++ )
if ( Abc_TtBitCount16(i) == p->pPars->nVars/2 || Abc_TtBitCount16(i) == p->pPars->nVars/2+1 )
Vec_IntPush( p->vMidMints, i );
}
//Dau_DsdPrintFromTruth( Zyx_ManTruth(p, p->nObjs), p->pPars->nVars );
return vInfo;
}
Vec_Int_t * Zyx_ManCreateSymVarPairs( word * pTruth, int nVars )
{
Vec_Int_t * vPairs = Vec_IntAlloc( 100 );
int i, k, nWords = Abc_TtWordNum(nVars);
word Cof0[64], Cof1[64];
word Cof01[64], Cof10[64];
assert( nVars <= 12 );
for ( i = 0; i < nVars; i++ )
{
Abc_TtCofactor0p( Cof0, pTruth, nWords, i );
Abc_TtCofactor1p( Cof1, pTruth, nWords, i );
for ( k = i+1; k < nVars; k++ )
{
Abc_TtCofactor1p( Cof01, Cof0, nWords, k );
Abc_TtCofactor0p( Cof10, Cof1, nWords, k );
if ( Abc_TtEqual( Cof01, Cof10, nWords ) )
Vec_IntPushTwo( vPairs, i, k );
}
}
return vPairs;
}
Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
{
Zyx_Man_t * p = ABC_CALLOC( Zyx_Man_t, 1 );
p->pPars = pPars;
p->pTruth = pTruth;
p->nObjs = p->pPars->nVars + p->pPars->nNodes;
p->nWords = Abc_TtWordNum(p->pPars->nVars);
p->LutMask = (1 << p->pPars->nLutSize) - 1;
p->TopoBase = (1 << p->pPars->nLutSize) * p->pPars->nNodes;
p->MintBase = p->TopoBase + p->pPars->nNodes * p->nObjs;
p->vVarValues = Vec_IntStartFull( p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
p->vMidMints = Vec_IntAlloc( 1 << p->pPars->nVars );
p->vInfo = Zyx_ManTruthTables( p, pTruth );
p->vPairs = Zyx_ManCreateSymVarPairs( p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : pTruth, p->pPars->nVars );
p->pSat = bmcg_sat_solver_start();
if ( pPars->fUseIncr )
{
if ( p->pPars->nLutSize == 2 || p->pPars->fMajority )
p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
else if ( p->pPars->nLutSize == 3 )
p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
}
bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
Zyx_ManSetupVars( p );
Zyx_ManAddCnfStart( p );
Zyx_ManPrintVarMap( p, 0 );
return p;
}
void Zyx_ManFree( Zyx_Man_t * p )
{
bmcg_sat_solver_stop( p->pSat );
Vec_WrdFree( p->vInfo );
Vec_BitFreeP( &p->vUsed2 );
Vec_BitFreeP( &p->vUsed3 );
Vec_IntFree( p->vPairs );
Vec_IntFree( p->vMidMints );
Vec_IntFree( p->vVarValues );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Zyx_ManCollectFanins( Zyx_Man_t * p, int i )
{
int k, Val;
assert( i >= p->pPars->nVars && i < p->nObjs );
p->nLits[0] = p->nLits[1] = 0;
for ( k = 0; k < i; k++ )
{
Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k));
p->pFanins[i][p->nLits[1]] = k;
p->pLits[Val][p->nLits[Val]++] = Abc_Var2Lit(Zyx_TopoVar(p, i, k), Val);
}
return p->nLits[1];
}
int Zyx_ManAddCnfLazyTopo( Zyx_Man_t * p )
{
int i, k, j, Entry[2], Node[2], nLazy = 0;
// fanin count
//printf( "Adding topology clauses.\n" );
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
int nFanins = Zyx_ManCollectFanins( p, i );
if ( nFanins == p->pPars->nLutSize )
continue;
nLazy++;
assert( nFanins == p->nLits[1] );
if ( p->nLits[1] > p->pPars->nLutSize )
{
p->nLits[1] = p->pPars->nLutSize + 1;
//Zyx_PrintClause( p->pLits[1], p->nLits[1] );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], p->nLits[1] ) )
return -1;
}
else // if ( p->nLits[1] < p->pPars->nLutSize )
{
//Zyx_PrintClause( p->pLits[0], p->nLits[0] );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return -1;
}
}
if ( nLazy || !p->pPars->fOrderNodes )
return nLazy;
// ordering
for ( i = p->pPars->nVars + 1; i < p->nObjs; i++ )
{
for ( k = p->pPars->nLutSize - 1; k >= 0; k-- )
if ( p->pFanins[i-1][k] != p->pFanins[i][k] )
break;
if ( k == -1 ) // fanins are equal
{
if ( p->pPars->fMajority )
continue;
// compare by LUT functions
for ( k = p->LutMask; k >= 0; k-- )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) !=
bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) )
break;
if ( k == -1 ) // truth tables cannot be equal
continue;
// rule out these truth tables
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 0 &&
bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) == 1 )
{
continue;
}
nLazy++;
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 1 );
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i , k)) == 0 );
// rule out this order
p->nLits[0] = 0;
for ( j = p->LutMask; j >= k; j-- )
{
int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, j));
int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, j));
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i-1, j), ValA );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i, j), ValB );
}
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return -1;
continue;
}
if ( p->pFanins[i-1][k] < p->pFanins[i][k] )
{
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i][k])) == 0 );
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i , p->pFanins[i][k])) == 1 );
continue;
}
nLazy++;
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i-1][k])) == 1 );
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i , p->pFanins[i-1][k])) == 0 );
// rule out this order
p->nLits[0] = 0;
for ( j = p->pFanins[i-1][k]; j < p->nObjs-1; j++ )
{
int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, j));
int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, j));
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i-1, j), ValA );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i, j), ValB );
}
//printf( "\n" );
//Zyx_ManPrintVarMap( p, 1 );
//Zyx_PrintClause( p->pLits[0], p->nLits[0] );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return -1;
//break;
}
// check symmetric variables
Vec_IntForEachEntryDouble( p->vPairs, Entry[0], Entry[1], k )
{
assert( Entry[0] < Entry[1] );
for ( j = 0; j < 2; j++ )
{
Node[j] = -1;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, Entry[j])) )
{
Node[j] = i;
break;
}
assert( Node[j] >= p->pPars->nVars );
}
// compare the nodes
if ( Node[0] <= Node[1] )
continue;
assert( Node[0] > Node[1] );
// create blocking clause
nLazy++;
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[0])) == 0 );
assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[1])) == 1 );
// rule out this order
p->nLits[0] = 0;
for ( j = p->pPars->nVars; j <= Node[1]; j++ )
{
int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[0]));
int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[1]));
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[0]), ValA );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[1]), ValB );
}
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return -1;
}
return nLazy;
}
int Zyx_ManAddCnfBlockSolution( Zyx_Man_t * p )
{
Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int i, k;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
int nFanins = Zyx_ManCollectFanins( p, i );
assert( nFanins == p->pPars->nLutSize );
for ( k = 0; k < p->pPars->nLutSize; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(Zyx_TopoVar(p, i, p->pFanins[i][k]), 1) );
}
//Zyx_ManPrintVarMap( p, 1 );
//Zyx_PrintClause( Vec_IntArray(vLits), Vec_IntSize(vLits) );
if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ) )
return 0;
Vec_IntFree( vLits );
return 1;
}
int Zyx_ManAddCnfLazyFunc2( Zyx_Man_t * p, int iMint )
{
int i, k, n, j, s;
assert( !p->pPars->fMajority || p->pPars->nLutSize == 3 );
//printf( "Adding functionality clauses for minterm %d.\n", iMint );
p->Counts[iMint]++;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
int nFanins = Zyx_ManCollectFanins( p, i );
assert( nFanins == p->pPars->nLutSize );
if ( p->pPars->fMajority )
{
int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}};
for ( k = 0; k < 3; k++ )
{
if ( Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][Sets[k][0]], p->pFanins[i][Sets[k][1]]) )
continue;
for ( n = 0; n < 2; n++ )
{
p->nLits[0] = 0;
for ( s = 0; s < 2; s++ )
{
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][Sets[k][s]]), 1 );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][Sets[k][s]]), n );
}
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return 0;
}
}
}
else
{
if ( p->pPars->nLutSize == 2 && Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][0], p->pFanins[i][1]) )
continue;
if ( p->pPars->nLutSize == 3 && Zyx_ManIsUsed3(p, iMint, i, p->pFanins[i][0], p->pFanins[i][1], p->pFanins[i][2]) )
continue;
for ( k = 0; k <= p->LutMask; k++ )
for ( n = 0; n < 2; n++ )
{
p->nLits[0] = 0;
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
for ( j = 0; j < p->pPars->nLutSize; j++ )
{
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
}
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return 0;
}
}
}
return 1;
}
int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
{
int i, k, n, j, s, t, u;
//printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
assert( !p->pPars->fMajority && p->pPars->nLutSize < 4 );
p->Counts[iMint]++;
if ( p->pPars->nLutSize == 2 )
{
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
for ( s = 0; s < i; s++ )
for ( t = s+1; t < i; t++ )
{
p->pFanins[i][0] = s;
p->pFanins[i][1] = t;
for ( k = 0; k <= p->LutMask; k++ )
for ( n = 0; n < 2; n++ )
{
p->nLits[0] = 0;
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
for ( j = 0; j < p->pPars->nLutSize; j++ )
{
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
}
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return 0;
}
}
}
else if ( p->pPars->nLutSize == 3 )
{
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
for ( s = 0; s < i; s++ )
for ( t = s+1; t < i; t++ )
for ( u = t+1; u < i; u++ )
{
p->pFanins[i][0] = s;
p->pFanins[i][1] = t;
p->pFanins[i][2] = u;
for ( k = 0; k <= p->LutMask; k++ )
for ( n = 0; n < 2; n++ )
{
p->nLits[0] = 0;
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
for ( j = 0; j < p->pPars->nLutSize; j++ )
{
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
}
p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
return 0;
}
}
}
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Zyx_ManPrintSolutionFile( Zyx_Man_t * p, int fCompl, int fFirst )
{
FILE * pFile;
char FileName[1000]; int i, k;
if ( fCompl ) Abc_TtNot( p->pTruth, Abc_TtWordNum(p->pPars->nVars) );
Abc_TtWriteHexRev( FileName, p->pTruth, p->pPars->nVars );
if ( fCompl ) Abc_TtNot( p->pTruth, Abc_TtWordNum(p->pPars->nVars) );
sprintf( FileName + (1 << (p->pPars->nVars-2)), "-%d-%d.bool", p->pPars->nLutSize, p->pPars->nNodes );
pFile = fopen( FileName, fFirst ? "wb" : "ab" );
if ( pFile == NULL )
{
printf( "Cannot open input file \"%s\".\n", FileName );
return;
}
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
fprintf( pFile, "%c", 'A' + i );
if ( p->pPars->fMajority )
fprintf( pFile, "maj3" );
else
{
for ( k = p->LutMask; k >= 0; k-- )
fprintf( pFile, "%d", bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) ^ (i == p->nObjs - 1 && fCompl) );
for ( k = 0; k < i; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) )
{
if ( k >= 0 && k < p->pPars->nVars )
fprintf( pFile, "%c", 'a' + k );
else
fprintf( pFile, "%c", 'A' + k );
}
}
fprintf( pFile, "\n" );
}
fprintf( pFile, "\n" );
fclose( pFile );
printf( "Dumped solution into file \"%s\".\n", FileName );
}
static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl, int fFirst )
{
int i, k;
printf( "Realization of given %d-input function using %d %d-input %s:\n",
p->pPars->nVars, p->pPars->nNodes, p->pPars->nLutSize, p->pPars->fMajority ? "MAJ-gates" : "LUTs" );
for ( i = p->nObjs - 1; i >= p->pPars->nVars; i-- )
{
printf( "%02d = ", i );
if ( p->pPars->fMajority )
printf( "MAJ3" );
else
{
printf( "%d\'b", 1 << p->pPars->nLutSize );
for ( k = p->LutMask; k >= 0; k-- )
printf( "%d", bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) ^ (i == p->nObjs - 1 && fCompl) );
}
printf( "(" );
for ( k = 0; k < i; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) )
{
if ( k >= 0 && k < p->pPars->nVars )
printf( " %c", 'a'+k );
else
printf( " %02d", k );
}
printf( " )\n" );
}
if ( !p->pPars->fMajority )
Zyx_ManPrintSolutionFile( p, fCompl, fFirst );
}
static inline int Zyx_ManEval( Zyx_Man_t * p )
{
static int Flag = 0;
//abctime clk = Abc_Clock();
int i, k, j, iMint; word * pFaninsW[6], * pSpec;
for ( i = p->pPars->nVars; i < p->nObjs; i++ )
{
int nFanins = Zyx_ManCollectFanins( p, i );
assert( nFanins == p->pPars->nLutSize );
for ( k = 0; k < p->pPars->nLutSize; k++ )
pFaninsW[k] = Zyx_ManTruth( p, p->pFanins[i][k] );
if ( p->pPars->fMajority )
Abc_TtMaj( Zyx_ManTruth(p, i), pFaninsW[0], pFaninsW[1], pFaninsW[2], p->nWords );
else
{
Abc_TtConst0( Zyx_ManTruth(p, i), p->nWords );
for ( k = 1; k <= p->LutMask; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) )
{
Abc_TtConst1( Zyx_ManTruth(p, p->nObjs), p->nWords );
for ( j = 0; j < p->pPars->nLutSize; j++ )
Abc_TtAndCompl( Zyx_ManTruth(p, p->nObjs), Zyx_ManTruth(p, p->nObjs), 0, pFaninsW[j], !((k >> j) & 1), p->nWords );
Abc_TtOr( Zyx_ManTruth(p, i), Zyx_ManTruth(p, i), Zyx_ManTruth(p, p->nObjs), p->nWords );
}
}
}
pSpec = p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : p->pTruth;
if ( p->pPars->fMajority )
{
Vec_IntForEachEntry( p->vMidMints, iMint, i )
if ( Abc_TtGetBit(pSpec, iMint) != Abc_TtGetBit(Zyx_ManTruth(p, p->nObjs-1), iMint) )
return iMint;
return -1;
}
else
{
if ( Flag && p->pPars->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Zyx_ManTruth(p, p->nObjs-1), pSpec, p->pPars->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Zyx_ManTruth(p, p->nObjs-1), pSpec, p->pPars->nVars );
}
//Flag ^= 1;
assert( iMint < (1 << p->pPars->nVars) );
//p->clkEval += Abc_Clock() - clk;
return iMint;
}
static inline void Zyx_ManEvalStats( Zyx_Man_t * p )
{
int i;
for ( i = 0; i < (1 << p->pPars->nVars); i++ )
printf( "%d=%d ", i, p->Counts[i] );
printf( "\n" );
}
static inline void Zyx_ManPrint( Zyx_Man_t * p, int Iter, int iMint, int nLazyAll, abctime clk )
{
printf( "Iter %6d : ", Iter );
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->pPars->nVars );
printf( " " );
printf( "Cla =%9d ", bmcg_sat_solver_clausenum(p->pSat) );
printf( "Lazy =%6d ", nLazyAll );
printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
Abc_PrintTime( 1, "Time", clk );
//Zyx_ManEvalStats( p );
//Abc_PrintTime( 1, "Eval", p->clkEval );
}
void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
int status, Iter, iMint = 0, fCompl = 0, nLazyAll = 0, nSols = 0;
abctime clkTotal = Abc_Clock(), clk = Abc_Clock(); Zyx_Man_t * p;
word pTruth[16];
if ( !pPars->fMajority )
{
Abc_TtReadHex( pTruth, pPars->pTtStr );
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
}
assert( pPars->nVars <= 10 );
assert( pPars->nLutSize <= 6 );
p = Zyx_ManAlloc( pPars, pPars->fMajority ? NULL : pTruth );
printf( "Running exact synthesis for %d-input function with %d %d-input %s...\n",
p->pPars->nVars, p->pPars->nNodes, p->pPars->nLutSize, p->pPars->fMajority ? "MAJ-gates" : "LUTs" );
for ( Iter = 0 ; ; Iter++ )
{
while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
{
int nLazy = Zyx_ManAddCnfLazyTopo( p );
if ( nLazy == -1 )
{
printf( "Became UNSAT after adding lazy constraints.\n" );
status = GLUCOSE_UNSAT;
break;
}
//printf( "Added %d lazy constraints.\n\n", nLazy );
if ( nLazy == 0 )
break;
nLazyAll += nLazy;
}
if ( status == GLUCOSE_UNSAT )
break;
// find mismatch
iMint = Zyx_ManEval( p );
if ( iMint == -1 )
{
if ( pPars->fEnumSols )
{
nSols++;
if ( pPars->fVerbose )
{
Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
clk = Abc_Clock();
}
Zyx_ManPrintSolution( p, fCompl, nSols==1 );
if ( !Zyx_ManAddCnfBlockSolution( p ) )
{
status = GLUCOSE_UNSAT;
break;
}
continue;
}
else
break;
}
if ( pPars->fUseIncr ? !Zyx_ManAddCnfLazyFunc2(p, iMint) : !Zyx_ManAddCnfLazyFunc(p, iMint) )
{
printf( "Became UNSAT after adding constraints for minterm %d\n", iMint );
status = GLUCOSE_UNSAT;
break;
}
status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
if ( pPars->fVerbose && (!pPars->fUseIncr || Iter % 100 == 0) )
{
Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clk );
clk = Abc_Clock();
}
if ( status == GLUCOSE_UNSAT )
break;
}
if ( pPars->fVerbose )
Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
if ( pPars->fEnumSols )
printf( "Finished enumerating %d solutions.\n", nSols );
else if ( iMint == -1 )
Zyx_ManPrintSolution( p, fCompl, 1 );
else
printf( "The problem has no solution.\n" );
//Zyx_ManEvalStats( p );
printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
Zyx_ManFree( p );
}
/**Function*************************************************************
Synopsis [Tests solution to the exact synthesis problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Zyx_TestGetTruthTablePars( char * pFileName, word * pTruth, int * nVars, int * nLutSize, int * nNodes )
{
char Symb, * pCur, * pBuffer = Abc_UtilStrsav( pFileName );
int nLength;
for ( pCur = pBuffer; *pCur; pCur++ )
if ( !Abc_TtIsHexDigit(*pCur) )
break;
Symb = *pCur; *pCur = 0;
nLength = (int)strlen(pBuffer);
if ( nLength == 1 )
*nVars = 2;
else if ( nLength == 2 )
*nVars = 3;
else if ( nLength == 4 )
*nVars = 4;
else if ( nLength == 8 )
*nVars = 5;
else if ( nLength == 16 )
*nVars = 6;
else if ( nLength == 32 )
*nVars = 7;
else if ( nLength == 64 )
*nVars = 8;
else
{
ABC_FREE( pBuffer );
printf( "Invalid truth table size.\n" );
return 0;
}
Abc_TtReadHex( pTruth, pBuffer );
*pCur = Symb;
// read LUT size
while ( *pCur && *pCur++ != '-' );
if ( *pCur == 0 )
{
ABC_FREE( pBuffer );
printf( "Expecting \'-\' after truth table before LUT size.\n" );
return 0;
}
// read node count
*nLutSize = atoi(pCur);
while ( *pCur && *pCur++ != '-' );
if ( *pCur == 0 )
{
ABC_FREE( pBuffer );
printf( "Expecting \'-\' after LUT size before node count.\n" );
return 0;
}
*nNodes = atoi(pCur);
ABC_FREE( pBuffer );
return 1;
}
static inline word * Zyx_TestTruth( Vec_Wrd_t * vInfo, int i, int nWords ) { return Vec_WrdEntryP(vInfo, nWords * i); }
Vec_Wrd_t * Zyx_TestCreateTruthTables( int nVars, int nNodes )
{
int i, nWords = Abc_TtWordNum(nVars);
Vec_Wrd_t * vInfo = Vec_WrdStart( nWords * (nVars + nNodes + 1) );
for ( i = 0; i < nVars; i++ )
Abc_TtIthVar( Zyx_TestTruth(vInfo, i, nWords), i, nVars );
//Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
return vInfo;
}
int Zyx_TestReadNode( char * pLine, Vec_Wrd_t * vTruths, int nVars, int nLutSize, int iObj )
{
int k, j, nWords = Abc_TtWordNum(nVars);
word * pFaninsW[6]; char * pTruth, * pFanins;
word * pThis, * pLast = Zyx_TestTruth( vTruths, Vec_WrdSize(vTruths)/nWords - 1, nWords );
if ( pLine[strlen(pLine)-1] == '\n' ) pLine[strlen(pLine)-1] = 0;
if ( pLine[strlen(pLine)-1] == '\r' ) pLine[strlen(pLine)-1] = 0;
if ( pLine[0] == 0 )
return 0;
if ( (int)strlen(pLine) != 1 + nLutSize + (1 << nLutSize) )
{
printf( "Node representation has %d chars (expecting %d chars).\n", (int)strlen(pLine), 1 + nLutSize + (1 << nLutSize) );
return 0;
}
if ( pLine[0] != 'A' + iObj )
{
printf( "The output node in line %s is not correct.\n", pLine );
return 0;
}
pTruth = pLine + 1;
pFanins = pTruth + (1 << nLutSize);
for ( k = nLutSize - 1; k >= 0; k-- )
pFaninsW[k] = Zyx_TestTruth( vTruths, pFanins[k] >= 'a' ? pFanins[k] - 'a' : pFanins[k] - 'A', nWords );
pThis = Zyx_TestTruth(vTruths, iObj, nWords);
Abc_TtConst0( pThis, nWords );
for ( k = 0; k < (1 << nLutSize); k++ )
{
if ( pTruth[(1 << nLutSize) - 1 - k] == '0' )
continue;
Abc_TtConst1( pLast, nWords );
for ( j = 0; j < nLutSize; j++ )
Abc_TtAndCompl( pLast, pLast, 0, pFaninsW[j], !((k >> j) & 1), nWords );
Abc_TtOr( pThis, pThis, pLast, nWords );
}
//Dau_DsdPrintFromTruth( pThis, nVars );
return 1;
}
void Zyx_TestExact( char * pFileName )
{
int iObj, nStrs = 0, nVars = -1, nLutSize = -1, nNodes = -1;
word * pImpl, pSpec[4]; Vec_Wrd_t * vInfo; char Line[1000];
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Cannot open input file \"%s\".\n", pFileName );
return;
}
if ( !Zyx_TestGetTruthTablePars( pFileName, pSpec, &nVars, &nLutSize, &nNodes ) )
return;
if ( nVars > 8 )
{
printf( "This tester does not support functions with more than 8 inputs.\n" );
return;
}
if ( nLutSize > 6 )
{
printf( "This tester does not support nodes with more than 6 inputs.\n" );
return;
}
if ( nNodes > 16 )
{
printf( "This tester does not support structures with more than 16 inputs.\n" );
return;
}
vInfo = Zyx_TestCreateTruthTables( nVars, nNodes );
for ( iObj = nVars; fgets(Line, 1000, pFile) != NULL; iObj++ )
{
if ( Zyx_TestReadNode( Line, vInfo, nVars, nLutSize, iObj ) )
continue;
if ( iObj != nVars + nNodes )
{
printf( "The number of nodes in the structure is not correct.\n" );
break;
}
nStrs++;
pImpl = Zyx_TestTruth( vInfo, iObj-1, Abc_TtWordNum(nVars) );
if ( Abc_TtEqual( pImpl, pSpec, Abc_TtWordNum(nVars) ) )
printf( "Structure %3d : Verification successful.\n", nStrs );
else
{
printf( "Structure %3d : Verification FAILED.\n", nStrs );
printf( "Implementation: " ); Dau_DsdPrintFromTruth( pImpl, nVars );
printf( "Specification: " ); Dau_DsdPrintFromTruth( pSpec, nVars );
}
iObj = nVars - 1;
}
Vec_WrdFree( vInfo );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END