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

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 ///.
 
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

◆ Dch_AddClausesMux()

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}
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
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
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:

◆ Dch_AddClausesSuper()

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}
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:

◆ Dch_CnfNodeAddToSolver()

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}
Dch_AddClausesSuper
void Dch_AddClausesSuper(Dch_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition dchCnf.c:164
Dch_ObjAddToFrontier
void Dch_ObjAddToFrontier(Dch_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition dchCnf.c:262
Dch_AddClausesMux
ABC_NAMESPACE_IMPL_START void Dch_AddClausesMux(Dch_Man_t *p, Aig_Obj_t *pNode)
DECLARATIONS ///.
Definition dchCnf.c:45
Dch_CollectSuper
void Dch_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition dchCnf.c:243
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:

◆ Dch_CollectSuper()

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}
Dch_CollectSuper_rec
void Dch_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition dchCnf.c:217
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dch_CollectSuper_rec()

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dch_ObjAddToFrontier()

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}
Here is the caller graph for this function: