abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dchCnf.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dchCnf.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Choice computation for tech-mapping.]
8 
9  Synopsis [Computation of CNF.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 29, 2008.]
16 
17  Revision [$Id: dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "dchInt.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 [Addes clauses to the solver.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
46 {
47  Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
48  int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
49 
50  assert( !Aig_IsComplement( pNode ) );
51  assert( Aig_ObjIsMuxType( pNode ) );
52  // get nodes (I = if, T = then, E = else)
53  pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
54  // get the variable numbers
55  VarF = Dch_ObjSatNum(p,pNode);
56  VarI = Dch_ObjSatNum(p,pNodeI);
57  VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT));
58  VarE = Dch_ObjSatNum(p,Aig_Regular(pNodeE));
59  // get the complementation flags
60  fCompT = Aig_IsComplement(pNodeT);
61  fCompE = Aig_IsComplement(pNodeE);
62 
63  // f = ITE(i, t, e)
64 
65  // i' + t' + f
66  // i' + t + f'
67  // i + e' + f
68  // i + e + f'
69 
70  // create four clauses
71  pLits[0] = toLitCond(VarI, 1);
72  pLits[1] = toLitCond(VarT, 1^fCompT);
73  pLits[2] = toLitCond(VarF, 0);
74  if ( p->pPars->fPolarFlip )
75  {
76  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
77  if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
78  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
79  }
80  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
81  assert( RetValue );
82  pLits[0] = toLitCond(VarI, 1);
83  pLits[1] = toLitCond(VarT, 0^fCompT);
84  pLits[2] = toLitCond(VarF, 1);
85  if ( p->pPars->fPolarFlip )
86  {
87  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
88  if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
89  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
90  }
91  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
92  assert( RetValue );
93  pLits[0] = toLitCond(VarI, 0);
94  pLits[1] = toLitCond(VarE, 1^fCompE);
95  pLits[2] = toLitCond(VarF, 0);
96  if ( p->pPars->fPolarFlip )
97  {
98  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
99  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
100  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
101  }
102  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
103  assert( RetValue );
104  pLits[0] = toLitCond(VarI, 0);
105  pLits[1] = toLitCond(VarE, 0^fCompE);
106  pLits[2] = toLitCond(VarF, 1);
107  if ( p->pPars->fPolarFlip )
108  {
109  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
110  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
111  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
112  }
113  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
114  assert( RetValue );
115 
116  // two additional clauses
117  // t' & e' -> f'
118  // t & e -> f
119 
120  // t + e + f'
121  // t' + e' + f
122 
123  if ( VarT == VarE )
124  {
125 // assert( fCompT == !fCompE );
126  return;
127  }
128 
129  pLits[0] = toLitCond(VarT, 0^fCompT);
130  pLits[1] = toLitCond(VarE, 0^fCompE);
131  pLits[2] = toLitCond(VarF, 1);
132  if ( p->pPars->fPolarFlip )
133  {
134  if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
135  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
136  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
137  }
138  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
139  assert( RetValue );
140  pLits[0] = toLitCond(VarT, 1^fCompT);
141  pLits[1] = toLitCond(VarE, 1^fCompE);
142  pLits[2] = toLitCond(VarF, 0);
143  if ( p->pPars->fPolarFlip )
144  {
145  if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
146  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
147  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
148  }
149  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
150  assert( RetValue );
151 }
152 
153 /**Function*************************************************************
154 
155  Synopsis [Addes clauses to the solver.]
156 
157  Description []
158 
159  SideEffects []
160 
161  SeeAlso []
162 
163 ***********************************************************************/
164 void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
165 {
166  Aig_Obj_t * pFanin;
167  int * pLits, nLits, RetValue, i;
168  assert( !Aig_IsComplement(pNode) );
169  assert( Aig_ObjIsNode( pNode ) );
170  // create storage for literals
171  nLits = Vec_PtrSize(vSuper) + 1;
172  pLits = ABC_ALLOC( int, nLits );
173  // suppose AND-gate is A & B = C
174  // add !A => !C or A + !C
175  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
176  {
177  pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
178  pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1);
179  if ( p->pPars->fPolarFlip )
180  {
181  if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
182  if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
183  }
184  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
185  assert( RetValue );
186  }
187  // add A & B => C or !A + !B + C
188  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
189  {
190  pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
191  if ( p->pPars->fPolarFlip )
192  {
193  if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
194  }
195  }
196  pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0);
197  if ( p->pPars->fPolarFlip )
198  {
199  if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
200  }
201  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
202  assert( RetValue );
203  ABC_FREE( pLits );
204 }
205 
206 /**Function*************************************************************
207 
208  Synopsis [Collects the supergate.]
209 
210  Description []
211 
212  SideEffects []
213 
214  SeeAlso []
215 
216 ***********************************************************************/
217 void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
218 {
219  // if the new node is complemented or a PI, another gate begins
220  if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
221  (!fFirst && Aig_ObjRefs(pObj) > 1) ||
222  (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
223  {
224  Vec_PtrPushUnique( vSuper, pObj );
225  return;
226  }
227  // go through the branches
228  Dch_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
229  Dch_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
230 }
231 
232 /**Function*************************************************************
233 
234  Synopsis [Collects the supergate.]
235 
236  Description []
237 
238  SideEffects []
239 
240  SeeAlso []
241 
242 ***********************************************************************/
243 void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
244 {
245  assert( !Aig_IsComplement(pObj) );
246  assert( !Aig_ObjIsCi(pObj) );
247  Vec_PtrClear( vSuper );
248  Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
249 }
250 
251 /**Function*************************************************************
252 
253  Synopsis [Updates the solver clause database.]
254 
255  Description []
256 
257  SideEffects []
258 
259  SeeAlso []
260 
261 ***********************************************************************/
262 void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
263 {
264  assert( !Aig_IsComplement(pObj) );
265  if ( Dch_ObjSatNum(p,pObj) )
266  return;
267  assert( Dch_ObjSatNum(p,pObj) == 0 );
268  if ( Aig_ObjIsConst1(pObj) )
269  return;
270  Vec_PtrPush( p->vUsedNodes, pObj );
271  Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
272  if ( Aig_ObjIsNode(pObj) )
273  Vec_PtrPush( vFrontier, pObj );
274 }
275 
276 /**Function*************************************************************
277 
278  Synopsis [Updates the solver clause database.]
279 
280  Description []
281 
282  SideEffects []
283 
284  SeeAlso []
285 
286 ***********************************************************************/
287 void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj )
288 {
289  Vec_Ptr_t * vFrontier;
290  Aig_Obj_t * pNode, * pFanin;
291  int i, k, fUseMuxes = 1;
292  // quit if CNF is ready
293  if ( Dch_ObjSatNum(p,pObj) )
294  return;
295  // start the frontier
296  vFrontier = Vec_PtrAlloc( 100 );
297  Dch_ObjAddToFrontier( p, pObj, vFrontier );
298  // explore nodes in the frontier
299  Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
300  {
301  // create the supergate
302  assert( Dch_ObjSatNum(p,pNode) );
303  if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
304  {
305  Vec_PtrClear( p->vFanins );
306  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
307  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
308  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
309  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
310  Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
311  Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
312  Dch_AddClausesMux( p, pNode );
313  }
314  else
315  {
316  Dch_CollectSuper( pNode, fUseMuxes, p->vFanins );
317  Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
318  Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
319  Dch_AddClausesSuper( p, pNode, p->vFanins );
320  }
321  assert( Vec_PtrSize(p->vFanins) > 1 );
322  }
323  Vec_PtrFree( vFrontier );
324 }
325 
326 
327 
328 ////////////////////////////////////////////////////////////////////////
329 /// END OF FILE ///
330 ////////////////////////////////////////////////////////////////////////
331 
332 
333 ABC_NAMESPACE_IMPL_END
334 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Dch_ObjAddToFrontier
void Dch_ObjAddToFrontier(Dch_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition: dchCnf.c:262
Dch_Man_t_::nSatVars
int nSatVars
Definition: dchInt.h:64
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Dch_CollectSuper
void Dch_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition: dchCnf.c:243
Dch_Man_t_
Definition: dchInt.h:51
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition: aigUtil.c:387
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Dch_AddClausesSuper
void Dch_AddClausesSuper(Dch_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition: dchCnf.c:164
Aig_Obj_t_
Definition: aig.h:69
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Dch_Man_t_::vUsedNodes
Vec_Ptr_t * vUsedNodes
Definition: dchInt.h:66
Dch_Man_t_::pSat
sat_solver * pSat
Definition: dchInt.h:63
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Dch_CollectSuper_rec
void Dch_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: dchCnf.c:217
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Dch_Man_t_::vFanins
Vec_Ptr_t * vFanins
Definition: dchInt.h:69
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Dch_Man_t_::pPars
Dch_Pars_t * pPars
Definition: dchInt.h:54
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Dch_CnfNodeAddToSolver
void Dch_CnfNodeAddToSolver(Dch_Man_t *p, Aig_Obj_t *pObj)
Definition: dchCnf.c:287
Dch_ObjSetSatNum
static void Dch_ObjSetSatNum(Dch_Man_t *p, Aig_Obj_t *pObj, int Num)
Definition: dchInt.h:103
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Dch_AddClausesMux
ABC_NAMESPACE_IMPL_START void Dch_AddClausesMux(Dch_Man_t *p, Aig_Obj_t *pNode)
DECLARATIONS ///.
Definition: dchCnf.c:45
Dch_ObjSatNum
static int Dch_ObjSatNum(Dch_Man_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: dchInt.h:102
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223