| /**CFile**************************************************************** |
| |
| FileName [sbdCnf.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based optimization using internal don't-cares.] |
| |
| Synopsis [CNF computation.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sbdInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sbd_PrintCnf( Vec_Str_t * vCnf ) |
| { |
| signed char Entry; |
| int i, Lit; |
| Vec_StrForEachEntry( vCnf, Entry, i ) |
| { |
| Lit = (int)Entry; |
| if ( Lit == -1 ) |
| printf( "\n" ); |
| else |
| printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) |
| { |
| Vec_StrClear( vCnf ); |
| if ( Truth == 0 || ~Truth == 0 ) |
| { |
| // assert( nVars == 0 ); |
| Vec_StrPush( vCnf, (char)(Truth == 0) ); |
| Vec_StrPush( vCnf, (char)-1 ); |
| return 1; |
| } |
| else |
| { |
| int i, k, c, RetValue, Literal, Cube, nCubes = 0; |
| assert( nVars > 0 ); |
| for ( c = 0; c < 2; c ++ ) |
| { |
| Truth = c ? ~Truth : Truth; |
| RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); |
| assert( RetValue == 0 ); |
| nCubes += Vec_IntSize( vCover ); |
| Vec_IntForEachEntry( vCover, Cube, i ) |
| { |
| for ( k = 0; k < nVars; k++ ) |
| { |
| Literal = 3 & (Cube >> (k << 1)); |
| if ( Literal == 1 ) // '0' -> pos lit |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) ); |
| else if ( Literal == 2 ) // '1' -> neg lit |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) ); |
| else if ( Literal != 0 ) |
| assert( 0 ); |
| } |
| Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) ); |
| Vec_StrPush( vCnf, (char)-1 ); |
| } |
| } |
| return nCubes; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar ) |
| { |
| Vec_Int_t * vClause; |
| signed char Entry; |
| int i, Lit; |
| Vec_WecClear( vRes ); |
| vClause = Vec_WecPushLevel( vRes ); |
| Vec_StrForEachEntry( vCnf, Entry, i ) |
| { |
| if ( (int)Entry == -1 ) |
| { |
| vClause = Vec_WecPushLevel( vRes ); |
| continue; |
| } |
| Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry ); |
| Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar ); |
| Vec_IntPush( vClause, Lit ); |
| } |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
