From a6d489e7d813a1bc727a2e8d9a2ce923d837dc0c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 23 Mar 2018 21:32:14 -0700 Subject: Updating &mfs to support hard objects. --- src/misc/util/utilTruth.h | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'src/misc/util') 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************************************************************* -- cgit v1.2.3