ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
fraCnf.c File Reference
#include "fra.h"
Include dependency graph for fraCnf.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux (Fra_Man_t *p, Aig_Obj_t *pNode)
 DECLARATIONS ///.
 
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

◆ Fra_AddClausesMux()

ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux ( Fra_Man_t * p,
Aig_Obj_t * pNode )

DECLARATIONS ///.

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

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraCnf.c.

47{
48 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
49 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
50
51 assert( !Aig_IsComplement( pNode ) );
52 assert( Aig_ObjIsMuxType( pNode ) );
53 // get nodes (I = if, T = then, E = else)
54 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
55 // get the variable numbers
56 VarF = Fra_ObjSatNum(pNode);
57 VarI = Fra_ObjSatNum(pNodeI);
58 VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
59 VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
60 // get the complementation flags
61 fCompT = Aig_IsComplement(pNodeT);
62 fCompE = Aig_IsComplement(pNodeE);
63
64 // f = ITE(i, t, e)
65
66 // i' + t' + f
67 // i' + t + f'
68 // i + e' + f
69 // i + e + f'
70
71 // create four clauses
72 pLits[0] = toLitCond(VarI, 1);
73 pLits[1] = toLitCond(VarT, 1^fCompT);
74 pLits[2] = toLitCond(VarF, 0);
75 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
76 assert( RetValue );
77 pLits[0] = toLitCond(VarI, 1);
78 pLits[1] = toLitCond(VarT, 0^fCompT);
79 pLits[2] = toLitCond(VarF, 1);
80 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
81 assert( RetValue );
82 pLits[0] = toLitCond(VarI, 0);
83 pLits[1] = toLitCond(VarE, 1^fCompE);
84 pLits[2] = toLitCond(VarF, 0);
85 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
86 assert( RetValue );
87 pLits[0] = toLitCond(VarI, 0);
88 pLits[1] = toLitCond(VarE, 0^fCompE);
89 pLits[2] = toLitCond(VarF, 1);
90 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
91 assert( RetValue );
92
93 // two additional clauses
94 // t' & e' -> f'
95 // t & e -> f
96
97 // t + e + f'
98 // t' + e' + f
99
100 if ( VarT == VarE )
101 {
102// assert( fCompT == !fCompE );
103 return;
104 }
105
106 pLits[0] = toLitCond(VarT, 0^fCompT);
107 pLits[1] = toLitCond(VarE, 0^fCompE);
108 pLits[2] = toLitCond(VarF, 1);
109 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
110 assert( RetValue );
111 pLits[0] = toLitCond(VarT, 1^fCompT);
112 pLits[1] = toLitCond(VarE, 1^fCompE);
113 pLits[2] = toLitCond(VarF, 0);
114 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
115 assert( RetValue );
116}
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition aigUtil.c:387
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition aigUtil.c:307
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
p
Cube * p
Definition exorList.c:222
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fra_AddClausesSuper()

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 129 of file fraCnf.c.

130{
131 Aig_Obj_t * pFanin;
132 int * pLits, nLits, RetValue, i;
133 assert( !Aig_IsComplement(pNode) );
134 assert( Aig_ObjIsNode( pNode ) );
135 // create storage for literals
136 nLits = Vec_PtrSize(vSuper) + 1;
137 pLits = ABC_ALLOC( int, nLits );
138 // suppose AND-gate is A & B = C
139 // add !A => !C or A + !C
140 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
141 {
142 pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
143 pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
144 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
145 assert( RetValue );
146 }
147 // add A & B => C or !A + !B + C
148 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
149 pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
150 pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
151 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
152 assert( RetValue );
153 ABC_FREE( pLits );
154}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the caller graph for this function:

◆ Fra_CnfNodeAddToSolver()

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 238 of file fraCnf.c.

239{
240 Vec_Ptr_t * vFrontier, * vFanins;
241 Aig_Obj_t * pNode, * pFanin;
242 int i, k, fUseMuxes = 1;
243 assert( pOld || pNew );
244 // quit if CNF is ready
245 if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
246 return;
247 // start the frontier
248 vFrontier = Vec_PtrAlloc( 100 );
249 if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
250 if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
251 // explore nodes in the frontier
252 Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
253 {
254 // create the supergate
255 assert( Fra_ObjSatNum(pNode) );
256 assert( Fra_ObjFaninVec(pNode) == NULL );
257 if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
258 {
259 vFanins = Vec_PtrAlloc( 4 );
260 Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
261 Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
262 Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
263 Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
264 Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
265 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
266 Fra_AddClausesMux( p, pNode );
267 }
268 else
269 {
270 vFanins = Fra_CollectSuper( pNode, fUseMuxes );
271 Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
272 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
273 Fra_AddClausesSuper( p, pNode, vFanins );
274 }
275 assert( Vec_PtrSize(vFanins) > 1 );
276 Fra_ObjSetFaninVec( pNode, vFanins );
277 }
278 Vec_PtrFree( vFrontier );
279}
Fra_AddClausesSuper
void Fra_AddClausesSuper(Fra_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition fraCnf.c:129
Fra_ObjAddToFrontier
void Fra_ObjAddToFrontier(Fra_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition fraCnf.c:213
Fra_CollectSuper
Vec_Ptr_t * Fra_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes)
Definition fraCnf.c:192
Fra_AddClausesMux
ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux(Fra_Man_t *p, Aig_Obj_t *pNode)
DECLARATIONS ///.
Definition fraCnf.c:46
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fra_CollectSuper()

Vec_Ptr_t * Fra_CollectSuper ( Aig_Obj_t * pObj,
int fUseMuxes )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file fraCnf.c.

193{
194 Vec_Ptr_t * vSuper;
195 assert( !Aig_IsComplement(pObj) );
196 assert( !Aig_ObjIsCi(pObj) );
197 vSuper = Vec_PtrAlloc( 4 );
198 Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
199 return vSuper;
200}
Fra_CollectSuper_rec
void Fra_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition fraCnf.c:167
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fra_CollectSuper_rec()

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 167 of file fraCnf.c.

168{
169 // if the new node is complemented or a PI, another gate begins
170 if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) ||
171 (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
172 {
173 Vec_PtrPushUnique( vSuper, pObj );
174 return;
175 }
176 // go through the branches
177 Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
178 Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
179}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fra_ObjAddToFrontier()

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 213 of file fraCnf.c.

214{
215 assert( !Aig_IsComplement(pObj) );
216 if ( Fra_ObjSatNum(pObj) )
217 return;
218 assert( Fra_ObjSatNum(pObj) == 0 );
219 assert( Fra_ObjFaninVec(pObj) == NULL );
220 if ( Aig_ObjIsConst1(pObj) )
221 return;
222 Fra_ObjSetSatNum( pObj, p->nSatVars++ );
223 if ( Aig_ObjIsNode(pObj) )
224 Vec_PtrPush( vFrontier, pObj );
225}
Here is the caller graph for this function: