Improvements to false path detection.

4 files changed, 352 insertions, 28 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 85bf8ab0..af35803a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1062,6 +1062,7 @@ extern Gia_Man_t *         Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int V
 extern Gia_Man_t *         Gia_ManDupExist( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern Gia_Man_t *         Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
 extern Gia_Man_t *         Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index d8ddff38..45c017bb 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1459,6 +1459,45 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManDupDfs3_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pObj->Value = Gia_ManAppendCi(pNew);
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupDfs3_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupDfs3_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pRoot )
+{
+    Gia_Man_t * pNew;
+    assert( Gia_ObjIsAnd(pRoot) );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManDupDfs3_rec( pNew, p, pRoot );
+    Gia_ManAppendCo( pNew, pRoot->Value );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
 {
     Gia_Man_t * pNew;
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c
index c918559f..0d609436 100644
--- a/src/aig/gia/giaFalse.c
+++ b/src/aig/gia/giaFalse.c
@@ -47,24 +47,43 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Gia_ManFalseRebuildOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vHook, int fVerbose, int fVeryVerbose )
 {
-    Gia_Obj_t * pObj, * pPrev = NULL; 
-    int i, iObjValue, iPrevValue = -1;
-    if ( fVerbose )
+    Gia_Obj_t * pObj, * pObj1, * pPrev = NULL;
+    int i, CtrlValue = 0, iPrevValue = -1;
+    pObj = Gia_ManObj( p, Vec_IntEntry(vHook, 0) );
+    if ( Vec_IntSize(vHook) == 1 )
     {
-        printf( "Eliminating path: " );
-        Vec_IntPrint( vHook );
+        pObj->Value = 0; // what if stuck at 1???
+        return;
     }
+    assert( Vec_IntSize(vHook) >= 2 );
+    // find controlling value
+    pObj1 = Gia_ManObj( p, Vec_IntEntry(vHook, 1) );
+    if ( Gia_ObjFanin0(pObj1) == pObj )
+        CtrlValue = Gia_ObjFaninC0(pObj1);
+    else if ( Gia_ObjFanin1(pObj1) == pObj )
+        CtrlValue = Gia_ObjFaninC1(pObj1);
+    else assert( 0 );
+//    printf( "%d ", CtrlValue );
+    // rewrite the path
     Gia_ManForEachObjVec( vHook, p, pObj, i )
     {
-        if ( fVeryVerbose )
-            Gia_ObjPrint( p, pObj );
-        iObjValue = pObj->Value;
-        pObj->Value = i ? Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)) : 0;
+        int iObjValue = pObj->Value;
+        pObj->Value = i ? Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)) : CtrlValue;
         if ( pPrev )
             pPrev->Value = iPrevValue;
         iPrevValue = iObjValue;
         pPrev = pObj;
     }
+    if ( fVeryVerbose )
+    {
+        printf( "Eliminated path: " );
+        Vec_IntPrint( vHook );
+        Gia_ManForEachObjVec( vHook, p, pObj, i )
+        {
+            printf( "Level %3d : ", Gia_ObjLevel(p, pObj) );
+            Gia_ObjPrint( p, pObj );
+        }
+    }
 }
 Gia_Man_t * Gia_ManFalseRebuild( Gia_Man_t * p, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
 {
@@ -82,7 +101,7 @@ Gia_Man_t * Gia_ManFalseRebuild( Gia_Man_t * p, Vec_Wec_t * vHooks, int fVerbose
         {
             if ( Vec_WecLevelSize(vHooks, i) > 0 )
             {
-                if ( fVerbose )
+                if ( fVeryVerbose )
                     printf( "Path %d : ", Counter++ );
                 Gia_ManFalseRebuildOne( pNew, p, Vec_WecEntry(vHooks, i), fVerbose, fVeryVerbose );
             }
@@ -130,7 +149,7 @@ void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPath
 Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     Vec_Int_t * vPath = Vec_IntAlloc( p->nLevels );
-    Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
+    Gia_ManCollectPath_rec( p, Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj, vPath );
     return vPath;
 }
 
@@ -148,7 +167,7 @@ Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj )
 void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
 {
     sat_solver * pSat;
-    Gia_Obj_t * pObj;
+    Gia_Obj_t * pObj, * pFanin;
     Gia_Obj_t * pPivot = Gia_ManCo( p, iOut );
     Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels );
     Vec_Int_t * vPath = Gia_ManCollectPath( p, pPivot );
@@ -164,15 +183,9 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
     // create SAT solver
     pSat = sat_solver_new();
     sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
-    sat_solver_setnvars( pSat, Vec_IntSize(vPath) + 2 * Vec_IntSize(vObjs) );
-    Shift[0] = Vec_IntSize(vPath);
-    Shift[1] = Vec_IntSize(vPath) + Vec_IntSize(vObjs);
-    // add CNF for the path
-    Gia_ManForEachObjVec( vPath, p, pObj, i )
-    {
-        sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 );
-        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
-    }
+    sat_solver_setnvars( pSat, 3 * Vec_IntSize(vPath) + 2 * Vec_IntSize(vObjs) );
+    Shift[0] = 3 * Vec_IntSize(vPath);
+    Shift[1] = 3 * Vec_IntSize(vPath) + Vec_IntSize(vObjs);
     // add CNF for the cone
     Gia_ManForEachObjVec( vObjs, p, pObj, i )
     {
@@ -185,8 +198,41 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
             Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1], 
             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
     }
+    // add CNF for the path
+    Gia_ManForEachObjVec( vPath, p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            assert( i > 0 );
+            pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
+            if ( pFanin == Gia_ObjFanin0(pObj) )
+            {
+                sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), 
+                    i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0], 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+                sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), 
+                    i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1], 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+            }
+            else if ( pFanin == Gia_ObjFanin1(pObj) )
+            {
+                sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), 
+                    Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath), 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+                sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), 
+                    Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath), 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+            }
+            else assert( 0 );
+            sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+            sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 );
+        else assert( 0 );
+        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+    }
     // call the SAT solver
-    status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)nTimeOut, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_False )
     {
         int iBeg, iEnd;
@@ -196,13 +242,13 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
         if ( iEnd - iBeg < 20 )
         {
             // check if nodes on the path are already used
-            for ( i = iBeg; i <= iEnd; i++ )
+            for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
                 if ( Vec_WecLevelSize(vHooks, Vec_IntEntry(vPath, i)) > 0 )
                     break;
             if ( i > iEnd )
             {
                 Vec_Int_t * vHook = Vec_WecEntry(vHooks, Vec_IntEntry(vPath, iEnd));
-                for ( i = iBeg; i <= iEnd; i++ )
+                for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
                     Vec_IntPush( vHook, Vec_IntEntry(vPath, i) );
             }
         }
@@ -216,7 +262,7 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
             printf( "There is no false path. " );
         else
         {
-            printf( "False path contains %d nodes (out of %d):  ", nLits, Vec_IntSize(vLits) );
+            printf( "False path contains %d nodes (out of %d):  ", nLits, Vec_IntSize(vPath) );
             printf( "top = %d  ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[0])) );
             if ( fVeryVerbose )
                 for ( i = 0; i < nLits; i++ )
@@ -230,7 +276,7 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
     Vec_IntFree( vPath );
     Vec_IntFree( vLits );
 }
-Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManCheckFalse2( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew;
     Vec_Wec_t * vHooks;
@@ -238,7 +284,7 @@ Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int f
     Vec_Flt_t * vWeights;
     Gia_Obj_t * pObj;
     int i;
-    srand( 111 );
+//    srand( 111 );
     Gia_ManLevelNum( p );
     // create PO weights
     vWeights = Vec_FltAlloc( Gia_ManCoNum(p) );
@@ -264,6 +310,244 @@ Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int f
     return pNew;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFalseRebuildPath( Gia_Man_t * p, Vec_Int_t * vHooks, int fVerbose, int fVeryVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    int iPathEnd = Vec_IntEntryLast(vHooks);
+    pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) / 3 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue(p);
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( iPathEnd == i )
+                Gia_ManFalseRebuildOne( pNew, p, vHooks, fVerbose, fVeryVerbose );
+            else
+                pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, int fVerbose, int fVeryVerbose )
+{
+    sat_solver * pSat;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pFanin;
+    Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels );
+    Vec_Int_t * vPath = Gia_ManCollectPath( p, Gia_ManObj(p, iObj) );
+    int nLits = 0, * pLits = NULL;
+    int i, Shift[2], status;
+    abctime clkStart = Abc_Clock();
+    // collect objects and assign SAT variables
+    Vec_Int_t * vObjs = Gia_ManCollectNodesCis( p, &iObj, 1 );
+    Gia_ManForEachObjVec( vObjs, p, pObj, i )
+        pObj->Value = Vec_IntSize(vObjs) - 1 - i;
+    // create SAT solver
+    pSat = sat_solver_new();
+    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+    sat_solver_setnvars( pSat, 3 * Vec_IntSize(vPath) + 2 * Vec_IntSize(vObjs) );
+    Shift[0] = 3 * Vec_IntSize(vPath);
+    Shift[1] = 3 * Vec_IntSize(vPath) + Vec_IntSize(vObjs);
+    // add CNF for the cone
+    Gia_ManForEachObjVec( vObjs, p, pObj, i )
+    {
+        if ( !Gia_ObjIsAnd(pObj) )
+            continue;
+        sat_solver_add_and( pSat, pObj->Value + Shift[0], 
+            Gia_ObjFanin0(pObj)->Value + Shift[0], Gia_ObjFanin1(pObj)->Value + Shift[0], 
+            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+        sat_solver_add_and( pSat, pObj->Value + Shift[1], 
+            Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1], 
+            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+    }
+    // add CNF for the path
+    Gia_ManForEachObjVec( vPath, p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            assert( i > 0 );
+            pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
+            if ( pFanin == Gia_ObjFanin0(pObj) )
+            {
+                sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), 
+                    i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0], 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+                sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), 
+                    i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1], 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+            }
+            else if ( pFanin == Gia_ObjFanin1(pObj) )
+            {
+                sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), 
+                    Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath), 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+                sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), 
+                    Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath), 
+                    Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 
+            }
+            else assert( 0 );
+            sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+            sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 );
+        else assert( 0 );
+        Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
+    }
+    // call the SAT solver
+    status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)nTimeOut, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    Vec_IntClear( vLits );
+    if ( status == l_False )
+    {
+        int iBeg, iEnd;
+        nLits = sat_solver_final( pSat, &pLits );
+        iBeg  = Abc_Lit2Var(pLits[nLits-1]);
+        iEnd  = Abc_Lit2Var(pLits[0]);
+        assert( iBeg <= iEnd );
+        // collect path
+        for ( i = Abc_MaxInt(iBeg-1, 0); i <= iEnd; i++ )
+//        for ( i = 0; i < Vec_IntSize(vPath); i++ )
+            Vec_IntPush( vLits, Vec_IntEntry(vPath, i) );
+    }
+    if ( fVerbose )
+    {
+        printf( "PO %6d : Level = %3d  ", iOut, Gia_ObjLevelId(p, iObj) );
+        if ( status == l_Undef )
+            printf( "Timeout reached after %d seconds. ", nTimeOut );
+        else if ( status == l_True )
+            printf( "There is no false path. " );
+        else
+        {
+            printf( "False path contains %d nodes (out of %d):  ", Vec_IntSize(vLits), Vec_IntSize(vPath) );
+            if ( fVeryVerbose )
+                for ( i = nLits-1; i >= 0; i-- )
+                    printf( "%d ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[i])) );
+            printf( "  " );
+        }
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+    }
+    sat_solver_delete( pSat );
+    Vec_IntFree( vObjs );
+    Vec_IntFree( vPath );
+    // update the AIG
+    pNew = Vec_IntSize(vLits) ? Gia_ManFalseRebuildPath( p, vLits, fVerbose, fVeryVerbose ) : NULL;
+    Vec_IntFree( vLits );
+/*
+    if ( pNew )
+    {
+        Gia_Man_t * pTemp = Gia_ManDupDfsNode( p, Gia_ManObj(p, iObj) );
+        Gia_AigerWrite( pTemp, "false.aig", 0, 0 );
+        Abc_Print( 1, "Dumping cone with %d nodes into file \"%s\".\n", Gia_ManAndNum(pTemp), "false.aig" );
+        Gia_ManStop( pTemp );
+    }
+*/
+    return pNew;
+}
+Gia_Man_t * Gia_ManCheckFalseAll( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
+{
+    int Tried = 0, Changed = 0;
+    p = Gia_ManDup( p );
+    while ( 1 )
+    {
+        Gia_Man_t * pNew;
+        Gia_Obj_t * pObj;
+        int i, LevelMax, Changed0 = Changed;
+        LevelMax = Gia_ManLevelNum( p );
+        Gia_ManForEachAnd( p, pObj, i )
+        {
+            if ( Gia_ObjLevel(p, pObj) > nSlackMax )
+                continue;
+            Tried++;
+            pNew = Gia_ManCheckOne( p, -1, i, nTimeOut, fVerbose, fVeryVerbose );
+            if ( pNew == NULL )
+                continue;
+            Changed++;
+            Gia_ManStop( p );
+            p = pNew;
+            LevelMax = Gia_ManLevelNum( p );
+        }
+        if ( Changed0 == Changed )
+            break;
+    }
+//    if ( fVerbose )
+        printf( "Performed %d attempts and %d changes.\n", Tried, Changed );
+    return p;
+}
+Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
+{
+    int Tried = 0, Changed = 0;
+    Vec_Int_t * vTried;
+//    srand( 111 );
+    p = Gia_ManDup( p );
+    vTried = Vec_IntStart( Gia_ManCoNum(p) );
+    while ( 1 )
+    {
+        Gia_Man_t * pNew;
+        Gia_Obj_t * pObj;
+        int i, LevelMax, Changed0 = Changed;
+        LevelMax = Gia_ManLevelNum( p );
+        Gia_ManForEachCo( p, pObj, i )
+        {
+            if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
+                continue;
+            if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < LevelMax - nSlackMax )
+                continue;
+            if ( Vec_IntEntry( vTried, i ) )
+                continue;
+            Tried++;
+            pNew = Gia_ManCheckOne( p, i, Gia_ObjFaninId0p(p, pObj), nTimeOut, fVerbose, fVeryVerbose );
+/*
+            if ( i != 126 && pNew )
+            {
+                Gia_ManStop( pNew );
+                pNew = NULL;
+            }
+*/
+            if ( pNew == NULL )
+            {
+                Vec_IntWriteEntry( vTried, i, 1 );
+                continue;
+            }
+            Changed++;
+            Gia_ManStop( p );
+            p = pNew;
+            LevelMax = Gia_ManLevelNum( p );
+        }
+        if ( Changed0 == Changed )
+            break;
+    }
+//    if ( fVerbose )
+        printf( "Performed %d attempts and %d changes.\n", Tried, Changed );
+    Vec_IntFree( vTried );
+    return p;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f6875464..6c869c7d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28166,7 +28166,7 @@ int Abc_CommandAbc9False( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     Abc_Print( -2, "usage: &false [-ST num] [-vwh]\n" );
     Abc_Print( -2, "\t         detecting and elimintation false paths\n" );
-    Abc_Print( -2, "\t-S num : maximum slack to idetify false paths [default = %d]\n",   nSlackMax );
+    Abc_Print( -2, "\t-S num : maximum slack to identify false paths [default = %d]\n",  nSlackMax );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n",   nTimeOut );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",    fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );