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

An improvement to 'twoexact' and 'lutexact'.

This commit is contained in:
Alan Mishchenko 2017-12-06 11:18:43 -08:00
parent c4322a0afd
commit 67181d0446
5 changed files with 63 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/abci/abc.c
View File

@ -8241,7 +8241,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-IN <num>] [-fcagvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-IN <num>] [-agvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", nNodes );
@ -8346,7 +8346,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-INK <num>] [-fcagvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-INK <num>] [-agvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", nNodes );

20
src/sat/bmc/bmcMaj.c
View File

@ -628,6 +628,16 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
return 0;
}
}
// node ordering
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
return 0;
}
// two input functions
for ( k = 0; k < 3; k++ )
{
@ -1007,6 +1017,16 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
return 0;
}
}
// node ordering
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
return 0;
}
if ( p->nLutSize != 2 )
continue;
// two-input functions

22
src/sat/bmc/bmcMaj2.c
View File

@ -735,6 +735,16 @@ static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
return 0;
}
}
// node ordering
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
return 0;
}
// two input functions
for ( k = 0; k < 3; k++ )
{
@ -1126,6 +1136,18 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
return 0;
}
}
//printf( "Node %d:\n", i );
//sat_solver_flip_print_clause( p->pSat );
// node ordering
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
return 0;
}
if ( p->nLutSize != 2 )
continue;
// two-input functions

3
src/sat/bsat/satSolver.c
View File

@ -1716,12 +1716,11 @@ void sat_solver_rollback( sat_solver* s )
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
int fVerbose = 0;
lit *i,*j;
int maxvar;
lit last;
assert( begin < end );
if ( fVerbose )
if ( s->fPrintClause )
{
for ( i = begin; i < end; i++ )
printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );

31
src/sat/bsat/satSolver.h
View File

@ -158,6 +158,7 @@ struct sat_solver_t
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
int fVerbose;
int fPrintClause;
stats_t stats;
int nLearntMax; // max number of learned clauses
@ -212,17 +213,21 @@ static inline clause * clause_read( sat_solver * s, cla h )
return Sat_MemClauseHand( &s->Mem, h );
}
static int sat_solver_var_value( sat_solver* s, int v )
static inline int sat_solver_var_value( sat_solver* s, int v )
{
assert( v >= 0 && v < s->size );
return (int)(s->model[v] == l_True);
}
static int sat_solver_var_literal( sat_solver* s, int v )
static inline int sat_solver_var_literal( sat_solver* s, int v )
{
assert( v >= 0 && v < s->size );
return toLitCond( v, s->model[v] != l_True );
}
static void sat_solver_act_var_clear(sat_solver* s)
static inline void sat_solver_flip_print_clause( sat_solver* s )
{
s->fPrintClause ^= 1;
}
static inline void sat_solver_act_var_clear(sat_solver* s)
{
int i;
if ( s->VarActType == 0 )
@ -245,7 +250,7 @@ static void sat_solver_act_var_clear(sat_solver* s)
}
else assert(0);
}
static void sat_solver_compress(sat_solver* s)
static inline void sat_solver_compress(sat_solver* s)
{
if ( s->qtail != s->qhead )
{
@ -254,19 +259,19 @@ static void sat_solver_compress(sat_solver* s)
(void) RetValue;
}
}
static void sat_solver_delete_p( sat_solver ** ps )
static inline void sat_solver_delete_p( sat_solver ** ps )
{
if ( *ps )
sat_solver_delete( *ps );
*ps = NULL;
}
static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
static inline void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
{
int i;
for ( i = 0; i < nVars; i++ )
s->polarity[pVars[i]] = 0;
}
static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
static inline void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
{
int i;
for ( i = 0; i < s->size; i++ )
@ -274,27 +279,27 @@ static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
for ( i = 0; i < nVars; i++ )
s->polarity[pVars[i]] = 1;
}
static void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
static inline void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
{
int i;
for ( i = 0; i < nLits; i++ )
s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]);
}
static int sat_solver_final(sat_solver* s, int ** ppArray)
static inline int sat_solver_final(sat_solver* s, int ** ppArray)
{
*ppArray = s->conf_final.ptr;
return s->conf_final.size;
}
static abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
static inline abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
{
int fNotUseRandomOld = s->fNotUseRandom;
s->fNotUseRandom = fNotUseRandom;
@ -330,11 +335,11 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
}
return nVars;
}
static void sat_solver_set_runid( sat_solver *s, int id )
static inline void sat_solver_set_runid( sat_solver *s, int id )
{
s->RunId = id;
}
static void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) )
static inline void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) )
{
s->pFuncStop = fnct;
}