diff options
Diffstat (limited to 'src/aig/fra/fraCnf.c')
-rw-r--r-- | src/aig/fra/fraCnf.c | 284 |
1 files changed, 284 insertions, 0 deletions
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c new file mode 100644 index 00000000..d96fe8a1 --- /dev/null +++ b/src/aig/fra/fraCnf.c @@ -0,0 +1,284 @@ +/**CFile**************************************************************** + + FileName [fraCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode ) +{ + Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_ObjIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Fra_ObjSatNum(pNode); + VarI = Fra_ObjSatNum(pNodeI); + VarT = Fra_ObjSatNum(Aig_Regular(pNodeT)); + VarE = Fra_ObjSatNum(Aig_Regular(pNodeE)); + // get the complementation flags + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 1^fCompT); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 0^fCompT); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = toLitCond(VarT, 0^fCompT); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarT, 1^fCompT); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) +{ + Aig_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); + pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); + pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + free( pLits ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || + (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes ) +{ + Vec_Ptr_t * vSuper; + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPi(pObj) ); + vSuper = Vec_PtrAlloc( 4 ); + Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); + return vSuper; +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +{ + assert( !Aig_IsComplement(pObj) ); + if ( Fra_ObjSatNum(pObj) ) + return; + assert( Fra_ObjSatNum(pObj) == 0 ); + assert( Fra_ObjFaninVec(pObj) == NULL ); + if ( Aig_ObjIsConst1(pObj) ) + return; + Fra_ObjSetSatNum( pObj, p->nSatVars++ ); + if ( Aig_ObjIsNode(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +{ + Vec_Ptr_t * vFrontier, * vFanins; + Aig_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + assert( pOld || pNew ); + // quit if CNF is ready + if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) ) + return; + // start the frontier + vFrontier = Vec_PtrAlloc( 100 ); + if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier ); + if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier ); + // explore nodes in the frontier + Vec_PtrForEachEntry( vFrontier, pNode, i ) + { + // create the supergate + assert( Fra_ObjSatNum(pNode) ); + assert( Fra_ObjFaninVec(pNode) == NULL ); + if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) + { + vFanins = Vec_PtrAlloc( 4 ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Fra_AddClausesMux( p, pNode ); + } + else + { + vFanins = Fra_CollectSuper( pNode, fUseMuxes ); + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); + Fra_AddClausesSuper( p, pNode, vFanins ); + } + assert( Vec_PtrSize(vFanins) > 1 ); + Fra_ObjSetFaninVec( pNode, vFanins ); + } + Vec_PtrFree( vFrontier ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |