Handling special case in 'fold' when the network is combinational.

2 files changed, 24 insertions, 15 deletions

diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 1d842b3c..7213bdff 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -944,7 +944,6 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
     Aig_Man_t * pAigNew;
     Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
     int i;
-    assert( Saig_ManRegNum(pAig) > 0 );
     if ( Aig_ManConstrNum(pAig) == 0 )
         return Aig_ManDupDfs( pAig );
     assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
@@ -969,9 +968,15 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
             continue;
         pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
     }
+
     // create additional flop
-    pFlopOut = Aig_ObjCreateCi( pAigNew );
-    pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
+    if ( Saig_ManRegNum(pAig) > 0 )
+    {
+        pFlopOut = Aig_ObjCreateCi( pAigNew );
+        pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
+    }
+    else 
+        pFlopIn = pMiter;
 
     // create primary output
     Saig_ManForEachPo( pAig, pObj, i )
@@ -985,10 +990,15 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
     // transfer to register outputs
     Saig_ManForEachLi( pAig, pObj, i )
         Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
+
     // create additional flop 
-    Aig_ObjCreateCo( pAigNew, pFlopIn );
+    if ( Saig_ManRegNum(pAig) > 0 )
+    {
+        Aig_ObjCreateCo( pAigNew, pFlopIn );
+        Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
+    }
 
-    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
+    // perform cleanup
     Aig_ManCleanup( pAigNew );
     Aig_ManSeqCleanup( pAigNew );
     return pAigNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 79f92b08..3a6c8b1b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21967,11 +21967,6 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsComb(pNtk) )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
@@ -22007,6 +22002,8 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     // consider the case of manual constraint definition
     if ( nConstrs > 0 )
     {
+        if ( Abc_NtkIsComb(pNtk) )
+            Abc_Print( -1, "The network is combinational.\n" );
         if ( Abc_NtkConstrNum(pNtk) > 0 )
         {
             Abc_Print( -1, "The network already has constraints.\n" );
@@ -22021,6 +22018,11 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtk->nConstrs = nConstrs;
         return 0;
     }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
     // detect constraints using functional/structural methods
     Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
     return 0;
@@ -22217,11 +22219,6 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsComb(pNtk) )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
@@ -22232,6 +22229,8 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network has no constraints.\n" );
         return 0;
     }
+    if ( Abc_NtkIsComb(pNtk) )
+        Abc_Print( 0, "The network is combinational.\n" );
     // modify the current network
     pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose );
     if ( pNtkRes == NULL )