ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Macros | Typedefs | Functions
saigGlaPba2.c File Reference
#include "saig.h"
#include "sat/bsat/satSolver2.h"
Include dependency graph for saigGlaPba2.c:

Go to the source code of this file.

Classes

struct  Aig_Gla3Man_t_
 

Macros

#define ABC_CPS   1000
 FUNCTION DEFINITIONS ///.
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Aig_Gla3Man_t_ Aig_Gla3Man_t
 DECLARATIONS ///.
 

Functions

int Aig_Gla3FetchVar (Aig_Gla3Man_t *p, Aig_Obj_t *pObj, int k)
 
void Aig_Gla3AssignVars_rec (Aig_Gla3Man_t *p, Aig_Obj_t *pObj, int f)
 
int Aig_Gla3CreateSatSolver (Aig_Gla3Man_t *p)
 
Aig_Gla3Man_t * Aig_Gla3ManStart (Aig_Man_t *pAig, int nStart, int nFramesMax, int fVerbose)
 
void Aig_Gla3ManStop (Aig_Gla3Man_t *p)
 
Vec_Int_t * Aig_Gla3ManUnsatCore (sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue)
 
Vec_Int_t * Aig_Gla3ManCollect (Aig_Gla3Man_t *p, Vec_Int_t *vCore)
 
Vec_Int_t * Aig_Gla3ManPerform (Aig_Man_t *pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose)
 

Macro Definition Documentation

◆ ABC_CPS

#define ABC_CPS   1000

FUNCTION DEFINITIONS ///.

Definition at line 59 of file saigGlaPba2.c.

Typedef Documentation

◆ Aig_Gla3Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Aig_Gla3Man_t_ Aig_Gla3Man_t

DECLARATIONS ///.

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

FileName [saigGlaPba.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Gate level abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file saigGlaPba2.c.

Function Documentation

◆ Aig_Gla3AssignVars_rec()

void Aig_Gla3AssignVars_rec ( Aig_Gla3Man_t * p,
Aig_Obj_t * pObj,
int f )

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

Synopsis [Assigns variables to the AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file saigGlaPba2.c.

189{
190 int nVars = Vec_IntSize(p->vVar2Inf);
191 Aig_Gla3FetchVar( p, pObj, f );
192 if ( nVars == Vec_IntSize(p->vVar2Inf) )
193 return;
194 if ( Aig_ObjIsConst1(pObj) )
195 return;
196 if ( Saig_ObjIsPo( p->pAig, pObj ) )
197 {
198 Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
199 return;
200 }
201 if ( Aig_ObjIsCi( pObj ) )
202 {
203 if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
204 Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
205 return;
206 }
207 assert( Aig_ObjIsNode(pObj) );
208 Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
209 Aig_Gla3AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
210}
p
Cube * p
Definition exorList.c:222
Aig_Gla3FetchVar
int Aig_Gla3FetchVar(Aig_Gla3Man_t *p, Aig_Obj_t *pObj, int k)
Definition saigGlaPba2.c:154
Aig_Gla3AssignVars_rec
void Aig_Gla3AssignVars_rec(Aig_Gla3Man_t *p, Aig_Obj_t *pObj, int f)
Definition saigGlaPba2.c:188
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:

◆ Aig_Gla3CreateSatSolver()

int Aig_Gla3CreateSatSolver ( Aig_Gla3Man_t * p)

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

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file saigGlaPba2.c.

224{
225 Vec_Int_t * vPoLits;
226 Aig_Obj_t * pObj;
227 int i, f, ObjId, nVars, RetValue = 1;
228
229 // assign variables
230 for ( f = p->nFramesMax - 1; f >= 0; f-- )
231 Aig_Gla3AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f );
232
233 // create SAT solver
234 p->pSat = sat_solver2_new();
235 sat_solver2_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
236
237 // add clauses
238 nVars = Vec_IntSize( p->vVar2Inf );
239 Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
240 {
241 if ( ObjId == -1 )
242 continue;
243 pObj = Aig_ManObj( p->pAig, ObjId );
244 if ( Aig_ObjIsNode(pObj) )
245 {
246 Aig_Gla3AddNode( p->pSat, Aig_Gla3FetchVar(p, pObj, f),
247 Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f),
248 Aig_Gla3FetchVar(p, Aig_ObjFanin1(pObj), f),
249 Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
250 Vec_IntPush( p->vCla2Obj, ObjId );
251 Vec_IntPush( p->vCla2Obj, ObjId );
252 Vec_IntPush( p->vCla2Obj, ObjId );
253
254 Vec_IntPush( p->vCla2Fra, f );
255 Vec_IntPush( p->vCla2Fra, f );
256 Vec_IntPush( p->vCla2Fra, f );
257 }
258 else if ( Saig_ObjIsLo(p->pAig, pObj) )
259 {
260 if ( f == 0 )
261 {
262 Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 1 );
263 Vec_IntPush( p->vCla2Obj, ObjId );
264
265 Vec_IntPush( p->vCla2Fra, f );
266 }
267 else
268 {
269 Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
270 Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f),
271 Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObjLi), f-1),
272 Aig_ObjFaninC0(pObjLi) );
273 Vec_IntPush( p->vCla2Obj, ObjId );
274 Vec_IntPush( p->vCla2Obj, ObjId );
275
276 Vec_IntPush( p->vCla2Fra, f );
277 Vec_IntPush( p->vCla2Fra, f );
278 }
279 }
280 else if ( Saig_ObjIsPo(p->pAig, pObj) )
281 {
282 Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f),
283 Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f),
284 Aig_ObjFaninC0(pObj) );
285 Vec_IntPush( p->vCla2Obj, ObjId );
286 Vec_IntPush( p->vCla2Obj, ObjId );
287
288 Vec_IntPush( p->vCla2Fra, f );
289 Vec_IntPush( p->vCla2Fra, f );
290 }
291 else if ( Aig_ObjIsConst1(pObj) )
292 {
293 Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 0 );
294 Vec_IntPush( p->vCla2Obj, ObjId );
295
296 Vec_IntPush( p->vCla2Fra, f );
297 }
298 else assert( Saig_ObjIsPi(p->pAig, pObj) );
299 }
300
301 // add output clause
302 vPoLits = Vec_IntAlloc( p->nFramesMax );
303 for ( f = p->nStart; f < p->nFramesMax; f++ )
304 Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
305 sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits), 0 );
306 Vec_IntFree( vPoLits );
307 Vec_IntPush( p->vCla2Obj, 0 );
308 Vec_IntPush( p->vCla2Fra, 0 );
309 assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
310 assert( nVars == Vec_IntSize(p->vVar2Inf) );
311 assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses+1 );
312 if ( p->fVerbose )
313 printf( "The resulting SAT problem contains %d variables and %d clauses.\n",
314 p->pSat->size, p->pSat->stats.clauses );
315 return RetValue;
316}
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition satSolver2.c:1109
sat_solver2_setnvars
void sat_solver2_setnvars(sat_solver2 *s, int n)
Definition satSolver2.c:1170
sat_solver2_addclause
int sat_solver2_addclause(sat_solver2 *s, lit *begin, lit *end, int Id)
Definition satSolver2.c:1287
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_Gla3FetchVar()

int Aig_Gla3FetchVar ( Aig_Gla3Man_t * p,
Aig_Obj_t * pObj,
int k )

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

Synopsis [Finds existing SAT variable or creates a new one.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file saigGlaPba2.c.

155{
156 int i, iVecId, iSatVar;
157 assert( k < p->nFramesMax );
158 iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
159 if ( iVecId == 0 )
160 {
161 iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
162 for ( i = 0; i < p->nFramesMax; i++ )
163 Vec_IntPush( p->vVec2Var, 0 );
164 Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
165 }
166 iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
167 if ( iSatVar == 0 )
168 {
169 iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
170 Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
171 Vec_IntPush( p->vVar2Inf, k );
172 Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
173 }
174 return iSatVar;
175}
Here is the caller graph for this function:

◆ Aig_Gla3ManCollect()

Vec_Int_t * Aig_Gla3ManCollect ( Aig_Gla3Man_t * p,
Vec_Int_t * vCore )

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

Synopsis [Collects abstracted objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file saigGlaPba2.c.

444{
445 Vec_Int_t * vResult;
446 Aig_Obj_t * pObj;
447 int i, ClaId, iVecId;
448// p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );
449
450 vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
451 Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
452 Vec_IntForEachEntry( vCore, ClaId, i )
453 {
454 pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
455 if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) )
456 continue;
457 assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
458 Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
459 if ( p->vVec2Use )
460 {
461 iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
462 Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
463 }
464 }
465 // count the number of objects in each frame
466 if ( p->vVec2Use )
467 {
468 Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
469 int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
470 for ( f = 0; f < p->nFramesMax; f++ )
471 for ( v = 0; v < nVecIds; v++ )
472 if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
473 Vec_IntAddToEntry( vCounts, f, 1 );
474 Vec_IntForEachEntry( vCounts, Entry, f )
475 printf( "%d ", Entry );
476 printf( "\n" );
477 Vec_IntFree( vCounts );
478 }
479 return vResult;
480}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Aig_Gla3ManPerform()

Vec_Int_t * Aig_Gla3ManPerform ( Aig_Man_t * pAig,
int nStart,
int nFramesMax,
int nConfLimit,
int TimeLimit,
int fSkipRand,
int fVerbose )

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

Synopsis [Performs gate-level localization abstraction.]

Description [Returns array of objects included in the abstraction. This array may contain only const1, flop outputs, and internal nodes, that is, objects that should have clauses added to the SAT solver.]

SideEffects []

SeeAlso []

Definition at line 495 of file saigGlaPba2.c.

496{
497 Aig_Gla3Man_t * p;
498 Vec_Int_t * vCore, * vResult;
499 clock_t clk, clk2 = clock();
500 assert( Saig_ManPoNum(pAig) == 1 );
501
502 if ( fVerbose )
503 {
504 if ( TimeLimit )
505 printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
506 else
507 printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
508 }
509
510 // start the solver
511 clk = clock();
512 p = Aig_Gla3ManStart( pAig, nStart, nFramesMax, fVerbose );
513 if ( !Aig_Gla3CreateSatSolver( p ) )
514 {
515 printf( "Error! SAT solver became UNSAT.\n" );
516 Aig_Gla3ManStop( p );
517 return NULL;
518 }
519 p->pSat->fNotUseRandom = fSkipRand;
520 p->timePre += clock() - clk;
521
522 // set runtime limit
523 if ( TimeLimit )
524 sat_solver2_set_runtime_limit( p->pSat, TimeLimit * CLOCKS_PER_SEC + clock() );
525
526 // compute UNSAT core
527 clk = clock();
528 vCore = Aig_Gla3ManUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
529 if ( vCore == NULL )
530 {
531 Aig_Gla3ManStop( p );
532 return NULL;
533 }
534 p->timeSat += clock() - clk;
535 p->timeTotal += clock() - clk2;
536
537 // print stats
538 if ( fVerbose )
539 {
540 ABC_PRTP( "Pre ", p->timePre, p->timeTotal );
541 ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
542 ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
543 }
544
545 // prepare return value
546 vResult = Aig_Gla3ManCollect( p, vCore );
547 Vec_IntFree( vCore );
548 Aig_Gla3ManStop( p );
549 return vResult;
550}
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Aig_Gla3Man_t
typedefABC_NAMESPACE_IMPL_START struct Aig_Gla3Man_t_ Aig_Gla3Man_t
DECLARATIONS ///.
Definition saigGlaPba2.c:31
Aig_Gla3ManStart
Aig_Gla3Man_t * Aig_Gla3ManStart(Aig_Man_t *pAig, int nStart, int nFramesMax, int fVerbose)
Definition saigGlaPba2.c:329
Aig_Gla3ManCollect
Vec_Int_t * Aig_Gla3ManCollect(Aig_Gla3Man_t *p, Vec_Int_t *vCore)
Definition saigGlaPba2.c:443
Aig_Gla3CreateSatSolver
int Aig_Gla3CreateSatSolver(Aig_Gla3Man_t *p)
Definition saigGlaPba2.c:223
Aig_Gla3ManStop
void Aig_Gla3ManStop(Aig_Gla3Man_t *p)
Definition saigGlaPba2.c:367
Aig_Gla3ManUnsatCore
Vec_Int_t * Aig_Gla3ManUnsatCore(sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue)
Definition saigGlaPba2.c:393
Here is the call graph for this function:

◆ Aig_Gla3ManStart()

Aig_Gla3Man_t * Aig_Gla3ManStart ( Aig_Man_t * pAig,
int nStart,
int nFramesMax,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file saigGlaPba2.c.

330{
331 Aig_Gla3Man_t * p;
332 int i;
333
334 p = ABC_CALLOC( Aig_Gla3Man_t, 1 );
335 p->pAig = pAig;
336
337 p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
338 p->vVec2Var = Vec_IntAlloc( 1 << 20 );
339 p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
340 p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Obj, -1 );
341 p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Fra, -1 );
342
343 // skip first vector ID
344 p->nStart = nStart;
345 p->nFramesMax = nFramesMax;
346 p->fVerbose = fVerbose;
347 for ( i = 0; i < p->nFramesMax; i++ )
348 Vec_IntPush( p->vVec2Var, -1 );
349
350 // skip first SAT variable
351 Vec_IntPush( p->vVar2Inf, -1 );
352 Vec_IntPush( p->vVar2Inf, -1 );
353 return p;
354}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Here is the caller graph for this function:

◆ Aig_Gla3ManStop()

void Aig_Gla3ManStop ( Aig_Gla3Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file saigGlaPba2.c.

368{
369 Vec_IntFreeP( &p->vObj2Vec );
370 Vec_IntFreeP( &p->vVec2Var );
371 Vec_IntFreeP( &p->vVar2Inf );
372 Vec_IntFreeP( &p->vCla2Obj );
373 Vec_IntFreeP( &p->vCla2Fra );
374 Vec_IntFreeP( &p->vVec2Use );
375
376 if ( p->pSat )
377 sat_solver2_delete( p->pSat );
378 ABC_FREE( p );
379}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition satSolver2.c:1225
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_Gla3ManUnsatCore()

Vec_Int_t * Aig_Gla3ManUnsatCore ( sat_solver2 * pSat,
int nConfMax,
int fVerbose,
int * piRetValue )

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

Synopsis [Finds the set of clauses involved in the UNSAT core.]

Description []

SideEffects []

SeeAlso []

Definition at line 393 of file saigGlaPba2.c.

394{
395 Vec_Int_t * vCore;
396 int RetValue;
397 clock_t clk = clock();
398 if ( piRetValue )
399 *piRetValue = -1;
400 // solve the problem
401 RetValue = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
402 if ( RetValue == l_Undef )
403 {
404 printf( "Conflict limit is reached.\n" );
405 return NULL;
406 }
407 if ( RetValue == l_True )
408 {
409 printf( "The BMC problem is SAT.\n" );
410 if ( piRetValue )
411 *piRetValue = 0;
412 return NULL;
413 }
414 if ( fVerbose )
415 {
416 printf( "SAT solver returned UNSAT after %7d conflicts. ", (int)pSat->stats.conflicts );
417 Abc_PrintTime( 1, "Time", clock() - clk );
418 }
419 assert( RetValue == l_False );
420
421 // derive the UNSAT core
422 clk = clock();
423 vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
424 if ( fVerbose )
425 {
426 printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
427 Abc_PrintTime( 1, "Time", clock() - clk );
428 }
429 return vCore;
430}
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver2_solve
int sat_solver2_solve(sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition satSolver2.c:1835
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition satSolver2.c:1985
sat_solver2_t::stats
stats_t stats
Definition satSolver2.h:172
stats_t::conflicts
ABC_INT64_T conflicts
Definition satVec.h:156
Here is the call graph for this function:
Here is the caller graph for this function: