Procedures for sorting fanins of the nodes.

abclib.dsp

@@ -115,6 +115,10 @@ SOURCE=.\src\base\abc\abcFanio.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcFanOrder.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcFunc.c
 # End Source File
 # Begin Source File
@@ -4199,6 +4203,26 @@ SOURCE=.\src\proof\int\intUtil.c
 # PROP Default_Filter ""
 # Begin Source File
 
+SOURCE=.\src\proof\live\arenaViolation.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\live\combination.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\live\disjunctiveMonotone.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\live\kLiveConstraints.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\live\kliveness.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\live\liveness.c
 # End Source File
 # Begin Source File
@@ -4209,6 +4233,10 @@ SOURCE=.\src\proof\live\liveness_sim.c
 
 SOURCE=.\src\proof\live\ltl_parser.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\live\monotone.c
+# End Source File
 # End Group
 # Begin Group "llb"
 

src/base/abc/abcUtil.c

@@ -2684,53 +2684,6 @@ int Abc_NtkIsTopo( Abc_Ntk_t * pNtk )
     return (int)(Counter == 0);
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Reroders fanins of the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vOrder;
-    Abc_Obj_t * pNode;
-    char * pSop, * pSopNew;
-    char * pCube, * pCubeNew;
-    int nVars, i, v, * pOrder;
-    assert( Abc_NtkIsSopLogic(pNtk) );
-    vOrder = Vec_IntAlloc( 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        pSop = (char *)pNode->pData;
-        nVars = Abc_SopGetVarNum(pSop);
-        assert( nVars == Abc_ObjFaninNum(pNode) );
-        Vec_IntClear( vOrder );
-        for ( v = 0; v < nVars; v++ )
-            Vec_IntPush( vOrder, v );
-        pOrder = Vec_IntArray(vOrder);
-        Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins );
-        pSopNew = pCubeNew = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars );
-        Abc_SopForEachCube( pSop, nVars, pCube )
-        {
-            for ( v = 0; v < nVars; v++ )
-                if ( pCube[pOrder[v]] == '0' )
-                    pCubeNew[v] = '0';
-                else if ( pCube[pOrder[v]] == '1' )
-                    pCubeNew[v] = '1';
-            pCubeNew += nVars + 3;
-        }
-        pNode->pData = pSopNew;
-        Vec_IntSort( &pNode->vFanins, 0 );
-//        Vec_IntPrint( vOrder );
-    }
-    Vec_IntFree( vOrder );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/module.make

@@ -3,6 +3,7 @@ SRC +=    src/base/abc/abcAig.c \
     src/base/abc/abcCheck.c \
     src/base/abc/abcDfs.c \
     src/base/abc/abcFanio.c \
+    src/base/abc/abcFanOrder.c \
     src/base/abc/abcFunc.c \
     src/base/abc/abcHie.c \
     src/base/abc/abcHieCec.c \

src/base/abci/abc.c

@@ -7091,14 +7091,18 @@ usage:
 int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int fReorder = 1;
     int c;
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'r':
+            fReorder ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -7128,8 +7132,9 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bdd [-h]\n" );
+    Abc_Print( -2, "usage: bdd [-rh]\n" );
     Abc_Print( -2, "\t         converts node functions to BDD\n" );
+    Abc_Print( -2, "\t-r     : toggles enabling dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -9609,19 +9614,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Aig_ManStop( pAig );
     }
 */
-
+/*
     if ( !Abc_NtkIsTopo(pNtk) )
     {
         Abc_Print( -1, "Current network is not in a topological order.\n" );
         return 1;
     }
-
+*/
     if ( pNtk )
-    {
+    { 
         extern void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose );
-        Abc_NtkTestTim( pNtk, fVerbose );
+        Abc_NtkTestTim( pNtk, fVerbose ); 
     }
-
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );