Experiments with simulation-based engines.

src/aig/gia/giaSimBase.c

@@ -936,9 +936,12 @@ Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOut
     else
     {
         printf( "The relation was successfully determized with don't-cares for %d patterns.\n", 64 * nWords );
-        printf( "Don't-cares in each output:" );
         for ( k = 0; k < nOuts; k++ )
-            printf( "   %d = %d", k, nDCs[k] );
+        {
+            int nOffs = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), nWords );
+            int nOns  = Abc_TtCountOnesVec( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), nWords );
+            printf( "%4d : Off = %6d  On = %6d  Dc = %6d (%6.2f %%)", k, nOffs, nOns, nDCs[k], 100.0*nDCs[k]/(64*nWords) );
+        }
         printf( "\n" );
     }
     Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs );
@@ -1512,7 +1515,7 @@ void Gia_RsbUpdateRemove( Gia_RsbMan_t * p, int Index )
 int Gia_RsbRemovalCost( Gia_RsbMan_t * p, int Index )
 {
     Vec_Int_t * vTemp[2][2];
-    unsigned Mask = Abc_InfoMask( Index );
+    //unsigned Mask = Abc_InfoMask( Index );
     int m, m2, Cost = 0, nLeaves = 1 << Vec_IntSize(p->vObjs);
     assert( Vec_WecSize(p->vSets[0]) == (1 << Vec_IntSize(p->vObjs)) );
     assert( Vec_WecSize(p->vSets[1]) == (1 << Vec_IntSize(p->vObjs)) );

src/misc/util/utilTruth.h

@@ -1835,6 +1835,23 @@ static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, in
             Count += Abc_TtCountOnes( pMask[w] & x[w] );
     return Count;
 }
+static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords )
+{
+    int w, Count = 0;
+    if ( !fComp0 && !fComp1 )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] &  x0[w] &  x1[w] );
+    else if (  fComp0 && !fComp1 )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & ~x0[w] &  x1[w] );
+    else if ( !fComp0 &&  fComp1 )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] &  x0[w] & ~x1[w] );
+    else 
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] );
+    return Count;
+}
 static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
 {
     int w, Count = 0;

src/sat/bsat/satClause.h

@@ -88,7 +88,8 @@ static inline void      Sat_MemWriteLimit( int * p, int nInts )      { p[0] = nI
 static inline int       Sat_MemHandPage( Sat_Mem_t * p, cla h )      { return h >> p->nPageSize;                    }
 static inline int       Sat_MemHandShift( Sat_Mem_t * p, cla h )     { return h & p->uPageMask;                     }
 
-static inline int       Sat_MemIntSize( int size, int lrn )          { return (size + 2 + lrn) & ~01;               }
+//static inline int       Sat_MemIntSize( int size, int lrn )          { return (size + 2 + lrn) & ~01;               }
+static inline int       Sat_MemIntSize( int size, int lrn )          { return 2*((size + 2 + lrn)/2);               }
 static inline int       Sat_MemClauseSize( clause * p )              { return Sat_MemIntSize(p->size, p->lrn);      }
 static inline int       Sat_MemClauseSize2( clause * p )             { return Sat_MemIntSize(p->size, 1);           }