From 73c8aa7c400bab320cea56529241e1d396f1e0f5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Sep 2008 08:01:00 -0700 Subject: Version abc80901 --- src/aig/dch/dchMan.c | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/aig/dch/dchMan.c') diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index 02d91ca3..6c005fbf 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [Computation of equivalence classes using simulation.] + PackageName [Choice computation for tech-mapping.] Synopsis [Calls to the SAT solver.] @@ -168,12 +168,13 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) } p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is reserved for const1 node - add the clause - Lit = toLit( 0 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + Lit = toLit( 1 ); if ( p->pPars->fPolarFlip ) Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - p->nSatVars = 1; + p->nSatVars = 2; p->nRecycles++; p->nCallsSince = 0; } -- cgit v1.2.3