Version abc80802_2

abc.dsp

@@ -2930,10 +2930,6 @@ SOURCE=.\src\aig\aig\aigTable.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\aig\aigTest.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\aig\aigTiming.c
 # End Source File
 # Begin Source File
@@ -3322,6 +3318,10 @@ SOURCE=.\src\aig\dch\dchSim.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\dch\dchSimSat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\dch\dchSweep.c
 # End Source File
 # End Group

src/aig/aig/aigRepr.c

@@ -473,17 +473,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj, * pRepr;
     int i;
-    int nReprs, nEquivs;
-
-extern int           Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
-extern int           Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
-
     assert( p->pReprs != NULL );
     // create equivalent nodes in the manager
     assert( p->pEquivs == NULL );
     p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
     memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
-
     // make the choice nodes
     Aig_ManForEachNode( p, pObj, i )
     {
@@ -513,11 +507,6 @@ extern int           Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
         p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
         p->pEquivs[pRepr->Id] = pObj;
     }
-
-    nReprs = Dch_DeriveChoiceCountReprs( p );
-    nEquivs = Dch_DeriveChoiceCountEquivs( p );
-    printf( "\nReprs = %d. Equivs = %d. Choices = %d.\n", 
-        nReprs, nEquivs, Aig_ManCountChoices(p) );
 }
 
 

src/aig/dar/darScript.c

@@ -416,6 +416,86 @@ PRT( "Choicing time ", clock() - clk );
 //    return NULL;
 }
 
+#include "dch.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+
+    int fVerbose = pPars->fVerbose;
+    int fConstruct = 0;
+    Aig_Man_t * pMan, * pTemp;
+    Vec_Ptr_t * vAigs;
+    int i, clk;
+
+clk = clock();
+//    vAigs = Dar_ManChoiceSynthesisExt();
+    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, fVerbose );
+
+    // swap the first and last network
+    // this should lead to the primary choice being "better" because of synthesis
+    // (it is also important when constructing choices)
+    if ( !fConstruct )
+    {
+        pMan = Vec_PtrPop( vAigs );
+        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+        Vec_PtrWriteEntry( vAigs, 0, pMan );
+    }
+
+if ( fVerbose )
+{
+PRT( "Synthesis time", clock() - clk );
+}
+//    pPars->timeSynth = clock() - clk;
+
+clk = clock();
+/*
+    if ( fConstruct )
+        pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
+    else
+        pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
+*/
+    pMan = Dch_ComputeChoices( vAigs, pPars );
+
+    // reconstruct the network
+    pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
+    Aig_ManStop( pTemp );
+    // duplicate the timing manager
+    pTemp = Vec_PtrEntry( vAigs, 0 );
+    if ( pTemp->pManTime )
+    {
+        extern void * Tim_ManDup( void * p, int fDiscrete );     
+        pMan->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+    }
+    // reset levels
+    Aig_ManChoiceLevel( pMan );
+    pMan->pName = Aig_UtilStrsav( pTemp->pName );
+    pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );
+
+    // cleanup
+    Vec_PtrForEachEntry( vAigs, pTemp, i )
+        Aig_ManStop( pTemp );
+    Vec_PtrFree( vAigs );
+
+if ( fVerbose )
+{
+//PRT( "Choicing time ", clock() - clk );
+}
+    return pMan;
+//    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/dch/dch.h

@@ -45,8 +45,12 @@ struct Dch_Pars_t_
     int              nBTLimit;      // conflict limit at a node
     int              nSatVarMax;    // the max number of SAT variables
     int              fSynthesis;    // set to 1 to perform synthesis
+    int              fPolarFlip;    // uses polarity adjustment
+    int              fSimulateTfo;  // uses simulatin of TFO classes
     int              fVerbose;      // verbose stats
     int              timeSynth;     // synthesis runtime
+    int              nNodesAhead;   // the lookahead in terms of nodes
+    int              nCallsRecycle; // calls to perform before recycling SAT solver
 };
 
 ////////////////////////////////////////////////////////////////////////

src/aig/dch/dchChoice.c

@@ -67,18 +67,27 @@ int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
 ***********************************************************************/
 int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
 {
-    Aig_Obj_t * pObj, * pTemp;
-    int i, nEquivs = 0;
+    Aig_Obj_t * pObj, * pTemp, * pPrev;
+    int i, nEquivs = 0, Counter = 0;
     Aig_ManForEachObj( pAig, pObj, i )
     {
         if ( !Aig_ObjIsChoice(pAig, pObj) )
             continue;
-        for ( pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; pTemp = Aig_ObjEquiv(pAig, pTemp) )
+        for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; 
+              pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
         {
-            assert( pTemp->nRefs == 0 );
+            if ( pTemp->nRefs > 0 )
+            {
+                // remove referenced node from equivalence class
+                assert( pAig->pEquivs[pPrev->Id] == pTemp );
+                pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
+                Counter++;
+            }
             nEquivs++;
         }
     }
+//    if ( Counter )
+//    printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
     return nEquivs;
 }
 
@@ -146,51 +155,6 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the AIG with choices from representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_DeriveChoiceAig_rec( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
-    if ( pObj->pData )
-        return;
-    // construct AIG for the representative
-    if ( (pRepr = Aig_ObjRepr(pAigOld, pObj)) )
-        Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, pRepr );
-    // construct AIG for the fanins
-    Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin0(pObj) );
-    Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin1(pObj) );
-    pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    if ( pRepr == NULL )
-        return;
-    // get the corresponding new nodes
-    pObjNew  = Aig_Regular(pObj->pData);
-    pReprNew = Aig_Regular(pRepr->pData);
-    if ( pObjNew == pReprNew )
-        return;
-    assert( pObjNew->nRefs == 0 );
-    // update new nodes of the object
-    pObj->pData = Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
-    if ( !Aig_ObjIsNode(pRepr) )
-        return;
-    // skip choices with combinational loops
-    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
-//    if ( Aig_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
-        return;
-    // add choice
-    pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
-    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Returns representatives of fanin in approapriate polarity.]
 
   Description []
@@ -237,14 +201,19 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_
     pReprNew = Aig_Regular(pRepr->pData);
     if ( pObjNew == pReprNew )
         return;
-//    assert( pObjNew->nRefs == 0 );
+    // skip the earlier nodes
+    if ( pReprNew->Id > pObjNew->Id )
+        return;
+    assert( pReprNew->Id < pObjNew->Id );
     // set the representatives
     Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+    // skip used nodes
+    if ( pObjNew->nRefs > 0 )
+        return;
+    assert( pObjNew->nRefs == 0 );
     // update new nodes of the object
     if ( !Aig_ObjIsNode(pRepr) )
         return;
-    if ( pObjNew->nRefs > 0 )
-        return;
     // skip choices with combinational loops
     if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
         return;
@@ -278,15 +247,8 @@ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
     Aig_ManForEachPi( pAig, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pChoices );
-    // construct choice nodes from the POs
+    // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
-/*
-    Aig_ManForEachPo( pAig, pObj, i )
-    {
-        Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) );
-        Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) );
-    }
-*/
     Aig_ManForEachNode( pAig, pObj, i )
         Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
     Aig_ManForEachPo( pAig, pObj, i )

src/aig/dch/dchClass.c

@@ -26,7 +26,7 @@
     The first node of the class is its representative node.
     The representative has the smallest topological order among the class nodes.
     The nodes inside each class are ordered according to their topological order.
-    The classes are ordered according to the topological order of their representatives.
+    The classes are ordered according to the topo order of their representatives.
 */
 
 // internal representation of candidate equivalence classes
@@ -207,6 +207,25 @@ int Dch_ClassesLitNum( Dch_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
+{
+    assert( p->pId2Class[pRepr->Id] != NULL );
+    assert( p->pClassSizes[pRepr->Id] > 1 );
+    *pnSize = p->pClassSizes[pRepr->Id];
+    return p->pId2Class[pRepr->Id];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks candidate equivalence classes.]
 
   Description []

src/aig/dch/dchCnf.c

@@ -68,21 +68,45 @@ void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
     pLits[0] = toLitCond(VarI, 1);
     pLits[1] = toLitCond(VarT, 1^fCompT);
     pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
     pLits[0] = toLitCond(VarI, 1);
     pLits[1] = toLitCond(VarT, 0^fCompT);
     pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
     pLits[0] = toLitCond(VarI, 0);
     pLits[1] = toLitCond(VarE, 1^fCompE);
     pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
     pLits[0] = toLitCond(VarI, 0);
     pLits[1] = toLitCond(VarE, 0^fCompE);
     pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
 
@@ -102,11 +126,23 @@ void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
     pLits[0] = toLitCond(VarT, 0^fCompT);
     pLits[1] = toLitCond(VarE, 0^fCompE);
     pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
     pLits[0] = toLitCond(VarT, 1^fCompT);
     pLits[1] = toLitCond(VarE, 1^fCompE);
     pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
     assert( RetValue );
 }
@@ -137,13 +173,28 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     {
         pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
         pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1);
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Aig_Regular(pFanin)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNode->fPhase )                pLits[1] = lit_neg( pLits[1] );
+        }
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
         assert( RetValue );
     }
     // add A & B => C   or   !A + !B + C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
         pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Aig_Regular(pFanin)->fPhase )  pLits[i] = lit_neg( pLits[i] );
+        }
+    }
     pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNode->fPhase )  pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+    }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
     free( pLits );
@@ -213,6 +264,7 @@ void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
     assert( Dch_ObjSatNum(p,pObj) == 0 );
     if ( Aig_ObjIsConst1(pObj) )
         return;
+    Vec_PtrPush( p->vUsedNodes, pObj );
     Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
     if ( Aig_ObjIsNode(pObj) )
         Vec_PtrPush( vFrontier, pObj );

src/aig/dch/dchCore.c

@@ -42,11 +42,15 @@
 void Dch_ManSetDefaultParams( Dch_Pars_t * p )
 {
     memset( p, 0, sizeof(Dch_Pars_t) );
-    p->nWords     =     4;    // the number of simulation words
-    p->nBTLimit   =   100;    // conflict limit at a node
-    p->nSatVarMax = 10000;    // the max number of SAT variables
+    p->nWords         =     8;  // the number of simulation words
+    p->nBTLimit       =  1000;  // conflict limit at a node
+    p->nSatVarMax     =  5000;  // the max number of SAT variables
     p->fSynthesis     =     1;  // derives three snapshots
-    p->fVerbose   =     1;    // verbose stats
+    p->fPolarFlip     =     1;  // uses polarity adjustment
+    p->fSimulateTfo   =     1;  // simulate TFO
+    p->fVerbose       =     0;  // verbose stats
+    p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
+    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
 }
 
 /**Function*************************************************************
@@ -66,6 +70,8 @@ Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
     Aig_Man_t * pResult;
     int clk, clkTotal = clock();
     assert( Vec_PtrSize(vAigs) > 0 );
+    // reset random numbers
+    Aig_ManRandom(1);
     // start the choicing manager
     p = Dch_ManCreate( vAigs, pPars );
     // compute candidate equivalence classes

src/aig/dch/dchInt.h

@@ -63,8 +63,10 @@ struct Dch_Man_t_
     int *            pSatVars;       // mapping of each node into its SAT var
     Vec_Ptr_t *      vUsedNodes;     // nodes whose SAT vars are assigned
     int              nRecycles;      // the number of times SAT solver was recycled
+    int              nCallsSince;    // the number of calls since the last recycle
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
-    Vec_Ptr_t *      vRoots;         // the roots of the current equiv class
+    Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
+    Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
     // solver cone size
     int              nConeThis;
     int              nConeMax;
@@ -95,6 +97,12 @@ struct Dch_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int  Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
+static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
+
+static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj )                       { return pObj->pData;  }
+static inline void        Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
+
 static inline int  Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
 {
     return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
@@ -105,9 +113,6 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
     Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
 }
 
-static inline int  Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
-static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
-
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -126,6 +131,7 @@ extern void          Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
                          int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
 extern void          Dch_ClassesStop( Dch_Cla_t * p );
 extern int           Dch_ClassesLitNum( Dch_Cla_t * p );
+extern Aig_Obj_t **  Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
 extern void          Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
 extern void          Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
 extern int           Dch_ClassesRefine( Dch_Cla_t * p );
@@ -143,7 +149,10 @@ extern void          Dch_ManSatSolverRecycle( Dch_Man_t * p );
 extern int           Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
 /*=== dchSim.c ===================================================*/
 extern Dch_Cla_t *   Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
-/*=== dchSim.c ===================================================*/
+/*=== dchSimSat.c ===================================================*/
+extern void          Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+extern void          Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+/*=== dchSweep.c ===================================================*/
 extern void          Dch_ManSweep( Dch_Man_t * p );
 
 #ifdef __cplusplus

src/aig/dch/dchMan.c

@@ -48,12 +48,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
     p->pPars        = pPars;
     p->vAigs        = vAigs;
     p->pAigTotal    = Dch_DeriveTotalAig( vAigs );
+    Aig_ManFanoutStart( p->pAigTotal );
     // SAT solving
     p->nSatVars     = 1;
     p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
     p->vUsedNodes   = Vec_PtrAlloc( 1000 );
     p->vFanins      = Vec_PtrAlloc( 100 );
-    p->vRoots     = Vec_PtrAlloc( 1000 );
+    p->vSimRoots    = Vec_PtrAlloc( 1000 );
+    p->vSimClasses  = Vec_PtrAlloc( 1000 );
     // equivalences proved
     p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
     return p;
@@ -73,10 +75,7 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
 void Dch_ManPrintStats( Dch_Man_t * p )
 {
 //    Aig_Man_t * pAig;
-    int i;
-    for ( i = 0; i < 85; i++ )
-        printf( " " );
-    printf( "\r" );
+//    int i;
 //    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
 //    Vec_PtrForEachEntry( p->vAigs, pAig, i )
 //        Aig_ManPrintStats( pAig );
@@ -94,7 +93,7 @@ void Dch_ManPrintStats( Dch_Man_t * p )
         p->nSatCallsSat, p->nSatFailsReal );
     printf( "Choices   : Lits = %6d. Reprs = %5d. Equivs = %5d. Choices = %5d.\n", 
         p->nLits, p->nReprs, p->nEquivs, p->nChoices );
-    printf( "Runtime statistics:\n" );
+    printf( "Choicing runtime statistics:\n" );
     p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice;
     PRTP( "Sim init   ", p->timeSimInit,  p->timeTotal );
     PRTP( "Sim SAT    ", p->timeSimSat,   p->timeTotal );
@@ -105,7 +104,10 @@ void Dch_ManPrintStats( Dch_Man_t * p )
     PRTP( "Choice     ", p->timeChoice,   p->timeTotal );
     PRTP( "Other      ", p->timeOther,    p->timeTotal );
     PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+    if ( p->pPars->timeSynth )
+    {
     PRT( "Synthesis  ", p->pPars->timeSynth );
+    }
 }
 
 /**Function*************************************************************
@@ -133,7 +135,8 @@ void Dch_ManStop( Dch_Man_t * p )
         sat_solver_delete( p->pSat );
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vFanins );
-    Vec_PtrFree( p->vRoots );
+    Vec_PtrFree( p->vSimRoots );
+    Vec_PtrFree( p->vSimClasses );
     FREE( p->pReprsProved );
     FREE( p->pSatVars );
     free( p );
@@ -155,16 +158,24 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
     int Lit;
     if ( p->pSat )
     {
+        Aig_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+            Dch_ObjSetSatNum( p, pObj, 0 );
+        Vec_PtrClear( p->vUsedNodes );
+//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
         sat_solver_delete( p->pSat );
-        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
     }
     p->pSat = sat_solver_new();
     sat_solver_setnvars( p->pSat, 1000 );
     // var 0 is reserved for const1 node - add the clause
     Lit = toLit( 0 );
+    if ( p->pPars->fPolarFlip )
+        Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
     p->nSatVars = 1;
     p->nRecycles++;
+    p->nCallsSince = 0;
 }
 
 

src/aig/dch/dchSat.c

@@ -51,7 +51,10 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     assert( pNew != pOld );
     
     // check if SAT solver needs recycling
-    if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax) )
+    if ( p->pSat == NULL || 
+        (p->pPars->nSatVarMax && 
+         p->nSatVars > p->pPars->nSatVarMax && 
+         ++p->nCallsSince > p->pPars->nCallsRecycle) )
         Dch_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
@@ -70,6 +73,11 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     // A = 1; B = 0     OR     A = 1; B = 1 
     pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
     pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
@@ -108,6 +116,11 @@ p->timeSatUndec += clock() - clk;
     // A = 0; B = 1     OR     A = 0; B = 0 
     pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
     pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );

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;
 }
 

src/aig/dch/dchSimSat.c

+/**CFile****************************************************************
+
+  FileName    [dchSimSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Performs resimulation using counter-examples.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the reverse DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanout, * pRepr;
+    int iFanout = -1, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    // traverse the fanouts
+    Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
+        Dch_ManCollectTfoCands_rec( p, pFanout );
+    // check if the given node has a representative
+    pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
+    if ( pRepr == NULL )
+        return;
+    // pRepr is the constant 1 node
+    if ( pRepr == Aig_ManConst1(p->pAigTotal) )
+    {
+        Vec_PtrPush( p->vSimRoots, pObj );
+        return;
+    }
+    // pRepr is the representative of the equivalence class
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
+    Vec_PtrPush( p->vSimClasses, pRepr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect equivalence classes and const1 cands in the TFO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+    Vec_PtrClear( p->vSimRoots );
+    Vec_PtrClear( p->vSimClasses );
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );    
+    Dch_ManCollectTfoCands_rec( p, pObj1 );
+    Dch_ManCollectTfoCands_rec( p, pObj2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the solved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj );
+        int nVarNum = Dch_ObjSatNum( p, pObjFraig );
+        // get the value from the SAT solver
+        // (account for the fact that some vars may be minimized away)
+        pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+        return;
+    }
+    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+    // count the cone size
+    if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
+        p->nConeThis++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the other nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        // set random value
+        pObj->fMarkB = Aig_ManRandom(0) & 1;
+        return;
+    }
+    Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pRoot, ** ppClass;
+    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    // get the equivalence classes
+    Dch_ManCollectTfoCands( p, pObj, pRepr );
+    // resimulate the cone of influence of the solved nodes
+    p->nConeThis = 0;
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+    Dch_ManResimulateSolved_rec( p, pObj );
+    Dch_ManResimulateSolved_rec( p, pRepr );
+    p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+    // resimulate the cone of influence of the other nodes
+    Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
+        Dch_ManResimulateOther_rec( p, pRoot );
+    // refine these nodes
+    RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+    // resimulate the cone of influence of the cand classes
+    RetValue2 = 0;
+    Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
+    {
+        ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
+        for ( k = 0; k < nSize; k++ )
+            Dch_ManResimulateOther_rec( p, ppClass[k] );
+        // refine this class
+        RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
+    }
+    // make sure refinement happened
+    if ( Aig_ObjIsConst1(pRepr) )
+        assert( RetValue1 );
+    else
+        assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pRoot;
+    int i, RetValue, clk = clock();
+    // get the equivalence class
+    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
+    else
+        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
+    // resimulate the cone of influence of the solved nodes
+    p->nConeThis = 0;
+    Aig_ManIncrementTravId( p->pAigTotal );
+    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+    Dch_ManResimulateSolved_rec( p, pObj );
+    Dch_ManResimulateSolved_rec( p, pRepr );
+    p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+    // resimulate the cone of influence of the other nodes
+    Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
+        Dch_ManResimulateOther_rec( p, pRoot );
+    // refine this class
+    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+    else
+        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
+    assert( RetValue );
+p->timeSimSat += clock() - clk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dch/dchSweep.c

 /**CFile****************************************************************
 
-  FileName    [dchSat.c]
+  FileName    [dchSweep.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Choice computation for tech-mapping.]
 
-  Synopsis    [Calls to the SAT solver.]
+  Synopsis    [One round of SAT sweeping.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 29, 2008.]
 
-  Revision    [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+  Revision    [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -25,9 +25,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj )                       { return pObj->pData;  }
-static inline void        Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
 static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
 
@@ -37,137 +34,6 @@ static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_Is
 
 /**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    [Resimulates the cone of influence of the solved nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
-    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        // get the value from the SAT solver
-        assert( p->pSatVars[pObj->Id] > 0 );
-        pObj->fMarkB = sat_solver_var_value( p->pSat, p->pSatVars[pObj->Id] );
-        return;
-    }
-    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
-    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
-    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
-                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-    // count the cone size
-    if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
-        p->nConeThis++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the cone of influence of the other nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
-{
-    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        // set random value
-        pObj->fMarkB = Aig_ManRandom(0) & 1;
-        return;
-    }
-    Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
-    Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
-    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
-                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Handle the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_ManSweepResimulate( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
-    Aig_Obj_t * pRoot;
-    int i, RetValue, clk = clock();
-    // get the equivalence class
-    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
-        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vRoots );
-    else
-        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vRoots );
-    // resimulate the cone of influence of the solved nodes
-    p->nConeThis = 0;
-    Aig_ManIncrementTravId( p->pAigTotal );
-    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
-    Dch_ManResimulateSolved_rec( p, pObj );
-    Dch_ManResimulateSolved_rec( p, pRepr );
-    p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
-    // resimulate the cone of influence of the other nodes
-    Vec_PtrForEachEntry( p->vRoots, pRoot, i )
-        Dch_ManResimulateOther_rec( p, pRoot );
-    // refine this class
-    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
-        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vRoots, 0 );
-    else
-        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
-    assert( RetValue );
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -187,8 +53,12 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
         return;
     // get the fraiged node
     pObjFraig = Dch_ObjFraig( pObj );
+    if ( pObjFraig == NULL )
+        return;
     // get the fraiged representative
     pObjReprFraig = Dch_ObjFraig( pObjRepr );
+    if ( pObjReprFraig == NULL )
+        return;
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
     {
@@ -199,7 +69,10 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
     assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
     RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
     if ( RetValue == -1 ) // timed out
+    {
+        Dch_ObjSetFraig( pObj, NULL );
         return;
+    }
     if ( RetValue == 1 )  // proved equivalent
     {
         pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
@@ -209,7 +82,10 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
         return;
     }
     // disproved the equivalence
-    Dch_ManSweepResimulate( p, pObj, pObjRepr );
+    if ( p->pPars->fSimulateTfo )
+        Dch_ManResimulateCex( p, pObj, pObjRepr );
+    else
+        Dch_ManResimulateCex2( p, pObj, pObjRepr );
 }
 
 /**Function*************************************************************
@@ -234,19 +110,21 @@ void Dch_ManSweep( Dch_Man_t * p )
     Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
     Aig_ManForEachPi( p->pAigTotal, pObj, i )
         pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
-    // prepare class refinement procedures
-    Dch_ClassesSetData( p->ppClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
     // sweep internal nodes
     pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
     Aig_ManForEachNode( p->pAigTotal, pObj, i )
     {
         Bar_ProgressUpdate( pProgress, i, NULL );
+        if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL || 
+             Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
+            continue;
         pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
         if ( pObjNew == NULL )
             continue;
         Dch_ObjSetFraig( pObj, pObjNew );
         Dch_ManSweepNode( p, pObj );
     }
+    Bar_ProgressStop( pProgress );
     // update the representatives of the nodes (makes classes invalid)
     FREE( p->pAigTotal->pReprs );
     p->pAigTotal->pReprs = p->pReprsProved;

src/aig/dch/module.make

@@ -6,4 +6,5 @@ SRC +=    src/aig/dch/dchAig.c \
     src/aig/dch/dchMan.c \
     src/aig/dch/dchSat.c \
     src/aig/dch/dchSim.c \
+    src/aig/dch/dchSimSat.c \
     src/aig/dch/dchSweep.c

src/aig/ntl/ntlCore.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntl.h"
+#include "dch.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -39,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
+Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
     extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
@@ -58,6 +59,23 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate
 
 /**Function*************************************************************
 
+  Synopsis    [Extracts AIG from the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManPerformChoicingNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+    return Dar_ManChoiceNew( pAig, pPars );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Testing procedure for insertion of mapping into the netlist.]
 
   Description []

src/base/abci/abc.c

@@ -229,6 +229,7 @@ static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Pfan       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Dch        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DC2        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Bidec      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Strash     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -488,6 +489,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*pfan",         Abc_CommandAbc8Pfan,         0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*dch",          Abc_CommandAbc8Dch,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dc2",          Abc_CommandAbc8DC2,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*bidec",        Abc_CommandAbc8Bidec,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*st",           Abc_CommandAbc8Strash,       0 );
@@ -7703,7 +7705,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
     extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
     extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
-    extern void Aig_ProcedureTest();
+//    extern void Aig_ProcedureTest();
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -7910,7 +7912,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pFileName = argv[globalUtilOptind];
     Nwk_ManLutMergeGraphTest( pFileName );
 */
-    Aig_ProcedureTest();
+//    Aig_ProcedureTest();
 
     return 0;
 usage:
@@ -8929,7 +8931,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blcvh]\n" );
-    fprintf( pErr, "\t         performs partitioned choicing using a new AIG package\n" );
+    fprintf( pErr, "\t         performs partitioned choicing using new AIG package\n" );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
     fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
@@ -8967,7 +8969,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9007,6 +9009,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fSynthesis ^= 1;
             break;
+        case 'p':
+            pPars->fPolarFlip ^= 1;
+            break;
+        case 't':
+            pPars->fSimulateTfo ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -9037,12 +9045,14 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dch [-WCS num] [-svh]\n" );
-    fprintf( pErr, "\t         performs computation of structural choices\n" );
+    fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" );
+    fprintf( pErr, "\t         computes structural choices using a new approach\n" );
     fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
     fprintf( pErr, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+    fprintf( pErr, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -17155,7 +17165,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_Man_t * pAigNew;
     int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
     int nConfMax, nLevelMax;
-    extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
+    extern Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
     // set defaults
     fBalance     = 1;
@@ -17216,7 +17226,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
+    pAigNew = Ntl_ManPerformChoicing( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     if ( pAigNew == NULL )
     {
         printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
@@ -17250,6 +17260,113 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Dch_Pars_t Pars, * pPars = &Pars;
+    Aig_Man_t * pAigNew;
+    int c;
+    extern Aig_Man_t * Ntl_ManPerformChoicingNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+
+    // set defaults
+    Dch_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            pPars->fSynthesis ^= 1;
+            break;
+        case 'p':
+            pPars->fPolarFlip ^= 1;
+            break;
+        case 't':
+            pPars->fSimulateTfo ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Dch(): There is no AIG to synthesize.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    pAigNew = Ntl_ManPerformChoicingNew( pAbc->pAbc8Aig, pPars );
+    if ( pAigNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" );
+        return 1;
+    }
+    Aig_ManStop( pAbc->pAbc8Aig );
+    pAbc->pAbc8Aig = pAigNew;
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" );
+    fprintf( stdout, "\t         computes structural choices using a new approach\n" );
+    fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
+    fprintf( stdout, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
+    fprintf( stdout, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+    fprintf( stdout, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAigNew;