diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-23 21:32:14 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-23 21:32:14 -0700 |
| commit | a6d489e7d813a1bc727a2e8d9a2ce923d837dc0c (patch) | |
| tree | e4c4decbe5cb2650ae50c9db362e0530949d0aba /src/misc/util | |
| parent | 53e7d1f9ef0b13e63f2b316c6f1de253fec6f42e (diff) | |
| download | abc-a6d489e7d813a1bc727a2e8d9a2ce923d837dc0c.tar.gz abc-a6d489e7d813a1bc727a2e8d9a2ce923d837dc0c.tar.bz2 abc-a6d489e7d813a1bc727a2e8d9a2ce923d837dc0c.zip | |
Updating &mfs to support hard objects.
Diffstat (limited to 'src/misc/util')
| -rw-r--r-- | src/misc/util/utilTruth.h | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index e0210a66..36da1271 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1534,6 +1534,36 @@ static inline int Abc_TtMinimumBase( word * t, int * pSupp, int nVarsAll, int * Abc_TtShrink( t, iVar, nVarsAll, uSupp ); return 1; } +static inline int Abc_TtSimplify( word * t, int * pLits, int nVarsAll, int * pnVars ) +{ + int v, u; + for ( v = 0; v < nVarsAll; v++ ) + { + if ( pLits[v] == 0 ) + Abc_TtCofactor0( t, Abc_TtWordNum(nVarsAll), v ); + else if ( pLits[v] == 1 ) + Abc_TtCofactor1( t, Abc_TtWordNum(nVarsAll), v ); + } + for ( v = 0; v < nVarsAll; v++ ) + for ( u = v+1; u < nVarsAll; u++ ) + if ( Abc_Lit2Var(pLits[v]) == Abc_Lit2Var(pLits[u]) ) + { + assert( nVarsAll <= 6 ); + if ( pLits[v] == pLits[u] ) + { + word t0 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor0(*t, v), u); + word t1 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor1(*t, v), u); + *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]); + } + else // if ( pLits[v] == Abc_LitNot(pLits[u]) ) + { + word t0 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor0(*t, v), u); + word t1 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor1(*t, v), u); + *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]); + } + } + return Abc_TtMinimumBase( t, pLits, nVarsAll, pnVars ); +} /**Function************************************************************* |