1 /**CFile****************************************************************
2
3 FileName [sswCnf.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Computation of CNF.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Starts the SAT manager.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Ssw_SatStart(int fPolarFlip)45 Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
46 {
47 Ssw_Sat_t * p;
48 int Lit;
49 p = ABC_ALLOC( Ssw_Sat_t, 1 );
50 memset( p, 0, sizeof(Ssw_Sat_t) );
51 p->pAig = NULL;
52 p->fPolarFlip = fPolarFlip;
53 p->vSatVars = Vec_IntStart( 10000 );
54 p->vFanins = Vec_PtrAlloc( 100 );
55 p->vUsedPis = Vec_PtrAlloc( 100 );
56 p->pSat = sat_solver_new();
57 sat_solver_setnvars( p->pSat, 1000 );
58 // var 0 is not used
59 // var 1 is reserved for const1 node - add the clause
60 p->nSatVars = 1;
61 Lit = toLit( p->nSatVars );
62 if ( fPolarFlip )
63 Lit = lit_neg( Lit );
64 sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
65 // Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
66 Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
67 return p;
68 }
69
70 /**Function*************************************************************
71
72 Synopsis [Stop the SAT manager.]
73
74 Description []
75
76 SideEffects []
77
78 SeeAlso []
79
80 ***********************************************************************/
Ssw_SatStop(Ssw_Sat_t * p)81 void Ssw_SatStop( Ssw_Sat_t * p )
82 {
83 // Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n",
84 // p->pSat->size, p->pSat->stats.starts );
85 if ( p->pSat )
86 sat_solver_delete( p->pSat );
87 Vec_IntFree( p->vSatVars );
88 Vec_PtrFree( p->vFanins );
89 Vec_PtrFree( p->vUsedPis );
90 ABC_FREE( p );
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Addes clauses to the solver.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Ssw_AddClausesMux(Ssw_Sat_t * p,Aig_Obj_t * pNode)104 void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
105 {
106 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
107 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
108
109 assert( !Aig_IsComplement( pNode ) );
110 assert( Aig_ObjIsMuxType( pNode ) );
111 // get nodes (I = if, T = then, E = else)
112 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
113 // get the variable numbers
114 VarF = Ssw_ObjSatNum(p,pNode);
115 VarI = Ssw_ObjSatNum(p,pNodeI);
116 VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT));
117 VarE = Ssw_ObjSatNum(p,Aig_Regular(pNodeE));
118 // get the complementation flags
119 fCompT = Aig_IsComplement(pNodeT);
120 fCompE = Aig_IsComplement(pNodeE);
121
122 // f = ITE(i, t, e)
123
124 // i' + t' + f
125 // i' + t + f'
126 // i + e' + f
127 // i + e + f'
128
129 // create four clauses
130 pLits[0] = toLitCond(VarI, 1);
131 pLits[1] = toLitCond(VarT, 1^fCompT);
132 pLits[2] = toLitCond(VarF, 0);
133 if ( p->fPolarFlip )
134 {
135 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
136 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
137 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
138 }
139 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
140 assert( RetValue );
141 pLits[0] = toLitCond(VarI, 1);
142 pLits[1] = toLitCond(VarT, 0^fCompT);
143 pLits[2] = toLitCond(VarF, 1);
144 if ( p->fPolarFlip )
145 {
146 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
147 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
148 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
149 }
150 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
151 assert( RetValue );
152 pLits[0] = toLitCond(VarI, 0);
153 pLits[1] = toLitCond(VarE, 1^fCompE);
154 pLits[2] = toLitCond(VarF, 0);
155 if ( p->fPolarFlip )
156 {
157 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
158 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
159 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
160 }
161 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
162 assert( RetValue );
163 pLits[0] = toLitCond(VarI, 0);
164 pLits[1] = toLitCond(VarE, 0^fCompE);
165 pLits[2] = toLitCond(VarF, 1);
166 if ( p->fPolarFlip )
167 {
168 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
169 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
170 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
171 }
172 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
173 assert( RetValue );
174
175 // two additional clauses
176 // t' & e' -> f'
177 // t & e -> f
178
179 // t + e + f'
180 // t' + e' + f
181
182 if ( VarT == VarE )
183 {
184 // assert( fCompT == !fCompE );
185 return;
186 }
187
188 pLits[0] = toLitCond(VarT, 0^fCompT);
189 pLits[1] = toLitCond(VarE, 0^fCompE);
190 pLits[2] = toLitCond(VarF, 1);
191 if ( p->fPolarFlip )
192 {
193 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
194 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
195 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
196 }
197 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
198 assert( RetValue );
199 pLits[0] = toLitCond(VarT, 1^fCompT);
200 pLits[1] = toLitCond(VarE, 1^fCompE);
201 pLits[2] = toLitCond(VarF, 0);
202 if ( p->fPolarFlip )
203 {
204 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
205 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
206 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
207 }
208 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
209 assert( RetValue );
210 }
211
212 /**Function*************************************************************
213
214 Synopsis [Addes clauses to the solver.]
215
216 Description []
217
218 SideEffects []
219
220 SeeAlso []
221
222 ***********************************************************************/
Ssw_AddClausesSuper(Ssw_Sat_t * p,Aig_Obj_t * pNode,Vec_Ptr_t * vSuper)223 void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
224 {
225 Aig_Obj_t * pFanin;
226 int * pLits, nLits, RetValue, i;
227 assert( !Aig_IsComplement(pNode) );
228 assert( Aig_ObjIsNode( pNode ) );
229 // create storage for literals
230 nLits = Vec_PtrSize(vSuper) + 1;
231 pLits = ABC_ALLOC( int, nLits );
232 // suppose AND-gate is A & B = C
233 // add !A => !C or A + !C
234 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
235 {
236 pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
237 pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
238 if ( p->fPolarFlip )
239 {
240 if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
241 if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
242 }
243 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
244 assert( RetValue );
245 }
246 // add A & B => C or !A + !B + C
247 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
248 {
249 pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
250 if ( p->fPolarFlip )
251 {
252 if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
253 }
254 }
255 pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
256 if ( p->fPolarFlip )
257 {
258 if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
259 }
260 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
261 assert( RetValue );
262 ABC_FREE( pLits );
263 }
264
265 /**Function*************************************************************
266
267 Synopsis [Collects the supergate.]
268
269 Description []
270
271 SideEffects []
272
273 SeeAlso []
274
275 ***********************************************************************/
Ssw_CollectSuper_rec(Aig_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)276 void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
277 {
278 // if the new node is complemented or a PI, another gate begins
279 if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
280 (!fFirst && Aig_ObjRefs(pObj) > 1) ||
281 (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
282 {
283 Vec_PtrPushUnique( vSuper, pObj );
284 return;
285 }
286 // pObj->fMarkA = 1;
287 // go through the branches
288 Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
289 Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
290 }
291
292 /**Function*************************************************************
293
294 Synopsis [Collects the supergate.]
295
296 Description []
297
298 SideEffects []
299
300 SeeAlso []
301
302 ***********************************************************************/
Ssw_CollectSuper(Aig_Obj_t * pObj,int fUseMuxes,Vec_Ptr_t * vSuper)303 void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
304 {
305 assert( !Aig_IsComplement(pObj) );
306 assert( !Aig_ObjIsCi(pObj) );
307 Vec_PtrClear( vSuper );
308 Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
309 }
310
311 /**Function*************************************************************
312
313 Synopsis [Updates the solver clause database.]
314
315 Description []
316
317 SideEffects []
318
319 SeeAlso []
320
321 ***********************************************************************/
Ssw_ObjAddToFrontier(Ssw_Sat_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vFrontier)322 void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
323 {
324 assert( !Aig_IsComplement(pObj) );
325 if ( Ssw_ObjSatNum(p,pObj) )
326 return;
327 assert( Ssw_ObjSatNum(p,pObj) == 0 );
328 if ( Aig_ObjIsConst1(pObj) )
329 return;
330 // pObj->fMarkA = 1;
331 // save PIs (used by register correspondence)
332 if ( Aig_ObjIsCi(pObj) )
333 Vec_PtrPush( p->vUsedPis, pObj );
334 Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
335 sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
336 if ( Aig_ObjIsNode(pObj) )
337 Vec_PtrPush( vFrontier, pObj );
338 }
339
340 /**Function*************************************************************
341
342 Synopsis [Updates the solver clause database.]
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Ssw_CnfNodeAddToSolver(Ssw_Sat_t * p,Aig_Obj_t * pObj)351 void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
352 {
353 Vec_Ptr_t * vFrontier;
354 Aig_Obj_t * pNode, * pFanin;
355 int i, k, fUseMuxes = 1;
356 // quit if CNF is ready
357 if ( Ssw_ObjSatNum(p,pObj) )
358 return;
359 // start the frontier
360 vFrontier = Vec_PtrAlloc( 100 );
361 Ssw_ObjAddToFrontier( p, pObj, vFrontier );
362 // explore nodes in the frontier
363 Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
364 {
365 // create the supergate
366 assert( Ssw_ObjSatNum(p,pNode) );
367 if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
368 {
369 Vec_PtrClear( p->vFanins );
370 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
371 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
372 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
373 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
374 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
375 Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
376 Ssw_AddClausesMux( p, pNode );
377 }
378 else
379 {
380 Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
381 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
382 Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
383 Ssw_AddClausesSuper( p, pNode, p->vFanins );
384 }
385 assert( Vec_PtrSize(p->vFanins) > 1 );
386 }
387 Vec_PtrFree( vFrontier );
388 }
389
390
391 /**Function*************************************************************
392
393 Synopsis [Copy pattern from the solver into the internal storage.]
394
395 Description []
396
397 SideEffects []
398
399 SeeAlso []
400
401 ***********************************************************************/
Ssw_CnfGetNodeValue(Ssw_Sat_t * p,Aig_Obj_t * pObj)402 int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
403 {
404 int Value0, Value1, nVarNum;
405 assert( !Aig_IsComplement(pObj) );
406 nVarNum = Ssw_ObjSatNum( p, pObj );
407 if ( nVarNum > 0 )
408 return sat_solver_var_value( p->pSat, nVarNum );
409 // if ( pObj->fMarkA == 1 )
410 // return 0;
411 if ( Aig_ObjIsCi(pObj) )
412 return 0;
413 assert( Aig_ObjIsNode(pObj) );
414 Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
415 Value0 ^= Aig_ObjFaninC0(pObj);
416 Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
417 Value1 ^= Aig_ObjFaninC1(pObj);
418 return Value0 & Value1;
419 }
420
421
422 ////////////////////////////////////////////////////////////////////////
423 /// END OF FILE ///
424 ////////////////////////////////////////////////////////////////////////
425
426
427 ABC_NAMESPACE_IMPL_END
428