From 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 5 Sep 2008 08:01:00 -0700 Subject: Version abc80905 --- src/aig/dch/dchMan.c | 9 +++++++-- src/aig/dch/dchSimSat.c | 7 +++++-- 2 files changed, 12 insertions(+), 4 deletions(-) (limited to 'src/aig/dch') 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 1fefa6eb..7a6865bd 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); if ( Aig_ObjIsPi(pObj) ) { - Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj ); - int nVarNum = Dch_ObjSatNum( p, pObjFraig ); + Aig_Obj_t * pObjFraig; + int nVarNum; + pObjFraig = Dch_ObjFraig( pObj ); + assert( !Aig_IsComplement(pObjFraig) ); + nVarNum = Dch_ObjSatNum( p, pObjFraig ); // get the value from the SAT solver // (account for the fact that some vars may be minimized away) pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); -- cgit v1.2.3