| /**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 | |