/**CFile**************************************************************** FileName [cnfFast.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [AIG-to-CNF conversion.] Synopsis [] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] Revision [$Id: cnfFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ #include "cnf.h" #include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Detects multi-input gate rooted at this node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_CollectLeaves_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl ) { if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) ) { Vec_PtrPushUnique( vSuper, fStopCompl ? pObj : Aig_Regular(pObj) ); return; } assert( Aig_ObjIsNode(pObj) ); if ( fStopCompl ) { Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 ); } else { Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 ); } } /**Function************************************************************* Synopsis [Detects multi-input gate rooted at this node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl ) { assert( !Aig_IsComplement(pRoot) ); Vec_PtrClear( vSuper ); Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl ); } /**Function************************************************************* Synopsis [Collects nodes inside the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_CollectVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) { if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) return; Aig_ObjSetTravIdCurrent( p, pObj ); assert( Aig_ObjIsNode(pObj) ); Cnf_CollectVolume_rec( p, Aig_ObjFanin0(pObj), vNodes ); Cnf_CollectVolume_rec( p, Aig_ObjFanin1(pObj), vNodes ); Vec_PtrPush( vNodes, pObj ); } /**Function************************************************************* Synopsis [Collects nodes inside the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_CollectVolume( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) { Aig_Obj_t * pObj; int i; Aig_ManIncrementTravId( p ); Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i ) Aig_ObjSetTravIdCurrent( p, pObj ); Vec_PtrClear( vNodes ); Cnf_CollectVolume_rec( p, pRoot, vNodes ); } /**Function************************************************************* Synopsis [Derive truth table.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) { static word Truth6[6] = { ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFFFFFF00000000) }; static word C[2] = { 0, ~(word)0 }; static word S[256]; Aig_Obj_t * pObj = NULL; int i; assert( Vec_PtrSize(vLeaves) <= 6 && Vec_PtrSize(vNodes) > 0 ); assert( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) <= 256 ); Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i ) { pObj->iData = i; S[pObj->iData] = Truth6[i]; } Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { pObj->iData = Vec_PtrSize(vLeaves) + i; S[pObj->iData] = (S[Aig_ObjFanin0(pObj)->iData] ^ C[Aig_ObjFaninC0(pObj)]) & (S[Aig_ObjFanin1(pObj)->iData] ^ C[Aig_ObjFaninC1(pObj)]); } return S[pObj->iData]; } /**Function************************************************************* Synopsis [Collects nodes inside the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl ) { int iSatVar = vMap ? Vec_IntEntry(vMap, Aig_ObjId(pObj)) : Aig_ObjId(pObj); assert( iSatVar > 0 ); return iSatVar + iSatVar + fCompl; } /**Function************************************************************* Synopsis [Collects nodes inside the cone.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses ) { Aig_Obj_t * pLeaf; int c, k, Cube, OutLit, RetValue; word Truth; assert( pRoot->fMarkA ); Vec_IntClear( vClauses ); OutLit = Cnf_ObjGetLit( vMap, pRoot, 0 ); // detect cone Cnf_CollectLeaves( pRoot, vLeaves, 0 ); Cnf_CollectVolume( p, pRoot, vLeaves, vNodes ); assert( pRoot == Vec_PtrEntryLast(vNodes) ); // check if this is an AND-gate Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k ) { if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA ) break; if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA ) break; } if ( k == Vec_PtrSize(vNodes) ) { Cnf_CollectLeaves( pRoot, vLeaves, 1 ); // write big clause Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ); Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k ) Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), !Aig_IsComplement(pLeaf)) ); // write small clauses Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k ) { Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ^ 1 ); Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), Aig_IsComplement(pLeaf)) ); } return; } if ( Vec_PtrSize(vLeaves) > 6 ) printf( "FastCnfGeneration: Internal error!!!\n" ); assert( Vec_PtrSize(vLeaves) <= 6 ); Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes ); if ( Truth == 0 || Truth == ~(word)0 ) { Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, (Truth == 0) ? (OutLit ^ 1) : OutLit ); return; } RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); assert( RetValue >= 0 ); Vec_IntForEachEntry( vCover, Cube, c ) { Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) { if ( (Cube & 3) == 0 ) continue; assert( (Cube & 3) != 3 ); Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) ); } } Truth = ~Truth; RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); assert( RetValue >= 0 ); Vec_IntForEachEntry( vCover, Cube, c ) { Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ^ 1 ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) { if ( (Cube & 3) == 0 ) continue; assert( (Cube & 3) != 3 ); Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) ); } } } /**Function************************************************************* Synopsis [Marks AIG for CNF computation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cnf_DeriveFastMark( Aig_Man_t * p ) { Vec_Int_t * vSupps; Vec_Ptr_t * vLeaves, * vNodes; Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1; int i, k, nFans, Counter; vLeaves = Vec_PtrAlloc( 100 ); vNodes = Vec_PtrAlloc( 100 ); vSupps = Vec_IntStart( Aig_ManObjNumMax(p) ); // mark CIs Aig_ManForEachCi( p, pObj, i ) pObj->fMarkA = 1; // mark CO drivers Aig_ManForEachCo( p, pObj, i ) Aig_ObjFanin0(pObj)->fMarkA = 1; // mark MUX/XOR nodes Aig_ManForEachNode( p, pObj, i ) { assert( !pObj->fMarkB ); if ( !Aig_ObjIsMuxType(pObj) ) continue; pObj0 = Aig_ObjFanin0(pObj); if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 ) continue; pObj1 = Aig_ObjFanin1(pObj); if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 ) continue; // mark nodes pObj->fMarkB = 1; pObj0->fMarkB = 1; pObj1->fMarkB = 1; // mark inputs and outputs pObj->fMarkA = 1; Aig_ObjFanin0(pObj0)->fMarkA = 1; Aig_ObjFanin1(pObj0)->fMarkA = 1; Aig_ObjFanin0(pObj1)->fMarkA = 1; Aig_ObjFanin1(pObj1)->fMarkA = 1; } // mark nodes with multiple fanouts and pointed to by complemented edges Aig_ManForEachNode( p, pObj, i ) { // mark nodes with many fanouts if ( Aig_ObjRefs(pObj) > 1 ) pObj->fMarkA = 1; // mark nodes pointed to by a complemented edge if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB ) Aig_ObjFanin0(pObj)->fMarkA = 1; if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB ) Aig_ObjFanin1(pObj)->fMarkA = 1; } // compute supergate size for internal marked nodes Aig_ManForEachNode( p, pObj, i ) { if ( !pObj->fMarkA ) continue; if ( pObj->fMarkB ) { if ( !Aig_ObjIsMuxType(pObj) ) continue; pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 ); pObj0 = Aig_Regular(pObj0); pObj1 = Aig_Regular(pObj1); assert( pObj0->fMarkA ); assert( pObj1->fMarkA ); // if ( pObj0 == pObj1 ) // continue; nFans = 1 + (pObj0 == pObj1); if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 ) { pObj0->fMarkA = 0; continue; } if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 ) { pObj1->fMarkA = 0; continue; } continue; } Cnf_CollectLeaves( pObj, vLeaves, 1 ); Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) ); if ( Vec_PtrSize(vLeaves) >= 6 ) continue; Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k ) { pTemp = Aig_Regular(pTemp); assert( pTemp->fMarkA ); if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 ) continue; assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 ); if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 ) continue; pTemp->fMarkA = 0; Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 ); //printf( "%d %d ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) ); break; } } Aig_ManCleanMarkB( p ); // check CO drivers Counter = 0; Aig_ManForEachCo( p, pObj, i ) Counter += !Aig_ObjFanin0(pObj)->fMarkA; if ( Counter ) printf( "PO-driver rule is violated %d times.\n", Counter ); // check that the AND-gates are fine Counter = 0; Aig_ManForEachNode( p, pObj, i ) { assert( pObj->fMarkB == 0 ); if ( !pObj->fMarkA ) continue; Cnf_CollectLeaves( pObj, vLeaves, 0 ); if ( Vec_PtrSize(vLeaves) <= 6 ) continue; Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k ) { if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA ) Counter++; if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA ) Counter++; } } if ( Counter ) printf( "AND-gate rule is violated %d times.\n", Counter ); Vec_PtrFree( vLeaves ); Vec_PtrFree( vNodes ); Vec_IntFree( vSupps ); } /**Function************************************************************* Synopsis [Counts the number of clauses.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cnf_CutCountClauses( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vCover ) { word Truth; Aig_Obj_t * pObj; int i, RetValue, nSize = 0; if ( Vec_PtrSize(vLeaves) > 6 ) { // make sure this is an AND gate Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkA ) printf( "Unusual 1!\n" ); if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkA ) printf( "Unusual 2!\n" ); continue; assert( !Aig_ObjFaninC0(pObj) || Aig_ObjFanin0(pObj)->fMarkA ); assert( !Aig_ObjFaninC1(pObj) || Aig_ObjFanin1(pObj)->fMarkA ); } return Vec_PtrSize(vLeaves) + 1; } Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes ); RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); assert( RetValue >= 0 ); nSize += Vec_IntSize(vCover); Truth = ~Truth; RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); assert( RetValue >= 0 ); nSize += Vec_IntSize(vCover); return nSize; } /**Function************************************************************* Synopsis [Counts the size of the CNF, assuming marks are set.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cnf_CountCnfSize( Aig_Man_t * p ) { Vec_Ptr_t * vLeaves, * vNodes; Vec_Int_t * vCover; Aig_Obj_t * pObj; int nVars = 0, nClauses = 0; int i, nSize; vLeaves = Vec_PtrAlloc( 100 ); vNodes = Vec_PtrAlloc( 100 ); vCover = Vec_IntAlloc( 1 << 16 ); Aig_ManForEachObj( p, pObj, i ) nVars += pObj->fMarkA; Aig_ManForEachNode( p, pObj, i ) { if ( !pObj->fMarkA ) continue; Cnf_CollectLeaves( pObj, vLeaves, 0 ); Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); assert( pObj == Vec_PtrEntryLast(vNodes) ); nSize = Cnf_CutCountClauses( p, vLeaves, vNodes, vCover ); // printf( "%d(%d) ", Vec_PtrSize(vLeaves), nSize ); nClauses += nSize; } // printf( "\n" ); printf( "Vars = %d Clauses = %d\n", nVars, nClauses ); Vec_PtrFree( vLeaves ); Vec_PtrFree( vNodes ); Vec_IntFree( vCover ); return nClauses; } /**Function************************************************************* Synopsis [Derives CNF from the marked AIG.] Description [Assumes that marking is such that when we traverse from each marked node, the logic cone has 6 inputs or less, or it is a multi-input AND.] SideEffects [] SeeAlso [] ***********************************************************************/ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) { Cnf_Dat_t * pCnf; Vec_Int_t * vLits, * vClas, * vMap, * vTemp; Vec_Ptr_t * vLeaves, * vNodes; Vec_Int_t * vCover; Aig_Obj_t * pObj; int i, k, nVars, Entry, OutLit, DriLit; vLits = Vec_IntAlloc( 1 << 16 ); vClas = Vec_IntAlloc( 1 << 12 ); vMap = Vec_IntStartFull( Aig_ManObjNumMax(p) ); // assign variables for the outputs nVars = 1; if ( nOutputs ) { if ( Aig_ManRegNum(p) == 0 ) { assert( nOutputs == Aig_ManCoNum(p) ); Aig_ManForEachCo( p, pObj, i ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); } else { assert( nOutputs == Aig_ManRegNum(p) ); Aig_ManForEachLiSeq( p, pObj, i ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); } } // assign variables to the internal nodes Aig_ManForEachNodeReverse( p, pObj, i ) if ( pObj->fMarkA ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); // assign variables to the PIs and constant node Aig_ManForEachCi( p, pObj, i ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ ); // create clauses vLeaves = Vec_PtrAlloc( 100 ); vNodes = Vec_PtrAlloc( 100 ); vCover = Vec_IntAlloc( 1 << 16 ); vTemp = Vec_IntAlloc( 100 ); Aig_ManForEachNodeReverse( p, pObj, i ) { if ( !pObj->fMarkA ) continue; Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp ); Vec_IntForEachEntry( vTemp, Entry, k ) { if ( Entry == 0 ) Vec_IntPush( vClas, Vec_IntSize(vLits) ); else Vec_IntPush( vLits, Entry ); } } Vec_PtrFree( vLeaves ); Vec_PtrFree( vNodes ); Vec_IntFree( vCover ); Vec_IntFree( vTemp ); // create clauses for the outputs Aig_ManForEachCo( p, pObj, i ) { DriLit = Cnf_ObjGetLit( vMap, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj) ); if ( i < Aig_ManCoNum(p) - nOutputs ) { Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vLits, DriLit ); } else { OutLit = Cnf_ObjGetLit( vMap, pObj, 0 ); // first clause Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vLits, OutLit ); Vec_IntPush( vLits, DriLit ^ 1 ); // second clause Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vLits, OutLit ^ 1 ); Vec_IntPush( vLits, DriLit ); } } // write the constant literal OutLit = Cnf_ObjGetLit( vMap, Aig_ManConst1(p), 0 ); Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vLits, OutLit ); // create structure pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); pCnf->pMan = p; pCnf->nVars = nVars; pCnf->nLiterals = Vec_IntSize( vLits ); pCnf->nClauses = Vec_IntSize( vClas ); pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses + 1 ); pCnf->pClauses[0] = Vec_IntReleaseArray( vLits ); Vec_IntForEachEntry( vClas, Entry, i ) pCnf->pClauses[i] = pCnf->pClauses[0] + Entry; pCnf->pClauses[pCnf->nClauses] = pCnf->pClauses[0] + pCnf->nLiterals; pCnf->pVarNums = Vec_IntReleaseArray( vMap ); // cleanup Vec_IntFree( vLits ); Vec_IntFree( vClas ); Vec_IntFree( vMap ); return pCnf; } /**Function************************************************************* Synopsis [Fast CNF computation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs ) { Cnf_Dat_t * pCnf = NULL; abctime clk;//, clkTotal = Abc_Clock(); // printf( "\n" ); Aig_ManCleanMarkAB( p ); // create initial marking clk = Abc_Clock(); Cnf_DeriveFastMark( p ); // Abc_PrintTime( 1, "Marking", Abc_Clock() - clk ); // compute CNF size clk = Abc_Clock(); pCnf = Cnf_DeriveFastClauses( p, nOutputs ); // Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk ); // derive the resulting CNF Aig_ManCleanMarkA( p ); // Abc_PrintTime( 1, "TOTAL ", Abc_Clock() - clkTotal ); // printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); // Cnf_DataFree( pCnf ); // pCnf = NULL; return pCnf; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END