summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-03-25 12:17:12 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2020-03-25 12:17:12 -0700
commita277d450bf7c624392d41739788f115f1d655556 (patch)
treed24c5a50f62bbc12e0d93b1e78d5be9dfe65c80e /src
parentc7bc6b63298f532270b6c696a6f36545429dfb52 (diff)
downloadabc-a277d450bf7c624392d41739788f115f1d655556.tar.gz
abc-a277d450bf7c624392d41739788f115f1d655556.tar.bz2
abc-a277d450bf7c624392d41739788f115f1d655556.zip
Experiments with simulation-based engines.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaSimBase.c9
-rw-r--r--src/misc/util/utilTruth.h17
-rw-r--r--src/sat/bsat/satClause.h3
3 files changed, 25 insertions, 4 deletions
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index afa13691..9f07da15 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/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)) );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 3716e9dd..18bae556 100644
--- a/src/misc/util/utilTruth.h
+++ b/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;
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index d2ed3b75..74e685c3 100644
--- a/src/sat/bsat/satClause.h
+++ b/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); }