summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-06-18 17:28:20 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-06-18 17:28:20 -0700
commit9842a666e6c1d2546c940c48bbd6602a448bc01b (patch)
tree493f1b83b6f05c9589497670e72dd5a830c7abf6 /src
parent590f74e9c1cd927108a8db2f601302eaa098993c (diff)
downloadabc-9842a666e6c1d2546c940c48bbd6602a448bc01b.tar.gz
abc-9842a666e6c1d2546c940c48bbd6602a448bc01b.tar.bz2
abc-9842a666e6c1d2546c940c48bbd6602a448bc01b.zip
Experiments with CNF generation.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaJf.c5
-rw-r--r--src/bool/rsb/rsbDec6.c2
-rw-r--r--src/misc/util/utilTruth.h13
3 files changed, 13 insertions, 7 deletions
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 08ad17c7..b5aa7787 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -397,7 +397,10 @@ void Jf_ManFree( Jf_Man_t * p )
if ( p->pPars->fVerbose && p->pDsd )
Sdm_ManPrintDsdStats( p->pDsd, 0 );
if ( p->pPars->fVerbose && p->vTtMem )
- printf( "Unique truth tables = %d. Memory = %.2f MB\n", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
+ {
+ printf( "Unique truth tables = %d. Memory = %.2f MB ", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+ }
if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && p->pPars->fFuncDsd )
Jf_ManProfileClasses( p );
if ( p->pPars->fCoarsen )
diff --git a/src/bool/rsb/rsbDec6.c b/src/bool/rsb/rsbDec6.c
index 88644686..da2652ba 100644
--- a/src/bool/rsb/rsbDec6.c
+++ b/src/bool/rsb/rsbDec6.c
@@ -519,7 +519,7 @@ void Rsb_DecPrintFunc( Rsb_Man_t * p, unsigned Truth4, word * f, word ** ppGs, i
word Copy = Truth4;
word wOn = Abc_Tt6Stretch( Copy >> (1 << nVars), nVars );
word wOnDc = ~Abc_Tt6Stretch( Copy, nVars );
- word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars );
+ word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars, NULL );
int i;
printf( "Offset : " );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index c82dc9e1..2fc4f3ce 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1416,16 +1416,19 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
SeeAlso []
***********************************************************************/
-static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
+static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars, int * pnCubes )
{
word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
int Var;
- assert( nVars <= 5 );
+ assert( nVars <= 6 );
assert( (uOn & ~uOnDc) == 0 );
if ( uOn == 0 )
return 0;
if ( uOnDc == ~(word)0 )
+ {
+ (*pnCubes)++;
return ~(word)0;
+ }
assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
@@ -1438,9 +1441,9 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
// solve for cofactors
- uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var );
- uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var );
- uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var );
+ uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var, pnCubes );
+ uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var, pnCubes );
+ uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pnCubes );
// derive the final truth table
uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
assert( (uOn & ~uRes2) == 0 );