Version abc70711

4 files changed, 26 insertions, 0 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index ee52520a..29195d19 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -117,6 +117,7 @@ struct Fra_Man_t_
     int              nSatProof;
     int              nSatFails;
     int              nSatFailsReal;
+    int              nSpeculs;         
     // runtime
     int              timeSim;
     int              timeTrav;
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
index 86cbbc9e..a360ce9b 100644
--- a/src/aig/fra/fraAnd.c
+++ b/src/aig/fra/fraAnd.c
@@ -51,6 +51,8 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
     // get the fraiged node
     pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
+        return pObjFraig;
     Dar_Regular(pObjFraig)->pData = p;
     // get representative of this class
     pObjOldRepr = Fra_ObjRepr(pObjOld);
@@ -79,14 +81,26 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     }
     if ( RetValue == -1 ) // failed
     {
+        Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
+        Vec_Ptr_t * vNodes;
+
         if ( !p->pPars->fSpeculate )
             return pObjFraig;
         // substitute the node
 //        pObjOld->fMarkB = 1;
+        p->nSpeculs++;
+
+        vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+        printf( "%d ", Vec_PtrSize(vNodes) );
+        Vec_PtrFree( vNodes );
+
         return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
+//    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
     // simulate the counter-example and return the Fraig node
+//    printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
     Fra_Resimulate( p );
+//    printf( "Representaive after  = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
     assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
     return pObjFraig;
 }
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index ac6a4f4a..33421423 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -334,6 +334,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
     Dar_Obj_t * pObj, ** ppThis;
     int i;
     assert( ppClass[0] != NULL && ppClass[1] != NULL );
+
     // check if the class is going to be refined
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
         if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
@@ -349,6 +350,15 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
             Vec_PtrPush( p->vClassOld, pObj );
         else
             Vec_PtrPush( p->vClassNew, pObj );
+/*
+    printf( "Refining class (" );
+    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+        printf( "%d,", pObj->Id );
+    printf( ") + (" );
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+        printf( "%d,", pObj->Id );
+    printf( ")\n" );
+*/
     // put the nodes back into the class memory
     Vec_PtrForEachEntry( p->vClassOld, pObj, i )
     {
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 67921318..19ed6c03 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -205,6 +205,7 @@ void Fra_ManPrint( Fra_Man_t * p )
     PRT( "Class refining  ", p->timeRef   );
     PRT( "TOTAL RUNTIME   ", p->timeTotal );
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    printf( "Speculations = %d.\n", p->nSpeculs );
 }
 
 ////////////////////////////////////////////////////////////////////////