diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
| commit | 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (patch) | |
| tree | fe4ae0c41d0481c1c3f9eec7689f49cba58cd4e8 /src/aig/dch/dchMan.c | |
| parent | 73c8aa7c400bab320cea56529241e1d396f1e0f5 (diff) | |
| download | abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.gz abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.bz2 abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.zip | |
Version abc80905
Diffstat (limited to 'src/aig/dch/dchMan.c')
| -rw-r--r-- | src/aig/dch/dchMan.c | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index 6c005fbf..a5faa2a6 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -170,16 +170,21 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) sat_solver_setnvars( p->pSat, 1000 ); // var 0 is not used // var 1 is reserved for const1 node - add the clause - Lit = toLit( 1 ); + p->nSatVars = 1; +// p->nSatVars = 0; + Lit = toLit( p->nSatVars ); if ( p->pPars->fPolarFlip ) Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - p->nSatVars = 2; + Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ ); + p->nRecycles++; p->nCallsSince = 0; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |