abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
dchCnf.c File Reference
#include "dchInt.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Dch_AddClausesMux (Dch_Man_t *p, Aig_Obj_t *pNode)
 DECLARATIONS ///. More...
 
void Dch_AddClausesSuper (Dch_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
 
void Dch_CollectSuper_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
 
void Dch_CollectSuper (Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
 
void Dch_ObjAddToFrontier (Dch_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
 
void Dch_CnfNodeAddToSolver (Dch_Man_t *p, Aig_Obj_t *pObj)
 

Function Documentation

ABC_NAMESPACE_IMPL_START void Dch_AddClausesMux ( Dch_Man_t *  p,
Aig_Obj_t *  pNode 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [dchCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Computation of CNF.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:
dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchCnf.c.

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 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
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
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
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
Aig_Obj_t_
Definition: aig.h:69
Dch_Man_t_::pSat
sat_solver * pSat
Definition: dchInt.h:63
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
assert
#define assert(ex)
Definition: util_old.h:213
Dch_Man_t_::pPars
Dch_Pars_t * pPars
Definition: dchInt.h:54
Dch_ObjSatNum
static int Dch_ObjSatNum(Dch_Man_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: dchInt.h:102
void Dch_AddClausesSuper ( Dch_Man_t *  p,
Aig_Obj_t *  pNode,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file dchCnf.c.

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 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
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
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
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
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Aig_Obj_t_
Definition: aig.h:69
Dch_Man_t_::pSat
sat_solver * pSat
Definition: dchInt.h:63
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
assert
#define assert(ex)
Definition: util_old.h:213
Dch_Man_t_::pPars
Dch_Pars_t * pPars
Definition: dchInt.h:54
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Dch_ObjSatNum
static int Dch_ObjSatNum(Dch_Man_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: dchInt.h:102
void Dch_CnfNodeAddToSolver ( Dch_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file dchCnf.c.

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 }
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
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
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
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
else
else
Definition: sparse_int.h:55
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
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
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
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
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
void Dch_CollectSuper ( Aig_Obj_t *  pObj,
int  fUseMuxes,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file dchCnf.c.

244 {
245  assert( !Aig_IsComplement(pObj) );
246  assert( !Aig_ObjIsCi(pObj) );
247  Vec_PtrClear( vSuper );
248  Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
249 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Dch_CollectSuper_rec
void Dch_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: dchCnf.c:217
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Dch_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 217 of file dchCnf.c.

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 }
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Dch_CollectSuper_rec
void Dch_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: dchCnf.c:217
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Dch_ObjAddToFrontier ( Dch_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vFrontier 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file dchCnf.c.

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 }
Dch_Man_t_::nSatVars
int nSatVars
Definition: dchInt.h:64
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Dch_Man_t_::vUsedNodes
Vec_Ptr_t * vUsedNodes
Definition: dchInt.h:66
assert
#define assert(ex)
Definition: util_old.h:213
Dch_ObjSetSatNum
static void Dch_ObjSetSatNum(Dch_Man_t *p, Aig_Obj_t *pObj, int Num)
Definition: dchInt.h:103
Dch_ObjSatNum
static int Dch_ObjSatNum(Dch_Man_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: dchInt.h:102