src/aig/fra/fraCnf.c File Reference

#include "fra.h"
Include dependency graph for fraCnf.c:

Go to the source code of this file.

Functions

void Fra_AddClausesMux (Fra_Man_t *p, Aig_Obj_t *pNode)
void Fra_AddClausesSuper (Fra_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
void Fra_CollectSuper_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Vec_Ptr_t * Fra_CollectSuper (Aig_Obj_t *pObj, int fUseMuxes)
void Fra_ObjAddToFrontier (Fra_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
void Fra_CnfNodeAddToSolver (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)

Function Documentation

void Fra_AddClausesMux ( Fra_Man_t *  p,
Aig_Obj_t *  pNode 
)

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

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraCnf.c.

00044 {
00045     Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
00046     int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
00047 
00048     assert( !Aig_IsComplement( pNode ) );
00049     assert( Aig_ObjIsMuxType( pNode ) );
00050     // get nodes (I = if, T = then, E = else)
00051     pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
00052     // get the variable numbers
00053     VarF = Fra_ObjSatNum(pNode);
00054     VarI = Fra_ObjSatNum(pNodeI);
00055     VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
00056     VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
00057     // get the complementation flags
00058     fCompT = Aig_IsComplement(pNodeT);
00059     fCompE = Aig_IsComplement(pNodeE);
00060 
00061     // f = ITE(i, t, e)
00062 
00063     // i' + t' + f
00064     // i' + t  + f'
00065     // i  + e' + f
00066     // i  + e  + f'
00067 
00068     // create four clauses
00069     pLits[0] = toLitCond(VarI, 1);
00070     pLits[1] = toLitCond(VarT, 1^fCompT);
00071     pLits[2] = toLitCond(VarF, 0);
00072     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00073     assert( RetValue );
00074     pLits[0] = toLitCond(VarI, 1);
00075     pLits[1] = toLitCond(VarT, 0^fCompT);
00076     pLits[2] = toLitCond(VarF, 1);
00077     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00078     assert( RetValue );
00079     pLits[0] = toLitCond(VarI, 0);
00080     pLits[1] = toLitCond(VarE, 1^fCompE);
00081     pLits[2] = toLitCond(VarF, 0);
00082     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00083     assert( RetValue );
00084     pLits[0] = toLitCond(VarI, 0);
00085     pLits[1] = toLitCond(VarE, 0^fCompE);
00086     pLits[2] = toLitCond(VarF, 1);
00087     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00088     assert( RetValue );
00089 
00090     // two additional clauses
00091     // t' & e' -> f'
00092     // t  & e  -> f 
00093 
00094     // t  + e   + f'
00095     // t' + e'  + f 
00096 
00097     if ( VarT == VarE )
00098     {
00099 //        assert( fCompT == !fCompE );
00100         return;
00101     }
00102 
00103     pLits[0] = toLitCond(VarT, 0^fCompT);
00104     pLits[1] = toLitCond(VarE, 0^fCompE);
00105     pLits[2] = toLitCond(VarF, 1);
00106     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00107     assert( RetValue );
00108     pLits[0] = toLitCond(VarT, 1^fCompT);
00109     pLits[1] = toLitCond(VarE, 1^fCompE);
00110     pLits[2] = toLitCond(VarF, 0);
00111     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
00112     assert( RetValue );
00113 }

void Fra_AddClausesSuper ( Fra_Man_t *  p,
Aig_Obj_t *  pNode,
Vec_Ptr_t *  vSuper 
)

Function*************************************************************

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file fraCnf.c.

00127 {
00128     Aig_Obj_t * pFanin;
00129     int * pLits, nLits, RetValue, i;
00130     assert( !Aig_IsComplement(pNode) );
00131     assert( Aig_ObjIsNode( pNode ) );
00132     // create storage for literals
00133     nLits = Vec_PtrSize(vSuper) + 1;
00134     pLits = ALLOC( int, nLits );
00135     // suppose AND-gate is A & B = C
00136     // add !A => !C   or   A + !C
00137     Vec_PtrForEachEntry( vSuper, pFanin, i )
00138     {
00139         pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
00140         pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
00141         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
00142         assert( RetValue );
00143     }
00144     // add A & B => C   or   !A + !B + C
00145     Vec_PtrForEachEntry( vSuper, pFanin, i )
00146         pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
00147     pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
00148     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
00149     assert( RetValue );
00150     free( pLits );
00151 }

void Fra_CnfNodeAddToSolver ( Fra_Man_t *  p,
Aig_Obj_t *  pOld,
Aig_Obj_t *  pNew 
)

Function*************************************************************

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file fraCnf.c.

00238 { 
00239     Vec_Ptr_t * vFrontier, * vFanins;
00240     Aig_Obj_t * pNode, * pFanin;
00241     int i, k, fUseMuxes = 1;
00242     assert( pOld || pNew );
00243     // quit if CNF is ready
00244     if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
00245         return;
00246     // start the frontier
00247     vFrontier = Vec_PtrAlloc( 100 );
00248     if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
00249     if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
00250     // explore nodes in the frontier
00251     Vec_PtrForEachEntry( vFrontier, pNode, i )
00252     {
00253         // create the supergate
00254         assert( Fra_ObjSatNum(pNode) );
00255         assert( Fra_ObjFaninVec(pNode) == NULL );
00256         if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
00257         {
00258             vFanins = Vec_PtrAlloc( 4 );
00259             Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
00260             Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
00261             Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
00262             Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
00263             Vec_PtrForEachEntry( vFanins, pFanin, k )
00264                 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
00265             Fra_AddClausesMux( p, pNode );
00266         }
00267         else
00268         {
00269             vFanins = Fra_CollectSuper( pNode, fUseMuxes );
00270             Vec_PtrForEachEntry( vFanins, pFanin, k )
00271                 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
00272             Fra_AddClausesSuper( p, pNode, vFanins );
00273         }
00274         assert( Vec_PtrSize(vFanins) > 1 );
00275         Fra_ObjSetFaninVec( pNode, vFanins );
00276     }
00277     Vec_PtrFree( vFrontier );
00278 }

Vec_Ptr_t* Fra_CollectSuper ( Aig_Obj_t *  pObj,
int  fUseMuxes 
)

Function*************************************************************

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file fraCnf.c.

00190 {
00191     Vec_Ptr_t * vSuper;
00192     assert( !Aig_IsComplement(pObj) );
00193     assert( !Aig_ObjIsPi(pObj) );
00194     vSuper = Vec_PtrAlloc( 4 );
00195     Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
00196     return vSuper;
00197 }

void Fra_CollectSuper_rec ( Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper,
int  fFirst,
int  fUseMuxes 
)

Function*************************************************************

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file fraCnf.c.

00165 {
00166     // if the new node is complemented or a PI, another gate begins
00167     if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
00168          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
00169     {
00170         Vec_PtrPushUnique( vSuper, pObj );
00171         return;
00172     }
00173     // go through the branches
00174     Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
00175     Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
00176 }

void Fra_ObjAddToFrontier ( Fra_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vFrontier 
)

Function*************************************************************

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file fraCnf.c.

00211 {
00212     Fra_Man_t * pTemp = pObj->pData;
00213     assert( !Aig_IsComplement(pObj) );
00214     if ( Fra_ObjSatNum(pObj) )
00215         return;
00216     assert( Fra_ObjSatNum(pObj) == 0 );
00217     assert( Fra_ObjFaninVec(pObj) == NULL );
00218     if ( Aig_ObjIsConst1(pObj) )
00219         return;
00220 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
00221     Fra_ObjSetSatNum( pObj, p->nSatVars++ );
00222     if ( Aig_ObjIsNode(pObj) )
00223         Vec_PtrPush( vFrontier, pObj );
00224 }

Generated on Tue Jan 5 12:18:19 2010 for abc70930 by  doxygen 1.6.1