Version abc80802_2

1 files changed, 36 insertions, 3 deletions

diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
index 9882dd05..49734b5a 100644
--- a/src/aig/dch/dchSim.c
+++ b/src/aig/dch/dchSim.c
@@ -6,7 +6,7 @@
 
   PackageName [Computation of equivalence classes using simulation.]
 
-  Synopsis    [Calls to the SAT solver.]
+  Synopsis    [Performs random simulation at the beginning.]
 
   Author      [Alan Mishchenko]
   
@@ -39,6 +39,38 @@ static inline unsigned Dch_ObjRandomSim()
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the node appears to be constant 1 candidate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
+{
+    return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the nodes appear equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes hash value of the node using its simulation info.]
 
   Description []
@@ -241,14 +273,15 @@ Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbo
     // hash nodes by sim info
     Dch_ClassesPrepare( pClasses, 0, 0 );
     // iterate random simulation
-    for ( i = 0; i < 3; i++ )
+    for ( i = 0; i < 7; i++ )
     {
         Dch_PerformRandomSimulation( pAig, vSims );
         Dch_ClassesRefine( pClasses );
     }
     // clean up and return
-    Dch_ClassesSetData( pClasses, NULL, NULL, NULL, NULL );
     Vec_PtrFree( vSims );
+    // prepare class refinement procedures
+    Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
     return pClasses;
 }