Version abc70831

3 files changed, 21 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3902830d..f740ee18 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5160,7 +5160,7 @@ usage:
   Description []
                
   SideEffects []
-
+ 
   SeeAlso     []
 
 ***********************************************************************/
@@ -11278,6 +11278,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for structrally hashed networks.\n" );
         return 1;
     }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
     // modify the current network
     pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
     if ( pNtkRes == NULL )
@@ -11367,6 +11372,11 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
         return 1;
     }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
 
     if ( Abc_NtkIsStrash(pNtk) )
         Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
@@ -11457,7 +11467,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks.\n" );
         return 1;
     }
-
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
     Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
     return 0;
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 40a52ce8..f8f7d20e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -834,8 +834,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     // conver to the manager
     pMan = Abc_NtkToDar( pNtk, 0 );
     // derive CNF
-//    pCnf = Cnf_Derive( pMan, 0 );
-    pCnf = Cnf_DeriveSimple( pMan, 0 );
+    pCnf = Cnf_Derive( pMan, 0 );
+//    pCnf = Cnf_DeriveSimple( pMan, 0 );
     // convert into the SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index f0989b23..23e9d28d 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -366,7 +366,7 @@ timeFind += clock() - clk2;
             Vec_PtrPush( vPartsAll, vPart );
             Vec_PtrPush( vPartSuppsAll, vPartSupp );
 
-            Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) );
+            Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkCiNum(pNtk)) );
         }
         else
         {
@@ -380,7 +380,7 @@ timeFind += clock() - clk2;
             // reinsert new support
             Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
 
-            Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) );
+            Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkCiNum(pNtk) );
         }
     }
 
@@ -801,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );