Version abc80313

1 files changed, 23 insertions, 1 deletions

diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c
index d86a938d..b7f10344 100644
--- a/src/aig/bdc/bdcTable.c
+++ b/src/aig/bdc/bdcTable.c
@@ -42,6 +42,9 @@
 void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 {
     int v;
+    // compute support
+    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
+        Kit_TruthSupport( pIsf->puOff, p->nVars );
     // go through the support variables
     for ( v = 0; v < p->nVars; v++ )
     {
@@ -72,7 +75,7 @@ void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
 {
     return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
-         Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars );
+         Kit_TruthIsDisjoint( puTruth, pIsf->puOff, p->nVars );
 }
 
 /**Function*************************************************************
@@ -88,10 +91,29 @@ int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTru
 ***********************************************************************/
 Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 {
+    int fDisableCache = 0;
     Bdc_Fun_t * pFunc;
+    if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 )
+        return NULL;
+    if ( pIsf->uSupp == 0 )
+    {
+        assert( p->pTable[pIsf->uSupp] == p->pNodes );
+        if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) )
+            return p->pNodes;
+        assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) );
+        return Bdc_Not(p->pNodes);
+    }
     for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
         if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
              return pFunc;
+    Bdc_IsfNot( pIsf );
+    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
+        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
+        {
+            Bdc_IsfNot( pIsf );
+            return Bdc_Not(pFunc);
+        }
+    Bdc_IsfNot( pIsf );
     return NULL;
 }