Trying to explicitly compute don't-cares during optimization.

4 files changed, 171 insertions, 12 deletions

diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 1aa8b7d0..f9c95c83 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -66,6 +66,7 @@ struct Sfm_Par_t_
     int             fUseAndOr;     // enable internal detection of AND/OR gates
     int             fZeroCost;     // enable zero-cost replacement
     int             fUseSim;       // enable simulation
+    int             fUseDcs;       // enable deriving don't-cares
     int             fPrintDecs;    // enable printing decompositions
     int             fAllBoxes;     // enable preserving all boxes
     int             fLibVerbose;   // enable library stats
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 27d584b4..fe69d480 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sfmInt.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -79,6 +80,8 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
     printf( "Attempts :   " );
     printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
     printf( "Resub  %6d out of %6d (%6.2f %%)   ", p->nResubs,  p->nTryResubs,  100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs)  );
+    if ( p->pPars->fUseDcs )
+    printf( "Improves %6d out of %6d (%6.2f %%)   ", p->nImproves,p->nTryImproves,100.0*p->nImproves/Abc_MaxInt(1, p->nTryImproves));
     printf( "\n" );
 
     printf( "Reduction:   " );
@@ -213,7 +216,70 @@ finish:
     // update the network
     Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
     return 1;
- }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_NodeResubOne( Sfm_Ntk_t * p, int iNode )
+{
+    int fSkipUpdate  = 0;
+    int fVeryVerbose = 0;//p->pPars->fVeryVerbose;
+    int i, iFanin;
+    word uTruth;
+    abctime clk;
+    assert( Sfm_ObjIsNode(p, iNode) );
+    p->nTryImproves++;
+    // report init stats
+    if ( p->pPars->fVeryVerbose )
+        printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanins = %d.  MFFC = %d\n", 
+            iNode, Sfm_ObjLevel(p, iNode), 0, Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), 
+            Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, iNode) );
+    // collect fanins
+    Vec_IntClear( p->vDivIds );
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
+clk = Abc_Clock();
+    uTruth = Sfm_ComputeInterpolant2( p );
+p->timeSat += Abc_Clock() - clk;
+    // analyze outcomes
+    if ( uTruth == SFM_SAT_UNDEC )
+    {
+        p->nTimeOuts++;
+        return 0;
+    }
+    assert( uTruth != SFM_SAT_SAT );
+    if ( uTruth == Vec_WrdEntry(p->vTruths, iNode) )
+        return 0;
+    else
+    {
+        word uTruth0  =  Vec_WrdEntry(p->vTruths, iNode);
+        //word uTruth0N = ~uTruth0;
+        //word uTruthN  = ~uTruth;
+        int Old  = Kit_TruthLitNum((unsigned*)&uTruth0,  Sfm_ObjFaninNum(p, iNode), p->vCover);
+        //int OldN = Kit_TruthLitNum((unsigned*)&uTruth0N, Sfm_ObjFaninNum(p, iNode), p->vCover);
+        int New  = Kit_TruthLitNum((unsigned*)&uTruth,   Sfm_ObjFaninNum(p, iNode), p->vCover);
+        //int NewN = Kit_TruthLitNum((unsigned*)&uTruthN,  Sfm_ObjFaninNum(p, iNode), p->vCover);
+        //if ( Abc_MinInt(New, NewN) > Abc_MinInt(Old, OldN) )
+        if ( New > Old )
+            return 0;
+    }
+    p->nImproves++;
+    if ( fSkipUpdate )
+        return 0;
+    // update truth table
+    Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
+    Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+    return 1;
+}
 int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
@@ -230,15 +296,18 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
             if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) )
                 return 1;
         }
-    if ( p->pPars->fArea )
-        return 0;
     // try removing redundant edges
+    if ( !p->pPars->fArea )
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) )
         {
             if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) )
                 return 1;
         }
+    // try simplifying local functions
+    if ( p->pPars->fUseDcs )
+        if ( Sfm_NodeResubOne( p, iNode ) )
+            return 1;
 /*
     // try replacing area critical fanins while adding two new fanins
     if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax )
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 80edd54d..08edf353 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -107,8 +107,10 @@ struct Sfm_Ntk_t_
     sat_solver *      pSat;        // SAT solver
     int               nSatVars;    // the number of variables
     int               nTryRemoves; // number of fanin removals
+    int               nTryImproves;// number of node improvements
     int               nTryResubs;  // number of resubstitutions
     int               nRemoves;    // number of fanin removals
+    int               nImproves;   // number of node improvements
     int               nResubs;     // number of resubstitutions
     // counter-examples
     int               nCexes;      // number of CEXes
@@ -218,6 +220,7 @@ extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNe
 /*=== sfmSat.c ==========================================================*/
 extern int          Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
 extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
+extern word         Sfm_ComputeInterpolant2( Sfm_Ntk_t * p );
 /*=== sfmTim.c ==========================================================*/
 extern Sfm_Tim_t *  Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit );
 extern void         Sfm_TimStop( Sfm_Tim_t * p );
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 6ccdd903..ed38e681 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sfmInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,15 +28,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static word s_Truths6[6] = {
-    ABC_CONST(0xAAAAAAAAAAAAAAAA),
-    ABC_CONST(0xCCCCCCCCCCCCCCCC),
-    ABC_CONST(0xF0F0F0F0F0F0F0F0),
-    ABC_CONST(0xFF00FF00FF00FF00),
-    ABC_CONST(0xFFFF0000FFFF0000),
-    ABC_CONST(0xFFFFFFFF00000000)
-};
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -228,6 +220,100 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Takes SAT solver and returns interpolant.]
+
+  Description [If interpolant does not exist, records difference variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_ComputeInterpolantInt( Sfm_Ntk_t * p, word Truth[2] )
+{
+    int fOnSet, iMint, iVar, nVars = sat_solver_nvars( p->pSat );
+    int iVarPivot = Sfm_ObjSatVar( p, p->iPivotNode );
+    int status, iNewLit, i, Div, nIter = 0;
+    Truth[0] = Truth[1] = 0;
+    sat_solver_setnvars( p->pSat, nVars + 1 );
+    iNewLit = Abc_Var2Lit( nVars, 0 ); // iNewLit
+    assert( Vec_IntSize(p->vDivIds) <= 6 );
+    Vec_IntFill( p->vValues, (1 << Vec_IntSize(p->vDivIds)) * Vec_IntSize(p->vDivVars), -1 );
+    while ( 1 ) 
+    {
+        // find care minterm
+        p->nSatCalls++; nIter++;
+        status = sat_solver_solve( p->pSat, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return l_Undef;
+        if ( status == l_False )
+            return l_False;
+        assert( status == l_True );
+        // collect values
+        iMint = 0;
+        fOnSet = sat_solver_var_value(p->pSat, iVarPivot);
+        Vec_IntClear( p->vLits );
+        Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) ); // NOT(iNewLit)
+        Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, iVarPivot)) );
+        Vec_IntForEachEntry( p->vDivIds, Div, i )
+        {
+            Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, Div)) );
+            if ( sat_solver_var_value(p->pSat, Div) )
+                iMint |= 1 << i;
+        }
+        if ( Truth[!fOnSet] & ((word)1 << iMint) )
+            break; 
+        assert( !(Truth[fOnSet] & ((word)1 << iMint)) );
+        Truth[fOnSet] |= ((word)1 << iMint);
+        // remember variable values
+        Vec_IntForEachEntry( p->vDivVars, iVar, i )
+            Vec_IntWriteEntry( p->vValues, iMint * Vec_IntSize(p->vDivVars) + i, sat_solver_var_value(p->pSat, iVar) );
+        status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
+        if ( status == 0 )
+            return l_False;
+    }
+    assert( status == l_True );
+    // store the counter-example
+    assert( iMint < (1 << Vec_IntSize(p->vDivIds)) );
+    Vec_IntForEachEntry( p->vDivVars, iVar, i )
+    {
+        int Value = Vec_IntEntry(p->vValues, iMint * Vec_IntSize(p->vDivVars) + i);
+        assert( Value != -1 );
+        if ( Value ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
+        {
+            word * pSign = Vec_WrdEntryP( p->vDivCexes, i );
+            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
+            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
+        }
+    }
+    p->nCexes++;
+    return l_True;
+}
+word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p )
+{
+    word Res, ResP, ResN, Truth[2];
+    int nCubesP = 0, nCubesN = 0;
+    int RetValue = Sfm_ComputeInterpolantInt( p, Truth );
+    if ( RetValue == l_Undef )
+        return SFM_SAT_UNDEC;
+    if ( RetValue == l_True )
+        return SFM_SAT_SAT;
+    assert( RetValue == l_False );
+    //printf( "Offset = %2d.  Onset = %2d.  DC = %2d.  Total = %2d.\n", 
+    //    Abc_TtCountOnes(Truth[0]), Abc_TtCountOnes(Truth[1]), 
+    //    (1<<Vec_IntSize(p->vDivIds)) - (Abc_TtCountOnes(Truth[0]) + Abc_TtCountOnes(Truth[1])), 
+    //     1<<Vec_IntSize(p->vDivIds) );
+    Truth[0] = Abc_Tt6Stretch( Truth[0], Vec_IntSize(p->vDivIds) );
+    Truth[1] = Abc_Tt6Stretch( Truth[1], Vec_IntSize(p->vDivIds) );
+    ResP = Abc_Tt6Isop( Truth[1], ~Truth[0], Vec_IntSize(p->vDivIds), &nCubesP );
+    ResN = Abc_Tt6Isop( Truth[0], ~Truth[1], Vec_IntSize(p->vDivIds), &nCubesN );
+    Res  = nCubesP <= nCubesN ? ResP : ~ResN;
+    //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) );            
+    return Res;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks resubstitution.]
 
   Description []