Version abc80901

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*************************************************************