diff options
Diffstat (limited to 'src/aig/dch')
| -rw-r--r-- | src/aig/dch/dchChoice.c | 2 | ||||
| -rw-r--r-- | src/aig/dch/dchClass.c | 8 | ||||
| -rw-r--r-- | src/aig/dch/dchMan.c | 9 | ||||
| -rw-r--r-- | src/aig/dch/dchSim.c | 2 | ||||
| -rw-r--r-- | src/aig/dch/dchSimSat.c | 2 | ||||
| -rw-r--r-- | src/aig/dch/dchSweep.c | 1 |
6 files changed, 15 insertions, 9 deletions
diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c index ee1ce034..19689051 100644 --- a/src/aig/dch/dchChoice.c +++ b/src/aig/dch/dchChoice.c @@ -89,7 +89,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) nEquivs++; } } - printf( "Removed %d classes.\n", Counter ); +// printf( "Removed %d classes.\n", Counter ); if ( Counter ) Dch_DeriveChoiceCountEquivs( pAig ); diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c index ab306ca9..5d042847 100644 --- a/src/aig/dch/dchClass.c +++ b/src/aig/dch/dchClass.c @@ -48,7 +48,7 @@ struct Dch_Cla_t_ Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting // procedures used for class refinement void * pManData; - unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns has key of the node + unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *); // returns hash key of the node int (*pFuncNodeIsConst) (void *,Aig_Obj_t *); // returns 1 if the node is a constant int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement }; @@ -158,7 +158,7 @@ Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ) ***********************************************************************/ void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, - unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns has key of the node + unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), // returns hash key of the node int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), // returns 1 if the node is a constant int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement { @@ -481,7 +481,7 @@ int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi if ( Vec_PtrSize(p->vClassNew) > 1 ) Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) ); - // skip of the class should not be recursively refined + // check if the class should be recursively refined if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 ) return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 ); return 1; @@ -568,6 +568,8 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs { Aig_Obj_t * pObj, * pReprNew, ** ppClassNew; int i; + if ( Vec_PtrSize(vRoots) == 0 ) + return 0; // collect the nodes to be refined Vec_PtrClear( p->vClassNew ); Vec_PtrForEachEntry( vRoots, pObj, i ) 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; } diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c index 49734b5a..44a96970 100644 --- a/src/aig/dch/dchSim.c +++ b/src/aig/dch/dchSim.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 [Performs random simulation at the beginning.] diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index cdfb9271..1fefa6eb 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -86,6 +86,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) ); Dch_ManCollectTfoCands_rec( p, pObj1 ); Dch_ManCollectTfoCands_rec( p, pObj2 ); + Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); + Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); } /**Function************************************************************* diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c index 019f6707..36c5fc33 100644 --- a/src/aig/dch/dchSweep.c +++ b/src/aig/dch/dchSweep.c @@ -86,6 +86,7 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj ) Dch_ManResimulateCex( p, pObj, pObjRepr ); else Dch_ManResimulateCex2( p, pObj, pObjRepr ); + assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr ); } /**Function************************************************************* |