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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux (Fra_Man_t *p, Aig_Obj_t *pNode)
 DECLARATIONS ///. More...
 
void Fra_AddClausesSuper (Fra_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
 
void Fra_CollectSuper_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
 
Vec_Ptr_t * Fra_CollectSuper (Aig_Obj_t *pObj, int fUseMuxes)
 
void Fra_ObjAddToFrontier (Fra_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
 
void Fra_CnfNodeAddToSolver (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
 

Function Documentation

ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux ( Fra_Man_t *  p,
Aig_Obj_t *  pNode 
)

DECLARATIONS ///.

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

FileName [fraCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraCnf.c.

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 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
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
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
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
void Fra_AddClausesSuper ( Fra_Man_t *  p,
Aig_Obj_t *  pNode,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file fraCnf.c.

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 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
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
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
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Fra_CnfNodeAddToSolver ( Fra_Man_t *  p,
Aig_Obj_t *  pOld,
Aig_Obj_t *  pNew 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file fraCnf.c.

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 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
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
Fra_ObjSetFaninVec
static void Fra_ObjSetFaninVec(Aig_Obj_t *pObj, Vec_Ptr_t *vFanins)
Definition: fra.h:264
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
Fra_ObjAddToFrontier
void Fra_ObjAddToFrontier(Fra_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition: fraCnf.c:213
Fra_AddClausesSuper
void Fra_AddClausesSuper(Fra_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition: fraCnf.c:129
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Fra_CollectSuper
Vec_Ptr_t * Fra_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes)
Definition: fraCnf.c:192
Fra_AddClausesMux
ABC_NAMESPACE_IMPL_START void Fra_AddClausesMux(Fra_Man_t *p, Aig_Obj_t *pNode)
DECLARATIONS ///.
Definition: fraCnf.c:46
Fra_ObjFaninVec
static Vec_Ptr_t * Fra_ObjFaninVec(Aig_Obj_t *pObj)
Definition: fra.h:263
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Vec_Ptr_t* Fra_CollectSuper ( Aig_Obj_t *  pObj,
int  fUseMuxes 
)

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file fraCnf.c.

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 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Fra_CollectSuper_rec
void Fra_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: fraCnf.c:167
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Fra_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 167 of file fraCnf.c.

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 }
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
Fra_CollectSuper_rec
void Fra_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: fraCnf.c:167
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 Fra_ObjAddToFrontier ( Fra_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vFrontier 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file fraCnf.c.

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 }
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
Fra_Man_t_::nSatVars
int nSatVars
Definition: fra.h:211
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Fra_ObjSetSatNum
static void Fra_ObjSetSatNum(Aig_Obj_t *pObj, int Num)
Definition: fra.h:267
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
Fra_ObjFaninVec
static Vec_Ptr_t * Fra_ObjFaninVec(Aig_Obj_t *pObj)
Definition: fra.h:263