1 /**CFile****************************************************************
2
3 FileName [fraCnf.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34
35 /**Function*************************************************************
36
37 Synopsis [Addes clauses to the solver.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Fra_AddClausesMux(Fra_Man_t * p,Aig_Obj_t * pNode)46 void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
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 }
117
118 /**Function*************************************************************
119
120 Synopsis [Addes clauses to the solver.]
121
122 Description []
123
124 SideEffects []
125
126 SeeAlso []
127
128 ***********************************************************************/
Fra_AddClausesSuper(Fra_Man_t * p,Aig_Obj_t * pNode,Vec_Ptr_t * vSuper)129 void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
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 }
155
156 /**Function*************************************************************
157
158 Synopsis [Collects the supergate.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
Fra_CollectSuper_rec(Aig_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)167 void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
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 }
180
181 /**Function*************************************************************
182
183 Synopsis [Collects the supergate.]
184
185 Description []
186
187 SideEffects []
188
189 SeeAlso []
190
191 ***********************************************************************/
Fra_CollectSuper(Aig_Obj_t * pObj,int fUseMuxes)192 Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
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 }
201
202 /**Function*************************************************************
203
204 Synopsis [Updates the solver clause database.]
205
206 Description []
207
208 SideEffects []
209
210 SeeAlso []
211
212 ***********************************************************************/
Fra_ObjAddToFrontier(Fra_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vFrontier)213 void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
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 }
226
227 /**Function*************************************************************
228
229 Synopsis [Updates the solver clause database.]
230
231 Description []
232
233 SideEffects []
234
235 SeeAlso []
236
237 ***********************************************************************/
Fra_CnfNodeAddToSolver(Fra_Man_t * p,Aig_Obj_t * pOld,Aig_Obj_t * pNew)238 void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
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 }
280
281
282
283 ////////////////////////////////////////////////////////////////////////
284 /// END OF FILE ///
285 ////////////////////////////////////////////////////////////////////////
286
287
288 ABC_NAMESPACE_IMPL_END
289
290