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

Improvement to CNF encoding of cardinality constraints proposed by Mathias Soaken.

This commit is contained in:
Alan Mishchenko 2016-06-07 00:22:32 -07:00
parent 31b2e8bebd
commit 998aeff15e
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/aig/gia/giaSatMap.c
View File

@ -314,6 +314,12 @@ static inline void Sbm_AddCardinConstrMerge( sat_solver * p, int * pVars, int lo
Sbm_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars ); Sbm_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars );
for ( i = lo+r; i < hi-r; i += step ) for ( i = lo+r; i < hi-r; i += step )
Sbm_AddSorter( p, pVars, i, i+r, pnVars ); Sbm_AddSorter( p, pVars, i, i+r, pnVars );
for ( i = lo+r; i < hi-r-1; i += r )
{
lit Lits[2] = { Abc_Var2Lit(pVars[i], 0), Abc_Var2Lit(pVars[i+r], 1) };
int Cid = sat_solver_addclause( p, Lits, Lits + 2 );
assert( Cid );
}
} }
} }
static inline void Sbm_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnVars ) static inline void Sbm_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnVars )