New assertions and bug fix in DSD balancing.

9 files changed, 90 insertions, 16 deletions

diff --git a/src/map/if/ifDelay.c b/src/map/if/ifDelay.c
index 5afb77eb..cb25e767 100644
--- a/src/map/if/ifDelay.c
+++ b/src/map/if/ifDelay.c
@@ -204,9 +204,9 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits,
         {
             Literal = 3 & (Entry >> (k << 1));
             if ( Literal == 1 ) // neg literal
-                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_LitNot(pFaninLits[k]), vAig, nSuppAll, 0, 0 );
+                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? Abc_LitNot(pFaninLits[k]) : -1, vAig, nSuppAll, 0, 0 );
             else if ( Literal == 2 ) // pos literal
-                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], pFaninLits[k], vAig, nSuppAll, 0, 0 );
+                nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? pFaninLits[k] : -1, vAig, nSuppAll, 0, 0 );
             else if ( Literal != 0 ) 
                 assert( 0 );
         }
@@ -216,7 +216,7 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits,
             iRes = If_LogCreateAndXorMulti( vAig, pFaninLitsAnd, nCounterAnd, nSuppAll, 0 );
         else
             *pArea += nLits == 1 ? 0 : nLits - 1;
-        Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, Abc_LitNot(iRes), vAig, nSuppAll, 0, 0 );
+        Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, vAig ? Abc_LitNot(iRes) : -1, vAig, nSuppAll, 0, 0 );
     }
     assert( nCounterOr > 0 );
     if ( vAig )
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index d97cd9be..9b09ce95 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -2211,7 +2211,7 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
     {
         int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] );
-        if ( vAig )
+        if ( vAig ) 
             *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) );
         (*pnSupp)++;
         return pTimes[iCutVar];
@@ -2224,7 +2224,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
             Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
             if ( Delays[i] == -1 )
                 return -1;
-            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
+            if ( vAig ) 
+                pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
         }
         if ( vAig )
             *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll );
@@ -2243,7 +2244,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
             Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
             if ( Delays[i] == -1 )
                 return -1;
-            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
+            if ( vAig ) 
+                pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
         }
         return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea );
     }
@@ -2258,8 +2260,9 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup
             Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits );
             if ( Delay == -1 )
                 return -1;
-            pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
-            Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, pFaninLits[i], vAig, nSuppAll, fXor, fXorFunc );
+            if ( vAig ) 
+                pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) );
+            Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, vAig ? pFaninLits[i] : -1, vAig, nSuppAll, fXor, fXorFunc );
         }
         assert( nCounter > 0 );
         if ( fXor )
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index b798961e..6e112bb8 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -80,6 +80,7 @@
 #include <time.h>
 #include <stdarg.h>
 #include <stdlib.h>
+#include <assert.h>
 
 ////////////////////////////////////////////////////////////////////////
 ///                         NAMESPACES                               ///
@@ -260,20 +261,30 @@ static inline void     Abc_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<
 static inline void     Abc_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                               }
 static inline unsigned Abc_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);                         }
 
-static inline int      Abc_Var2Lit( int Var, int fCompl )     { return Var + Var + fCompl; }
-static inline int      Abc_Lit2Var( int Lit )                 { return Lit >> 1;           }
-static inline int      Abc_LitIsCompl( int Lit )              { return Lit & 1;            }
-static inline int      Abc_LitNot( int Lit )                  { return Lit ^ 1;            }
-static inline int      Abc_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0); }
-static inline int      Abc_LitRegular( int Lit )              { return Lit & ~01;          }
-static inline int      Abc_Lit2LitV( int * pMap, int Lit )    { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) );   }
-static inline int      Abc_Lit2LitL( int * pMap, int Lit )    { return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) );   }
+static inline int      Abc_Var2Lit( int Var, int c )          { assert(Var >= 0 && !(c >> 1)); return Var + Var + c;        }
+static inline int      Abc_Lit2Var( int Lit )                 { assert(Lit >= 0); return Lit >> 1;                          }
+static inline int      Abc_LitIsCompl( int Lit )              { assert(Lit >= 0); return Lit & 1;                           }
+static inline int      Abc_LitNot( int Lit )                  { assert(Lit >= 0); return Lit ^ 1;                           }
+static inline int      Abc_LitNotCond( int Lit, int c )       { assert(Lit >= 0); return Lit ^ (int)(c > 0);                }
+static inline int      Abc_LitRegular( int Lit )              { assert(Lit >= 0); return Lit & ~01;                         }
+static inline int      Abc_Lit2LitV( int * pMap, int Lit )    { assert(Lit >= 0); return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) );      }
+static inline int      Abc_Lit2LitL( int * pMap, int Lit )    { assert(Lit >= 0); return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) );   }
 
 static inline int      Abc_Ptr2Int( void * p )                { return (int)(ABC_PTRINT_T)p;      }
 static inline void *   Abc_Int2Ptr( int i )                   { return (void *)(ABC_PTRINT_T)i;   }
 static inline word     Abc_Ptr2Wrd( void * p )                { return (word)(ABC_PTRUINT_T)p;    }
 static inline void *   Abc_Wrd2Ptr( word i )                  { return (void *)(ABC_PTRUINT_T)i;  }
 
+static inline int      Abc_Var2Lit2( int Var, int Att )       { assert(!(Att >> 2)); return (Var << 2) + Att; }
+static inline int      Abc_Lit2Var2( int Lit )                { assert(Lit >= 0);    return Lit >> 2;         }
+static inline int      Abc_Lit2Att2( int Lit )                { assert(Lit >= 0);    return Lit & 3;          }
+static inline int      Abc_Var2Lit3( int Var, int Att )       { assert(!(Att >> 3)); return (Var << 3) + Att; }
+static inline int      Abc_Lit2Var3( int Lit )                { assert(Lit >= 0);    return Lit >> 3;         }
+static inline int      Abc_Lit2Att3( int Lit )                { assert(Lit >= 0);    return Lit & 7;          }
+static inline int      Abc_Var2Lit4( int Var, int Att )       { assert(!(Att >> 4)); return (Var << 4) + Att; }
+static inline int      Abc_Lit2Var4( int Lit )                { assert(Lit >= 0);    return Lit >> 4;         }
+static inline int      Abc_Lit2Att4( int Lit )                { assert(Lit >= 0);    return Lit & 15;         }
+
 // time counting
 typedef ABC_INT64_T abctime;
 static inline abctime Abc_Clock()
diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h
index 8f3005a4..482973f7 100644
--- a/src/misc/vec/vecFlt.h
+++ b/src/misc/vec/vecFlt.h
@@ -86,6 +86,16 @@ static inline Vec_Flt_t * Vec_FltAlloc( int nCap )
     p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Flt_t * Vec_FltAllocExact( int nCap )
+{
+    Vec_Flt_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL;
+    return p;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 3e195bd3..e37743c5 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -96,6 +96,16 @@ static inline Vec_Int_t * Vec_IntAlloc( int nCap )
     p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Int_t * Vec_IntAllocExact( int nCap )
+{
+    Vec_Int_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Int_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
+    return p;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 516429ff..5fa40112 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -91,6 +91,16 @@ static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
     p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Ptr_t * Vec_PtrAllocExact( int nCap )
+{
+    Vec_Ptr_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 5f04615c..4198ac82 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -80,6 +80,16 @@ static inline Vec_Str_t * Vec_StrAlloc( int nCap )
     p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Str_t * Vec_StrAllocExact( int nCap )
+{
+    Vec_Str_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL;
+    return p;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index f2fe3216..b09852ff 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -95,6 +95,16 @@ static inline Vec_Wec_t * Vec_WecAlloc( int nCap )
     p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Wec_t * Vec_WecAllocExact( int nCap )
+{
+    Vec_Wec_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Wec_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL;
+    return p;
+}
 static inline Vec_Wec_t * Vec_WecStart( int nSize )
 {
     Vec_Wec_t * p;
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 5688d7b2..5227fec5 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -88,6 +88,16 @@ static inline Vec_Wrd_t * Vec_WrdAlloc( int nCap )
     p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL;
     return p;
 }
+static inline Vec_Wrd_t * Vec_WrdAllocExact( int nCap )
+{
+    Vec_Wrd_t * p;
+    assert( nCap >= 0 );
+    p = ABC_ALLOC( Vec_Wrd_t, 1 );
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL;
+    return p;
+}
 
 /**Function*************************************************************