diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-03-15 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-03-15 08:01:00 -0700 |
| commit | 770bc99e79baa07a9d2cc7a25dc30ee86ed34d91 (patch) | |
| tree | c1240cf561832c51469197f7d01c91844b09c6a7 /src/opt | |
| parent | 81b51657f5c502e45418630614fd56e5e1506230 (diff) | |
| download | abc-770bc99e79baa07a9d2cc7a25dc30ee86ed34d91.tar.gz abc-770bc99e79baa07a9d2cc7a25dc30ee86ed34d91.tar.bz2 abc-770bc99e79baa07a9d2cc7a25dc30ee86ed34d91.zip | |
Version abc90315
Diffstat (limited to 'src/opt')
| -rw-r--r-- | src/opt/mfs/mfsSat.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index a35d67e4..eab80c53 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -43,11 +43,16 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) { int Lits[MFS_FANIN_MAX]; int RetValue, nBTLimit, iVar, b, Mint; +// int nConfs = p->pSat->stats.conflicts; if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts ) return -1; nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0; RetValue = sat_solver_solve( p->pSat, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False ); +//printf( "%c", RetValue==l_Undef ? '?' : (RetValue==l_False ? '-' : '+') ); +//printf( "%d ", p->pSat->stats.conflicts-nConfs ); +//if ( RetValue==l_False ) +//printf( "\n" ); if ( RetValue == l_Undef ) return -1; if ( RetValue == l_False ) |