ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
int2Int.h File Reference
#include "aig/gia/gia.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"
#include "int2.h"
Include dependency graph for int2Int.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Int2_Man_t_
 DECLARATIONS ///. More...
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_ Int2_Man_t
 INCLUDES ///.
 

Functions

int Int2_ManCheckInit (Gia_Man_t *p)
 MACRO DEFINITIONS ///.
 
Gia_Man_t * Int2_ManDupInit (Gia_Man_t *p, int fVerbose)
 DECLARATIONS ///.
 
sat_solver * Int2_ManSetupBmcSolver (Gia_Man_t *p, int nFrames)
 
void Int2_ManCreateFrames (Int2_Man_t *p, int iFrame, Vec_Int_t *vPrefCos)
 
int Int2_ManCheckBmc (Int2_Man_t *p, Vec_Int_t *vCube)
 
Vec_Int_t * Int2_ManRefineCube (Gia_Man_t *p, Vec_Int_t *vAssign, Vec_Int_t *vPrio)
 
Gia_Man_t * Int2_ManProbToGia (Gia_Man_t *p, Vec_Int_t *vSop)
 

Typedef Documentation

◆ Int2_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_ Int2_Man_t

INCLUDES ///.

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

FileName [int2Int.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 1, 2013.]

Revision [

Id
int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 45 of file int2Int.h.

Function Documentation

◆ Int2_ManCheckBmc()

int Int2_ManCheckBmc ( Int2_Man_t * p,
Vec_Int_t * vCube )
extern

Definition at line 318 of file int2Bmc.c.

319{
320 int status;
321 if ( vCube == NULL )
322 {
323 Gia_Obj_t * pObj;
324 int i, iLit;
325 Gia_ManForEachPo( p->pGia, pObj, i )
326 {
327 iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
328 if ( iLit == 0 )
329 continue;
330 if ( iLit == 1 )
331 return 0;
332 status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
333 if ( status == l_False )
334 continue;
335 if ( status == l_True )
336 return 0;
337 return -1;
338 }
339 return 1;
340 }
341 status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
342 if ( status == l_False )
343 return 1;
344 if ( status == l_True )
345 return 0;
346 return -1;
347}
l_True
#define l_True
Definition bmcBmcS.c:35
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Here is the caller graph for this function:

◆ Int2_ManCheckInit()

int Int2_ManCheckInit ( Gia_Man_t * p)
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Returns 1 if AIG has transition into init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file int2Bmc.c.

93{
94 sat_solver * pSat;
95 Cnf_Dat_t * pCnf;
96 Gia_Man_t * pNew;
97 Gia_Obj_t * pObj;
98 Vec_Int_t * vLits;
99 int i, Lit, RetValue = 0;
100 assert( Gia_ManRegNum(p) > 0 );
101 pNew = Jf_ManDeriveCnf( p, 0 );
102 pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
103 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
104 if ( pSat != NULL )
105 {
106 vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
107 Gia_ManForEachRi( pNew, pObj, i )
108 {
109 Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
110 Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
111 Vec_IntPush( vLits, Abc_LitNot(Lit) );
112 }
113 if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
114 RetValue = 1;
115 Vec_IntFree( vLits );
116 sat_solver_delete( pSat );
117 }
118 Cnf_DataFree( pCnf );
119 Gia_ManStop( pNew );
120 return RetValue;
121}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Jf_ManDeriveCnf
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition giaJf.c:1749
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Gia_Man_t_::pData
void * pData
Definition gia.h:198
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Int2_ManCreateFrames()

void Int2_ManCreateFrames ( Int2_Man_t * p,
int iFrame,
Vec_Int_t * vPrefCos )
extern

Definition at line 219 of file int2Bmc.c.

220{
221 Gia_Obj_t * pObj;
222 int i, Entry, iLit;
223 // create storage room for unfolded IDs
224 for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
225 Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
226 assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
227 // create constant 0 node
228 if ( f == 0 )
229 {
230 iLit = 1;
231 Int2_ManWriteFrames( p, iFrame, iObj, 0 );
232 sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
233 }
234 // start the stack
235 Vec_IntClear( p->vStack );
236 Vec_IntForEachEntry( vPrefCos, Entry, i )
237 {
238 pObj = Gia_ManCo( p->pGia, Entry );
239 Vec_IntPush( p->vStack, iFrame );
240 Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
241 }
242 // construct unfolded AIG
243 while ( Vec_IntSize(p->vStack) > 0 )
244 {
245 int iObj = Vec_IntPop(p->vStack);
246 int iFrame = Vec_IntPop(p->vStack);
247 if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
248 continue;
249 pObj = Gia_ManObj( p->pGia, iObj );
250 if ( Gia_ObjIsPi(p->pGia, pObj) )
251 Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
252 else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
253 Int2_ManWriteFrames( p, iFrame, iObj, 0 );
254 else if ( Gia_ObjIsRo(p->pGia, iObj) )
255 {
256 int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
257 int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
258 if ( iLit >= 0 )
259 Int2_ManWriteFrames( p, iFrame, iObj, iLit );
260 else
261 {
262 Vec_IntPush( p->vStack, iFrame );
263 Vec_IntPush( p->vStack, iObj );
264 Vec_IntPush( p->vStack, iFrame-1 );
265 Vec_IntPush( p->vStack, iObjF );
266 }
267 }
268 else if ( Gia_ObjIsCo(pObj) )
269 {
270 int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
271 int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
272 if ( iLit >= 0 )
273 Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
274 else
275 {
276 Vec_IntPush( p->vStack, iFrame );
277 Vec_IntPush( p->vStack, iObj );
278 Vec_IntPush( p->vStack, iFrame );
279 Vec_IntPush( p->vStack, iObjF );
280 }
281 }
282 else if ( Gia_ObjIsAnd(pObj) )
283 {
284 int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
285 int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
286 int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
287 int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
288 if ( iLit0 >= 0 && iLit1 >= 0 )
289 {
290 Entry = Gia_ManObjNum(pFrames);
291 iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
292 Int2_ManWriteFrames( p, iFrame, iObj, iLit );
293 if ( Entry < Gia_ManObjNum(pFrames) )
294 {
295 assert( !Abc_LitIsCompl(iLit) );
296 sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 );
297 }
298 }
299 else
300 {
301 Vec_IntPush( p->vStack, iFrame );
302 Vec_IntPush( p->vStack, iObj );
303 if ( iLit0 < 0 )
304 {
305 Vec_IntPush( p->vStack, iFrame );
306 Vec_IntPush( p->vStack, iObjF0 );
307 }
308 if ( iLit1 < 0 )
309 {
310 Vec_IntPush( p->vStack, iFrame );
311 Vec_IntPush( p->vStack, iObjF1 );
312 }
313 }
314 }
315 else assert( 0 );
316 }
317}
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_and
#define sat_solver_add_and
Definition cecSatG2.c:38
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Int2_ManDupInit()

Gia_Man_t * Int2_ManDupInit ( Gia_Man_t * p,
int fVerbose )
extern

DECLARATIONS ///.

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

FileName [int2Bmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [BMC used inside IMC.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 1, 2013.]

Revision [

Id
int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp

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

Synopsis [Trasnforms AIG to transition into the init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file int2Bmc.c.

47{
48 Gia_Man_t * pNew, * pTemp;
49 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
50 int i, iCtrl;
51 assert( Gia_ManRegNum(p) > 0 );
52 pNew = Gia_ManStart( 10000 );
53 pNew->pName = Abc_UtilStrsav( p->pName );
54 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
55 Gia_ManConst0(p)->Value = 0;
56 Gia_ManForEachCi( p, pObj, i )
57 {
58 if ( i == Gia_ManPiNum(p) )
59 iCtrl = Gia_ManAppendCi( pNew );
60 pObj->Value = Gia_ManAppendCi( pNew );
61 }
62 Gia_ManHashAlloc( pNew );
63 Gia_ManForEachAnd( p, pObj, i )
64 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
65 Gia_ManForEachPo( p, pObj, i )
66 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
67 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
68 Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
69 Gia_ManHashStop( pNew );
70 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
71 // remove dangling
72 pNew = Gia_ManCleanup( pTemp = pNew );
73 if ( fVerbose )
74 printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
75 Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
76 Gia_ManStop( pTemp );
77 return pNew;
78}
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Here is the call graph for this function:

◆ Int2_ManProbToGia()

Gia_Man_t * Int2_ManProbToGia ( Gia_Man_t * p,
Vec_Int_t * vSop )
extern

Definition at line 98 of file int2Util.c.

99{
100 Vec_Int_t * vCoPres, * vNodes;
101 Gia_Man_t * pNew, * pTemp;
102 Gia_Obj_t * pObj;
103 int i, k, Entry, Limit;
104 int Lit, Cube, Sop;
105 assert( Gia_ManPoNum(p) == 1 );
106 // collect COs and ANDs
107 vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) );
108 vNodes = Int2_ManCollectInternal( p, vCoPres );
109 // create new manager
110 pNew = Gia_ManStart( Gia_ManObjNum(p) );
111 pNew->pName = Abc_UtilStrsav( p->pName );
112 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
113 Gia_ManConst0(p)->Value = 0;
114 Gia_ManForEachCi( p, pObj, i )
115 pObj->Value = Gia_ManAppendCi(pNew);
116 Gia_ManHashAlloc( pNew );
117 Gia_ManForEachObjVec( vNodes, p, pObj, i )
118 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
119 Vec_IntForEachEntry( vCoPres, Entry, i )
120 {
121 pObj = Gia_ManCo(p, Entry);
122 pObj->Value = Gia_ObjFanin0Copy( pObj );
123 }
124 // create additional cubes
125 Sop = 0;
126 Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
127 {
128 Cube = 1;
129 for ( k = 0; k < Limit; k++ )
130 {
131 i++;
132 Lit = Vec_IntEntry( vSop, i + k );
133 pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) );
134 Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) );
135 }
136 Sop = Gia_ManHashOr( pNew, Sop, Cube );
137 }
138 Gia_ManAppendCo( pNew, Sop );
139 Gia_ManHashStop( pNew );
140 // cleanup
141 pNew = Gia_ManCleanup( pTemp = pNew );
142 Gia_ManStop( pTemp );
143 return pNew;
144}
Cube
struct cube Cube
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Int2_ManCollectInternal
Vec_Int_t * Int2_ManCollectInternal(Gia_Man_t *p, Vec_Int_t *vCoPres)
Definition int2Util.c:84
Int2_ManComputeCoPres
ABC_NAMESPACE_IMPL_START Vec_Int_t * Int2_ManComputeCoPres(Vec_Int_t *vSop, int nRegs)
DECLARATIONS ///.
Definition int2Util.c:45
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Int2_ManRefineCube()

Vec_Int_t * Int2_ManRefineCube ( Gia_Man_t * p,
Vec_Int_t * vAssign,
Vec_Int_t * vPrio )
extern

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

Synopsis [Computes the reduced set of flop variables.]

Description [Given is a single-output seq AIG manager and an assignment of its CIs. Returned is a subset of flops that justifies the output.]

SideEffects []

SeeAlso []

Definition at line 104 of file int2Refine.c.

105{
106 Vec_Int_t * vSubset;
107 Gia_Obj_t * pObj;
108 int i;
109 // set values and prios
110 assert( Gia_ManRegNum(p) > 0 );
111 assert( Vec_IntSize(vAssign) == Vec_IntSize(vPrio) );
112 Gia_ManConst0(p)->fMark0 = 0;
113 Gia_ManConst0(p)->fMark1 = 0;
114 Gia_ManConst0(p)->Value = ABC_INFINITY;
115 Gia_ManForEachCi( p, pObj, i )
116 {
117 pObj->fMark0 = Vec_IntEntry(vAssign, i);
118 pObj->fMark1 = 0;
119 pObj->Value = Vec_IntEntry(vPrio, i);
120 }
121 Gia_ManForEachAnd( p, pObj, i )
122 {
123 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
124 pObj->fMark1 = 0;
125 if ( pObj->fMark0 == 1 )
126 pObj->Value = Abc_MaxInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
127 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
128 pObj->Value = Abc_MinInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); // choice
129 else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
130 pObj->Value = Gia_ObjFanin0(pObj)->Value;
131 else
132 pObj->Value = Gia_ObjFanin1(pObj)->Value;
133 }
134 pObj = Gia_ManPo( p, 0 );
135 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
136 pObj->fMark1 = 0;
137 pObj->Value = Gia_ObjFanin0(pObj)->Value;
138 assert( pObj->fMark0 == 1 );
139 assert( pObj->Value < ABC_INFINITY );
140 // select subset
141 vSubset = Vec_IntAlloc( 100 );
142 Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSubset );
143 return vSubset;
144}
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Int2_ManJustify_rec
ABC_NAMESPACE_IMPL_START void Int2_ManJustify_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSelect)
DECLARATIONS ///.
Definition int2Refine.c:45
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Int2_ManSetupBmcSolver()

sat_solver * Int2_ManSetupBmcSolver ( Gia_Man_t * p,
int nFrames )
extern

Definition at line 170 of file int2Bmc.c.

171{
172 Gia_Man_t * pFrames, * pTemp;
173 Cnf_Dat_t * pCnf;
174 sat_solver * pSat;
175 // unfold for the given number of timeframes
176 pFrames = Int2_ManFrameInit( p, nFrames, 1 );
177 assert( Gia_ManRegNum(pFrames) == 0 );
178 // derive CNF for the timeframes
179 pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp );
180 pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
181 // create SAT solver
182 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
183 if ( pSat != NULL )
184 {
185 Gia_Obj_t * pObj;
186 int i, nVars = sat_solver_nvars( pSat );
187 sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
188 // add clauses for the POs
189 Gia_ManForEachCo( pFrames, pObj, i )
190 sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
191 }
192 Cnf_DataFree( pCnf );
193 Gia_ManStop( pFrames );
194 return pSat;
195}
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Int2_ManFrameInit
Gia_Man_t * Int2_ManFrameInit(Gia_Man_t *p, int nFrames, int fVerbose)
Definition int2Bmc.c:136
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
Here is the call graph for this function: