Experiments with don't-cares.

abclib.dsp

@@ -5695,7 +5695,7 @@ SOURCE=.\src\proof\acec\acec.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\proof\acec\acec2Booth.c
+SOURCE=.\src\proof\acec\acec2Mult.c
 # End Source File
 # Begin Source File
 

src/base/acb/acb.h

@@ -88,9 +88,13 @@ struct Acb_Ntk_t_
     Vec_Int_t       vLevelR;    // level
     Vec_Int_t       vPathD;     // path
     Vec_Int_t       vPathR;     // path
+    Vec_Wec_t       vClauses;
+    Vec_Wec_t       vCnfs;
+    Vec_Int_t       vCover;
     // other
     Vec_Int_t       vArray0;
     Vec_Int_t       vArray1;
+    Vec_Int_t       vArray2;
 };
 
 // design
@@ -239,6 +243,7 @@ static inline int            Acb_ObjFanOffset( Acb_Ntk_t * p, int i )        { a
 static inline int *          Acb_ObjFanins( Acb_Ntk_t * p, int i )           { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i));                                   }
 static inline int            Acb_ObjFanin( Acb_Ntk_t * p, int i, int k )     { return Acb_ObjFanins(p, i)[k+1];                                                             }
 static inline int            Acb_ObjFaninNum( Acb_Ntk_t * p, int i )         { return Acb_ObjFanins(p, i)[0];                                                               }
+static inline int            Acb_ObjFanoutNum( Acb_Ntk_t * p, int i )        { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) );                                         }
 static inline int            Acb_ObjFanin0( Acb_Ntk_t * p, int i )           { return Acb_ObjFanins(p, i)[1];                                                               }
 static inline int            Acb_ObjCioId( Acb_Ntk_t * p, int i )            { return Acb_ObjFanins(p, i)[2];                                                               }
  
@@ -288,10 +293,13 @@ static inline void           Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int
 static inline int            Acb_ObjRangeSign( Acb_Ntk_t * p, int i )               { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) );                           }
 
 static inline int            Acb_ObjTravId( Acb_Ntk_t * p, int i )                  { return Vec_IntGetEntry(&p->vObjTrav, i);                                                     }
+static inline int            Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i )              { return p->nObjTravs - Vec_IntGetEntry(&p->vObjTrav, i);                                      }
 static inline int            Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i )             { return Acb_ObjTravId(p, i) == p->nObjTravs;                                                  }
 static inline int            Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i )            { return Acb_ObjTravId(p, i) == p->nObjTravs-1;                                                }
+static inline int            Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d )     { return Acb_ObjTravId(p, i) == p->nObjTravs-d;                                                }
 static inline int            Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i )            { int r = Acb_ObjIsTravIdCur(p, i);  Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs);   return r; }
 static inline int            Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i )           { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; }
+static inline int            Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d )    { int r = Acb_ObjTravIdDiff(p, i);   Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; }
 static inline int            Acb_NtkTravId( Acb_Ntk_t * p )                         { return p->nObjTravs;                                                                         }
 static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )                      { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++;                       }
 
@@ -493,6 +501,7 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
     // other
     Vec_IntErase( &p->vArray0 );    
     Vec_IntErase( &p->vArray1 );    
+    Vec_IntErase( &p->vArray2 );    
     ABC_FREE( p );
 }
 static inline int Acb_NtkNewStrId( Acb_Ntk_t * pNtk, const char * format, ...  )
@@ -663,8 +672,9 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p )
     nMem += (int)Vec_IntMemory(&p->vNtkObjs );  
     nMem += (int)Vec_IntMemory(&p->vTargets );  
     // other
+    nMem += (int)Vec_IntMemory(&p->vArray0 );
     nMem += (int)Vec_IntMemory(&p->vArray1 );
-    nMem += (int)Vec_IntMemory(&p->vArray1 );
+    nMem += (int)Vec_IntMemory(&p->vArray2 );
     return nMem;
 }
 static inline void Acb_NtkPrintStats( Acb_Ntk_t * p )

src/base/acb/acbMfs.c

@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [acb.c]
+  FileName    [abcMfs.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Hierarchical word-level netlist.]
 
-  Synopsis    []
+  Synopsis    [Optimization with don't-cares.]
 
   Author      [Alan Mishchenko]
   
@@ -14,11 +14,13 @@
 
   Date        [Ver. 1.0. Started - July 21, 2015.]
 
-  Revision    [$Id: acb.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcMfs.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
 #include "acb.h"
+#include "bool/kit/kit.h"
+#include "sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -41,7 +43,591 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+int Acb_Truth2Cnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+{
+    Vec_StrClear( vCnf );
+    if ( Truth == 0 || ~Truth == 0 )
+    {
+//        assert( nVars == 0 );
+        Vec_StrPush( vCnf, (char)(Truth == 0) );
+        Vec_StrPush( vCnf, (char)-1 );
+        return 1;
+    }
+    else 
+    {
+        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+        assert( nVars > 0 );
+        for ( c = 0; c < 2; c ++ )
+        {
+            Truth = c ? ~Truth : Truth;
+            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            assert( RetValue == 0 );
+            nCubes += Vec_IntSize( vCover );
+            Vec_IntForEachEntry( vCover, Cube, i )
+            {
+                for ( k = 0; k < nVars; k++ )
+                {
+                    Literal = 3 & (Cube >> (k << 1));
+                    if ( Literal == 1 )      // '0'  -> pos lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+                    else if ( Literal == 2 ) // '1'  -> neg lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+                    else if ( Literal != 0 )
+                        assert( 0 );
+                }
+                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+                Vec_StrPush( vCnf, (char)-1 );
+            }
+        }
+        return nCubes;
+    }
+}
+Vec_Wec_t * Acb_NtkDeriveCnf( Acb_Ntk_t * p )
+{
+    Vec_Wec_t * vCnfs = Vec_WecStart( Acb_NtkObjNumMax(p) );
+    Vec_Str_t * vCnf = Vec_StrAlloc( 100 ); int iObj;
+    Acb_NtkForEachNode( p, iObj )
+    {
+        int nCubes = Acb_Truth2Cnf( Acb_ObjTruth(p, iObj), Acb_ObjFaninNum(p, iObj), &p->vCover, vCnf );
+        Vec_Str_t * vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj );
+        Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
+        memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
+        vCnfBase->nSize = Vec_StrSize(vCnf);
+    }
+    Vec_StrFree( vCnf );
+    return vCnfs;
+}
+void Acb_CnfTranslate( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vSatVars, int iPivotVar )
+{
+    Vec_Int_t * vClause;
+    signed char Entry;
+    int i, Lit;
+    Vec_WecClear( vRes );
+    vClause = Vec_WecPushLevel( vRes );
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        if ( (int)Entry == -1 )
+        {
+            vClause = Vec_WecPushLevel( vRes );
+            continue;
+        }
+        Lit = Abc_Lit2LitV( Vec_IntArray(vSatVars), (int)Entry );
+        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
+        Vec_IntPush( vClause, Lit );
+    }
+}
+int Acb_ObjCreateCnf( sat_solver * pSat, Acb_Ntk_t * p, int iObj, Vec_Int_t * vSatVars, int iPivotVar )
+{
+    Vec_Int_t * vClause; int k, RetValue;
+    Acb_CnfTranslate( &p->vClauses, (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, iObj), vSatVars, iPivotVar );
+    Vec_WecForEachLevel( &p->vClauses, vClause, k )
+    {
+        if ( Vec_IntSize(vClause) == 0 )
+            break;
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vClause), Vec_IntLimit(vClause) );
+        if ( RetValue == 0 )
+            return 0;
+    }
+    return 1;
+}
 
+/**Function*************************************************************
+
+  Synopsis    [Constructs SAT solver for the window.]
+
+  Description [The window for the pivot node is represented as a DFS ordered array 
+  of objects (vWinObjs) whose indexes are used as SAT variable IDs (stored in p->vCopies).
+  PivotVar is the index of the pivot node in array vWinObjs.
+  The nodes before (after) PivotVar are TFI (TFO) nodes.
+  The leaf (root) nodes are labeled with Abc_LitIsCompl().
+  If fQbf is 1, returns the instance meant for QBF solving. It uses the last 
+  variable (LastVar) as the placeholder for the second copy of the pivot node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_NtkCountRoots( Vec_Int_t * vWinObjs, int PivotVar )
+{
+    int i, iObjLit, nRoots = 0;
+    Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, PivotVar + 1 )
+        nRoots += Abc_LitIsCompl(iObjLit);
+    return nRoots;
+}
+sat_solver * Acb_NtkWindow2Solver( sat_solver * pSat, Acb_Ntk_t * p, int Pivot, Vec_Int_t * vWinObjs, int fQbf )
+{
+    Vec_Int_t * vFaninVars = Vec_IntAlloc( 8 );
+    int PivotVar = Vec_IntFind(vWinObjs, Abc_Var2Lit(Pivot, 0));
+    int nRoots   = Acb_NtkCountRoots(vWinObjs, PivotVar);
+    int TfoStart = PivotVar + 1;
+    int nTfoSize = Vec_IntSize(vWinObjs) - TfoStart;
+    int LastVar  = Vec_IntSize(vWinObjs) + TfoStart + nRoots;
+    int i, k, iLit = 1, RetValue, iObj, iObjLit, iFanin, * pFanins;
+    //Vec_IntPrint( vWinObjs );
+    // mark new SAT variables
+    Vec_IntForEachEntry( vWinObjs, iObj, i )
+        Acb_ObjSetCopy( p, i, iObj );
+    // create SAT solver
+    if ( pSat == NULL )
+        pSat = sat_solver_new();
+    else
+        sat_solver_restart( pSat );
+    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + nTfoSize + nRoots + 1 );
+    // create constant 0 clause
+    sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+    // add clauses for all nodes
+    Vec_IntForEachEntryStop( vWinObjs, iObjLit, i, TfoStart )
+    {
+        if ( Abc_LitIsCompl(iObjLit) )
+            continue;
+        iObj = Abc_Lit2Var(iObjLit);
+        assert( !Acb_ObjIsCio(p, iObj) );
+        // collect SAT variables
+        Vec_IntClear( vFaninVars );
+        Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+            Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) );
+        Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) );
+        // derive CNF for the node
+        RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, -1 );
+        assert( RetValue );
+    }
+    // add second clauses for the TFO
+    Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, TfoStart )
+    {
+        iObj = Abc_Lit2Var(iObjLit);
+        assert( !Acb_ObjIsCio(p, iObj) );
+        // collect SAT variables
+        Vec_IntClear( vFaninVars );
+        Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+            Vec_IntPush( vFaninVars, (fQbf && iFanin == Pivot) ? LastVar : Acb_ObjCopy(p, iFanin) );
+        Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) );
+        // derive CNF for the node
+        RetValue = Acb_ObjCreateCnf( pSat, p, iObj, vFaninVars, fQbf ? -1 : PivotVar );
+        assert( RetValue );
+    }
+    if ( nRoots > 0 )
+    {
+        // create XOR clauses for the roots
+        int nVars = Vec_IntSize(vWinObjs) + nTfoSize;
+        Vec_IntClear( vFaninVars );
+        Vec_IntForEachEntryStart( vWinObjs, iObjLit, i, TfoStart )
+        {
+            if ( !Abc_LitIsCompl(iObjLit) )
+                continue;
+            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
+            sat_solver_add_xor( pSat, Acb_ObjCopy(p, iObj), Acb_ObjCopy(p, iObj) + nTfoSize, nVars++, 0 );
+        }
+        // make OR clause for the last nRoots variables
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
+        if ( RetValue == 0 )
+        {
+            Vec_IntFree( vFaninVars );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+        assert( sat_solver_nvars(pSat) == nVars + 1 );
+    }
+    else if ( fQbf )
+    {
+        int n, pLits[2];
+        for ( n = 0; n < 2; n++ )
+        {
+            pLits[0] = Abc_Var2Lit( PivotVar, n );
+            pLits[1] = Abc_Var2Lit( LastVar, n );
+            RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
+            assert( RetValue );
+        }
+    }
+    Vec_IntFree( vFaninVars );
+    // finalize
+    RetValue = sat_solver_simplify( pSat );
+    if ( RetValue == 0 )
+    {
+        sat_solver_delete( pSat );
+        return NULL;    
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkUnmarkWindow( Acb_Ntk_t * p, Vec_Int_t * vWin )
+{
+    int i, iObj;
+    Vec_IntForEachEntry( vWin, iObj, i )
+        Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Acb_ObjIsCritFanin( Acb_Ntk_t * p, int i, int f )  { return Acb_ObjLevelR(p, i) + Acb_ObjLevelD(p, f) == p->LevelMax; }
+Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int nTfiLevMin )
+{
+    int i, k, iObj, iFanin, iFanin2, * pFanins, * pFanins2, Lev, Level = Acb_ObjLevelD(p, Pivot);
+    // include non-critical pivot fanins AND fanins of critical pivot fanins
+    Vec_Int_t * vDivs  = Vec_IntAlloc( 100 );
+    Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, i )
+    {
+        if ( !Acb_ObjIsCritFanin(p, Pivot, iFanin) ) // non-critical fanin
+            Vec_IntPush( vDivs, iFanin ); 
+        else // critical fanin
+            Acb_ObjForEachFaninFast( p, iFanin, pFanins2, iFanin2, k )
+                Vec_IntPushUnique( vDivs, iFanin2 );
+    }
+    // continue for a few more levels
+    for ( Lev = Level-2; Lev >= nTfiLevMin; Lev-- )
+    {
+        Vec_IntForEachEntry( vDivs, iObj, i )
+            if ( Acb_ObjLevelD(p, iObj) == Lev )
+                Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+                    Vec_IntPushUnique( vDivs, iFanin );
+    }
+    // sort them by level
+    Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
+    return vDivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks TFO of divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int nFanMax )
+{
+    int iFanout, i;
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax || iObj == Pivot )
+        return;
+    Acb_ObjForEachFanout( p, iObj, iFanout, i )
+        Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax );
+}
+void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax, int nFanMax )
+{
+    int i, iObj;
+    Acb_NtkIncTravId( p );
+    Vec_IntForEachEntry( vDivs, iObj, i )
+        Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels TFO nodes with {none, root, inner} based on their type.]
+
+  Description [Assuming TFO of TFI is marked with the current trav ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
+{
+    int iFanout, i, Diff, fHasNone = 0;
+    if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 )
+        return Diff;
+    Acb_ObjSetTravIdDiff( p, iObj, 2 );
+    if ( Acb_ObjIsCo(p, iObj) || Acb_ObjLevelD(p, iObj) > nTfoLevMax )
+        return 2;
+    if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax )
+    {
+        if ( Diff == 3 )  
+            Acb_ObjSetTravIdDiff( p, iObj, 1 ); // mark root
+        return Acb_ObjTravIdDiff(p, iObj);
+    }
+    Acb_ObjForEachFanout( p, iObj, iFanout, i )
+        fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax );
+    if ( fHasNone && Diff == 3 )
+        Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root
+    else
+        Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner
+    return Acb_ObjTravIdDiff(p, iObj);
+}
+int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax )
+{
+    Acb_NtkIncTravId( p ); // none  (2)    marked (3)  unmarked (4)
+    Acb_NtkIncTravId( p ); // root  (1)
+    Acb_NtkIncTravId( p ); // inner (0)
+    assert( Acb_ObjTravIdDiff(p, Root) < 3 );
+    return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects labeled TFO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+{
+    int iFanout, i, Diff = Acb_ObjTravIdDiff(p, iObj);
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( Diff == 2 ) // root
+    {
+        Vec_IntPush( vRoots, Diff );
+        return;
+    }
+    assert( Diff == 1 );
+    Acb_ObjForEachFanout( p, iObj, iFanout, i )
+        Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots );
+    Vec_IntPush( vTfo, Diff );
+}
+void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots )
+{
+    int Res = Acb_ObjLabelTfo( p, Root, nTfoLevMax, nFanMax );
+    Vec_Int_t * vTfo   = *pvTfo   = Vec_IntAlloc( 100 );
+    Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 );
+    if ( Res ) // none or root
+        return;
+    Acb_NtkIncTravId( p ); // root (2)   inner (1)  visited (0)
+    Acb_ObjDeriveTfo_rec( p, Root, vTfo, vRoots );
+    assert( Vec_IntEntryLast(vTfo) == Root );
+    Vec_IntPop( vTfo );
+    assert( Vec_IntEntryLast(vRoots) != Root );
+    Vec_IntReverseOrder( vTfo );
+    Vec_IntReverseOrder( vRoots );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collect side-inputs of the TFO, except the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acb_NtkCollectTfoSideInputs( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfo )
+{
+    Vec_Int_t * vSide  = Vec_IntAlloc( 100 );
+    int i, k, Node, iFanin, * pFanins;
+    Acb_NtkIncTravId( p );
+    Vec_IntForEachEntry( vTfo, Node, i )
+        Acb_ObjSetTravIdCur( p, Node ), assert( Node != Pivot );
+    Vec_IntForEachEntry( vTfo, Node, i )
+        Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k )
+            if ( !Acb_ObjSetTravIdCur(p, iFanin) && iFanin != Pivot )
+                Vec_IntPush( vSide, iFanin );
+    return vSide;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [From side inputs, collect marked nodes and their unmarked fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkCollectNewTfi1_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew )
+{
+    int i, iFanin, * pFanins;
+    if ( !Acb_ObjIsTravIdPrev(p, iObj) )
+        return;
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, i )
+        Acb_NtkCollectNewTfi1_rec( p, iFanin, vTfiNew );
+    Vec_IntPush( vTfiNew, iObj );
+}
+void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew )
+{
+    int i, iFanin, * pFanins;
+    int fTravIdPrev = Acb_ObjIsTravIdPrev(p, iObj);
+    if ( Acb_ObjSetTravIdCur(p, iObj) )
+        return;
+    if ( fTravIdPrev && !Acb_ObjIsCi(p, iObj) )
+        Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, i )
+            Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew );
+    Vec_IntPush( vTfiNew, iObj );
+}
+Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vSide )
+{
+    Vec_Int_t * vTfiNew  = Vec_IntAlloc( 100 );
+    int i, Node;
+    Acb_NtkIncTravId( p );
+    Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew );
+    assert( Vec_IntEntryLast(vTfiNew) == Pivot );
+    Vec_IntPop( vTfiNew );
+    Vec_IntForEachEntry( vSide, Node, i )
+        Acb_NtkCollectNewTfi2_rec( p, Node, vTfiNew );
+    Vec_IntPush( vTfiNew, Pivot );
+    return vTfiNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+{
+    Vec_Int_t * vWin = Vec_IntAlloc( 100 );
+    int i, k, iObj, iFanin, * pFanins;
+    // mark leaves
+    Acb_NtkIncTravId( p );
+    Vec_IntForEachEntry( vTfi, iObj, i )
+        Acb_ObjSetTravIdCur(p, iObj);
+    Acb_NtkIncTravId( p );
+    Vec_IntForEachEntry( vTfi, iObj, i )
+        if ( !Acb_ObjIsCi(p, iObj) )
+            Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+                if ( !Acb_ObjIsTravIdCur(p, iFanin) )
+                    Acb_ObjSetTravIdCur(p, iObj);
+    // add TFI
+    Vec_IntForEachEntry( vTfi, iObj, i )
+        Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) );
+    // mark roots
+    Vec_IntForEachEntry( vRoots, iObj, i )
+        Acb_ObjSetTravIdCur(p, iObj);
+    // add TFO
+    Vec_IntForEachEntry( vTfo, iObj, i )
+        Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) );
+    return vWin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax, Vec_Int_t ** pvDivs )
+{
+    int nTfiLevMin = Acb_ObjLevelD(p, Pivot) - nTfiLevs;
+    int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs;
+    Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi;
+    // collect divisors by traversing limited TFI
+    vDivs = Acb_NtkDivisors( p, Pivot, nTfiLevMin );
+    // mark limited TFO of the divisors
+    Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
+    // collect TFO and roots
+    Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots );
+    // collect side inputs of the TFO
+    vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo );
+    // collect new TFI
+    vTfi = Acb_NtkCollectNewTfi( p, Pivot, vSide );
+    // collect all nodes
+    vWin = Acb_NtkCollectWindow( p, Pivot, vTfi, vTfo, vRoots );
+    // cleanup
+    Vec_IntFree( vTfi );
+    Vec_IntFree( vTfo );
+    Vec_IntFree( vRoots );
+    Vec_IntFree( vSide );
+    *pvDivs = vDivs;
+    return vWin;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int_t * vDivs, int nBTLimit )
+{
+    int i, iObj, nDivsNew;
+    // reload divisors in terms of SAT variables
+    Vec_IntForEachEntry( vDivs, iObj, i )
+        Vec_IntWriteEntry( vDivs, i, Acb_ObjCopy(p, iObj) );
+    // try solving 
+    nDivsNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vDivs), Vec_IntSize(vDivs), nBTLimit );
+    Vec_IntShrink( vDivs, nDivsNew );
+    // reload divisors in terms of network variables
+    Vec_IntForEachEntry( vDivs, iObj, i )
+        Vec_IntWriteEntry( vDivs, i, Vec_IntEntry(vWin, iObj) );
+    return Vec_IntSize(vDivs);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs, int nFanMax )
+{
+    Vec_Int_t * vSupp = &p->vArray0;
+    Vec_Int_t * vDivs, * vWin = Acb_NtkWindow( p, Pivot, nTfiLevs, nTfoLevs, nFanMax, &vDivs );
+    sat_solver * pSat = Acb_NtkWindow2Solver( pSat, p, Pivot, vWin, 0 );
+    int nSuppNew, Level = Acb_ObjLevelD( p, Pivot );
+
+    // try solving the original support
+    Vec_IntClear( vSupp );
+    Vec_IntAppend( vSupp, vDivs );
+    nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
+    Vec_IntShrink( vSupp, nSuppNew );
+
+    // try solving by level
+
+    Acb_NtkUnmarkWindow( p, vWin );
+    Vec_IntFree( vWin );
+    Vec_IntFree( vDivs );
+
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/sat/bmc/bmcFault.c

@@ -1069,7 +1069,7 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
             continue;
         if ( c != '0' && c != '1' )
         {
-            printf( "Wring symbol (%c) in the input file.\n", c );
+            printf( "Wrong symbol (%c) in the input file.\n", c );
             Vec_IntFreeP( &vTests );
             break;
         }