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

Go to the source code of this file.

Classes

struct  Vta_Obj_t_
 
struct  Vta_Man_t_
 

Macros

#define VTA_LARGE   0xFFFFFFF
 
#define VTA_VAR0   1
 
#define VTA_VAR1   2
 
#define VTA_VARX   3
 
#define Vta_ManForEachObj(p, pObj, i)
 
#define Vta_ManForEachObjObj(p, pObjVta, pObjGia, i)
 
#define Vta_ManForEachObjObjReverse(p, pObjVta, pObjGia, i)
 
#define Vta_ManForEachObjVec(vVec, p, pObj, i)
 
#define Vta_ManForEachObjVecReverse(vVec, p, pObj, i)
 
#define Vta_ManForEachObjObjVec(vVec, p, pObj, pObjG, i)
 
#define Vta_ManForEachObjObjVecReverse(vVec, p, pObj, pObjG, i)
 

Typedefs

typedef struct Vta_Obj_t_ Vta_Obj_t
 DECLARATIONS ///.
 
typedef struct Vta_Man_t_ Vta_Man_t
 

Functions

void Vga_ManAddClausesOne (Vta_Man_t *p, int iObj, int iFrame)
 
Vec_Ptr_t * Gia_VtaAbsToFrames (Vec_Int_t *vAbs)
 FUNCTION DEFINITIONS ///.
 
Vec_Int_t * Gia_VtaFramesToAbs (Vec_Vec_t *vFrames)
 
int Vec_IntDoubleWidth (Vec_Int_t *p, int nWords)
 
Abc_Cex_t * Vga_ManDeriveCex (Vta_Man_t *p)
 
void Vta_ManUnsatCoreRemap (Vta_Man_t *p, Vec_Int_t *vCore)
 
int Vta_ManComputeDepthIncrease (Vta_Obj_t **pp1, Vta_Obj_t **pp2)
 
int Vta_ManObjIsUsed (Vta_Man_t *p, int iObj)
 
void Vta_ManCollectNodes_rec (Vta_Man_t *p, Vta_Obj_t *pThis, Vec_Int_t *vOrder)
 
Vec_Int_t * Vta_ManCollectNodes (Vta_Man_t *p, int f)
 
void Vta_ManSatVerify (Vta_Man_t *p)
 
void Vta_ManProfileAddition (Vta_Man_t *p, Vec_Int_t *vTermsToAdd)
 
Abc_Cex_t * Vta_ManRefineAbstraction (Vta_Man_t *p, int f)
 
Vta_Man_t * Vga_ManStart (Gia_Man_t *pGia, Abs_Par_t *pPars)
 
void Vga_ManStop (Vta_Man_t *p)
 
Vec_Int_t * Vta_ManUnsatCore (int iLit, sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue, int *pnConfls)
 
int Vta_ManAbsPrintFrame (Vta_Man_t *p, Vec_Int_t *vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose)
 
void Vga_ManLoadSlice (Vta_Man_t *p, Vec_Int_t *vOne, int Lift)
 
void Vga_ManPrintCore (Vta_Man_t *p, Vec_Int_t *vCore, int Lift)
 
void Vga_ManRollBack (Vta_Man_t *p, int nObjOld)
 
void Gia_VtaSendAbsracted (Vta_Man_t *p, int fVerbose)
 
void Gia_VtaSendCancel (Vta_Man_t *p, int fVerbose)
 
void Gia_VtaDumpAbsracted (Vta_Man_t *p, int fVerbose)
 
void Gia_VtaPrintMemory (Vta_Man_t *p)
 
int Gia_VtaPerformInt (Gia_Man_t *pAig, Abs_Par_t *pPars)
 
int Gia_VtaPerform (Gia_Man_t *pAig, Abs_Par_t *pPars)
 

Macro Definition Documentation

◆ VTA_LARGE

#define VTA_LARGE   0xFFFFFFF

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

FileName [absVta.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Variable time-frame abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 27 of file absVta.c.

◆ Vta_ManForEachObj

#define Vta_ManForEachObj ( p,
pObj,
i )
Value:
for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
p
Cube * p
Definition exorList.c:222

Definition at line 107 of file absVta.c.

107#define Vta_ManForEachObj( p, pObj, i ) \
108 for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )

◆ Vta_ManForEachObjObj

#define Vta_ManForEachObjObj ( p,
pObjVta,
pObjGia,
i )
Value:
for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

Definition at line 109 of file absVta.c.

109#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \
110 for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

◆ Vta_ManForEachObjObjReverse

#define Vta_ManForEachObjObjReverse ( p,
pObjVta,
pObjGia,
i )
Value:
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

Definition at line 111 of file absVta.c.

111#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \
112 for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )

◆ Vta_ManForEachObjObjVec

#define Vta_ManForEachObjObjVec ( vVec,
p,
pObj,
pObjG,
i )
Value:
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )

Definition at line 119 of file absVta.c.

119#define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i ) \
120 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )

◆ Vta_ManForEachObjObjVecReverse

#define Vta_ManForEachObjObjVecReverse ( vVec,
p,
pObj,
pObjG,
i )
Value:
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )

Definition at line 121 of file absVta.c.

121#define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i ) \
122 for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )

◆ Vta_ManForEachObjVec

#define Vta_ManForEachObjVec ( vVec,
p,
pObj,
i )
Value:
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )

Definition at line 114 of file absVta.c.

114#define Vta_ManForEachObjVec( vVec, p, pObj, i ) \
115 for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )

◆ Vta_ManForEachObjVecReverse

#define Vta_ManForEachObjVecReverse ( vVec,
p,
pObj,
i )
Value:
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )

Definition at line 116 of file absVta.c.

116#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \
117 for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )

◆ VTA_VAR0

#define VTA_VAR0   1

Definition at line 83 of file absVta.c.

◆ VTA_VAR1

#define VTA_VAR1   2

Definition at line 84 of file absVta.c.

◆ VTA_VARX

#define VTA_VARX   3

Definition at line 85 of file absVta.c.

Typedef Documentation

◆ Vta_Man_t

typedef struct Vta_Man_t_ Vta_Man_t

Definition at line 45 of file absVta.c.

◆ Vta_Obj_t

typedef struct Vta_Obj_t_ Vta_Obj_t

DECLARATIONS ///.

Definition at line 33 of file absVta.c.

Function Documentation

◆ Gia_VtaAbsToFrames()

Vec_Ptr_t * Gia_VtaAbsToFrames ( Vec_Int_t * vAbs)

FUNCTION DEFINITIONS ///.

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

Synopsis [Converting from one array to per-frame arrays.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file absVta.c.

149{
150 Vec_Ptr_t * vFrames;
151 Vec_Int_t * vFrame;
152 int i, k, Entry, iStart, iStop = -1;
153 int nFrames = Vec_IntEntry( vAbs, 0 );
154 assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
155 vFrames = Vec_PtrAlloc( nFrames );
156 for ( i = 0; i < nFrames; i++ )
157 {
158 iStart = Vec_IntEntry( vAbs, i+1 );
159 iStop = Vec_IntEntry( vAbs, i+2 );
160 vFrame = Vec_IntAlloc( iStop - iStart );
161 Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
162 Vec_IntPush( vFrame, Entry );
163 Vec_PtrPush( vFrames, vFrame );
164 }
165 assert( iStop == Vec_IntSize(vAbs) );
166 return vFrames;
167}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition vecInt.h:60
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the caller graph for this function:

◆ Gia_VtaDumpAbsracted()

void Gia_VtaDumpAbsracted ( Vta_Man_t * p,
int fVerbose )

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1424 of file absVta.c.

1425{
1426 char * pFileNameDef = "vabs.aig";
1427 char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
1428 Gia_Man_t * pAbs;
1429 if ( fVerbose )
1430 Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1431 // create obj classes
1432 Vec_IntFreeP( &p->pGia->vObjClasses );
1433 p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1434 // create gate classes
1435 Vec_IntFreeP( &p->pGia->vGateClasses );
1436 p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
1437 Vec_IntFreeP( &p->pGia->vObjClasses );
1438 // create abstrated model
1439 pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
1440 Vec_IntFreeP( &p->pGia->vGateClasses );
1441 // send it out
1442 Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
1443 Gia_ManStop( pAbs );
1444}
Gia_VtaFramesToAbs
Vec_Int_t * Gia_VtaFramesToAbs(Vec_Vec_t *vFrames)
Definition absVta.c:180
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition absDup.c:220
Gia_VtaConvertToGla
Vec_Int_t * Gia_VtaConvertToGla(Gia_Man_t *p, Vec_Int_t *vVta)
Definition absUtil.c:78
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_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_VtaFramesToAbs()

Vec_Int_t * Gia_VtaFramesToAbs ( Vec_Vec_t * vFrames)

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

Synopsis [Converting from per-frame arrays to one integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file absVta.c.

181{
182 Vec_Int_t * vOne, * vAbs;
183 int i, k, Entry, nSize;
184 vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) );
185 Vec_IntPush( vAbs, Vec_VecSize(vFrames) );
186 nSize = Vec_VecSize(vFrames) + 2;
187 Vec_VecForEachLevelInt( vFrames, vOne, i )
188 {
189 Vec_IntPush( vAbs, nSize );
190 nSize += Vec_IntSize( vOne );
191 }
192 Vec_IntPush( vAbs, nSize );
193 assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 );
194 Vec_VecForEachLevelInt( vFrames, vOne, i )
195 Vec_IntForEachEntry( vOne, Entry, k )
196 Vec_IntPush( vAbs, Entry );
197 assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) );
198 return vAbs;
199}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_VecForEachLevelInt
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition vecVec.h:71
Here is the caller graph for this function:

◆ Gia_VtaPerform()

int Gia_VtaPerform ( Gia_Man_t * pAig,
Abs_Par_t * pPars )

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

Synopsis [Collect nodes/flops involved in different timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1743 of file absVta.c.

1744{
1745 int RetValue = -1;
1746 if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
1747 {
1748 int nFramesMaxOld = pPars->nFramesMax;
1749 pPars->nFramesMax = pPars->nFramesStart;
1750 RetValue = Gia_VtaPerformInt( pAig, pPars );
1751 pPars->nFramesMax = nFramesMaxOld;
1752 }
1753 if ( RetValue == 0 )
1754 return RetValue;
1755 return Gia_VtaPerformInt( pAig, pPars );
1756}
Gia_VtaPerformInt
int Gia_VtaPerformInt(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition absVta.c:1492
Gia_Man_t_::vObjClasses
Vec_Int_t * vObjClasses
Definition gia.h:158
Here is the call graph for this function:

◆ Gia_VtaPerformInt()

int Gia_VtaPerformInt ( Gia_Man_t * pAig,
Abs_Par_t * pPars )

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

Synopsis [Collect nodes/flops involved in different timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1492 of file absVta.c.

1493{
1494 Vta_Man_t * p;
1495 Vec_Int_t * vCore;
1496 Abc_Cex_t * pCex = NULL;
1497 int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
1498 abctime clk = Abc_Clock(), clk2;
1499 // preconditions
1500 assert( Gia_ManPoNum(pAig) == 1 );
1501 assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
1502 if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
1503 {
1504 if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
1505 {
1506 printf( "Sequential miter is trivially UNSAT.\n" );
1507 return 1;
1508 }
1509 ABC_FREE( pAig->pCexSeq );
1510 pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
1511 printf( "Sequential miter is trivially SAT.\n" );
1512 return 0;
1513 }
1514
1515 // compute intial abstraction
1516 if ( pAig->vObjClasses == NULL )
1517 {
1518 pAig->vObjClasses = Vec_IntAlloc( 5 );
1519 Vec_IntPush( pAig->vObjClasses, 1 );
1520 Vec_IntPush( pAig->vObjClasses, 3 );
1521 Vec_IntPush( pAig->vObjClasses, 4 );
1522 Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
1523 }
1524 // start the manager
1525 p = Vga_ManStart( pAig, pPars );
1526 // set runtime limit
1527 if ( p->pPars->nTimeOut )
1528 sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1529 // perform initial abstraction
1530 if ( p->pPars->fVerbose )
1531 {
1532 Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
1533 Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n",
1534 pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
1535 Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
1536 pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
1537// Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
1538 Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
1539 }
1540 assert( Vec_PtrSize(p->vFrames) > 0 );
1541 for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
1542 {
1543 int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1544 p->pPars->iFrame = f;
1545 // realloc storage for abstraction marks
1546 if ( f == p->nWords * 32 )
1547 p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
1548
1549 // create bookmark to be used for rollback
1550 nObjOld = p->nObjs;
1551 sat_solver2_bookmark( p->pSat );
1552 Vec_IntClear( p->vAddedNew );
1553
1554 // load new timeframe
1555 Vga_ManAddClausesOne( p, 0, f );
1556 if ( f < Vec_PtrSize(p->vFrames) )
1557 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
1558 else
1559 {
1560 for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
1561 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
1562 }
1563
1564 // iterate as long as there are counter-examples
1565 for ( i = 0; ; i++ )
1566 {
1567 clk2 = Abc_Clock();
1568 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
1569 assert( (vCore != NULL) == (Status == 1) );
1570 if ( Status == -1 ) // resource limit is reached
1571 {
1572 Vga_ManRollBack( p, nObjOld );
1573 goto finish;
1574 }
1575 // check timeout
1576 if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit )
1577 {
1578 Vga_ManRollBack( p, nObjOld );
1579 goto finish;
1580 }
1581 if ( vCore != NULL )
1582 {
1583 p->timeUnsat += Abc_Clock() - clk2;
1584 break;
1585 }
1586 p->timeSat += Abc_Clock() - clk2;
1587 assert( Status == 0 );
1588 p->nCexes++;
1589 // perform the refinement
1590 clk2 = Abc_Clock();
1591 pCex = Vta_ManRefineAbstraction( p, f );
1592 p->timeCex += Abc_Clock() - clk2;
1593 if ( pCex != NULL )
1594 goto finish;
1595 // print the result (do not count it towards change)
1596 Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose );
1597 }
1598 assert( Status == 1 );
1599 // valid core is obtained
1600 Vta_ManUnsatCoreRemap( p, vCore );
1601 Vec_IntSort( vCore, 1 );
1602 // update the SAT solver
1603 sat_solver2_rollback( p->pSat );
1604 // update storage
1605 Vga_ManRollBack( p, nObjOld );
1606 // load this timeframe
1607 Vga_ManLoadSlice( p, vCore, 0 );
1608 Vec_IntFree( vCore );
1609
1610 // run SAT solver
1611 clk2 = Abc_Clock();
1612 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
1613 p->timeUnsat += Abc_Clock() - clk2;
1614 assert( (vCore != NULL) == (Status == 1) );
1615 if ( Status == -1 ) // resource limit is reached
1616 break;
1617 if ( Status == 0 )
1618 {
1619 Vta_ManSatVerify( p );
1620 // make sure, there was no initial abstraction (otherwise, it was invalid)
1621 assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
1622 pCex = Vga_ManDeriveCex( p );
1623 break;
1624 }
1625 // add the core
1626 Vta_ManUnsatCoreRemap( p, vCore );
1627 // add in direct topological order
1628 Vec_IntSort( vCore, 1 );
1629 Vec_PtrPush( p->vCores, vCore );
1630 // print the result
1631 if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) )
1632 {
1633 // reset the counter of frames without change
1634 nCountNoChange = 1;
1635 p->pPars->nFramesNoChange = 0;
1636 }
1637 else if ( ++nCountNoChange == 2 ) // time to send
1638 {
1639 p->pPars->nFramesNoChange++;
1640 if ( Abc_FrameIsBridgeMode() )
1641 {
1642 // cancel old one if it was sent
1643 if ( fOneIsSent )
1644 Gia_VtaSendCancel( p, pPars->fVerbose );
1645 // send new one
1646 Gia_VtaSendAbsracted( p, pPars->fVerbose );
1647 fOneIsSent = 1;
1648 }
1649 }
1650 // dump the model
1651 if ( p->pPars->fDumpVabs && (f & 1) )
1652 {
1653 char Command[1000];
1654 Abc_FrameSetStatus( -1 );
1655 Abc_FrameSetCex( NULL );
1656 Abc_FrameSetNFrames( f+1 );
1657 sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "vtabs.aig"), ".status") );
1658 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1659 Gia_VtaDumpAbsracted( p, pPars->fVerbose );
1660 }
1661 // check if the number of objects is below limit
1662 if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
1663 {
1664 Status = -1;
1665 break;
1666 }
1667 }
1668finish:
1669 // analize the results
1670 if ( pCex == NULL )
1671 {
1672 if ( p->pPars->fVerbose && Status == -1 )
1673 printf( "\n" );
1674 if ( Vec_PtrSize(p->vCores) == 0 )
1675 Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " );
1676 else
1677 {
1678 assert( Vec_PtrSize(p->vCores) > 0 );
1679// if ( pAig->vObjClasses != NULL )
1680// Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
1681 Vec_IntFreeP( &pAig->vObjClasses );
1682 pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1683 if ( Status == -1 )
1684 {
1685 if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
1686 Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
1687 else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1688 Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
1689 else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
1690 Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
1691 else
1692 Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
1693 }
1694 else
1695 {
1696 p->pPars->iFrame++;
1697 Abc_Print( 1, "VTA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
1698 }
1699 }
1700 }
1701 else
1702 {
1703 if ( p->pPars->fVerbose )
1704 printf( "\n" );
1705 ABC_FREE( p->pGia->pCexSeq );
1706 p->pGia->pCexSeq = pCex;
1707 if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
1708 Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" );
1709 Abc_Print( 1, "Counter-example detected in frame %d. ", f );
1710 p->pPars->iFrame = pCex->iFrame - 1;
1711 Vec_IntFreeP( &pAig->vObjClasses );
1712 RetValue = 0;
1713 }
1714 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1715
1716 if ( p->pPars->fVerbose )
1717 {
1718 p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
1719 ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
1720 ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
1721 ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
1722 ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
1723 ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1724 Gia_VtaPrintMemory( p );
1725 }
1726
1727 Vga_ManStop( p );
1728 fflush( stdout );
1729 return RetValue;
1730}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Gia_VtaSendAbsracted
void Gia_VtaSendAbsracted(Vta_Man_t *p, int fVerbose)
Definition absVta.c:1384
Vta_ManUnsatCoreRemap
void Vta_ManUnsatCoreRemap(Vta_Man_t *p, Vec_Int_t *vCore)
Definition absVta.c:368
Vta_ManRefineAbstraction
Abc_Cex_t * Vta_ManRefineAbstraction(Vta_Man_t *p, int f)
Definition absVta.c:581
Gia_VtaPrintMemory
void Gia_VtaPrintMemory(Vta_Man_t *p)
Definition absVta.c:1458
Gia_VtaDumpAbsracted
void Gia_VtaDumpAbsracted(Vta_Man_t *p, int fVerbose)
Definition absVta.c:1424
Vta_ManSatVerify
void Vta_ManSatVerify(Vta_Man_t *p)
Definition absVta.c:512
Vec_IntDoubleWidth
int Vec_IntDoubleWidth(Vec_Int_t *p, int nWords)
Definition absVta.c:241
Vga_ManStart
Vta_Man_t * Vga_ManStart(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition absVta.c:983
Gia_VtaSendCancel
void Gia_VtaSendCancel(Vta_Man_t *p, int fVerbose)
Definition absVta.c:1404
Vga_ManLoadSlice
void Vga_ManLoadSlice(Vta_Man_t *p, Vec_Int_t *vOne, int Lift)
Definition absVta.c:1313
Vga_ManStop
void Vga_ManStop(Vta_Man_t *p)
Definition absVta.c:1033
Vta_ManAbsPrintFrame
int Vta_ManAbsPrintFrame(Vta_Man_t *p, Vec_Int_t *vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose)
Definition absVta.c:1143
Vta_ManUnsatCore
Vec_Int_t * Vta_ManUnsatCore(int iLit, sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue, int *pnConfls)
Definition absVta.c:1083
Vga_ManAddClausesOne
void Vga_ManAddClausesOne(Vta_Man_t *p, int iObj, int iFrame)
Definition absVta.c:1254
Vga_ManDeriveCex
Abc_Cex_t * Vga_ManDeriveCex(Vta_Man_t *p)
Definition absVta.c:342
Vga_ManRollBack
void Vga_ManRollBack(Vta_Man_t *p, int nObjOld)
Definition absVta.c:1355
Vta_Man_t
struct Vta_Man_t_ Vta_Man_t
Definition absVta.c:45
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition mainFrame.c:100
Abc_FrameSetStatus
ABC_DLL void Abc_FrameSetStatus(int Status)
Definition mainFrame.c:101
Abc_FrameSetCex
ABC_DLL void Abc_FrameSetCex(Abc_Cex_t *pCex)
Definition mainFrame.c:99
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition mainFrame.c:113
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition satSolver2.c:1586
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition gia.h:150
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition utilCex.c:85
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
sprintf
char * sprintf()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_VtaPrintMemory()

void Gia_VtaPrintMemory ( Vta_Man_t * p)

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

Synopsis [Print memory report.]

Description []

SideEffects []

SeeAlso []

Definition at line 1458 of file absVta.c.

1459{
1460 double memTot = 0;
1461 double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
1462 double memSat = sat_solver2_memory( p->pSat, 1 );
1463 double memPro = sat_solver2_memory_proof( p->pSat );
1464 double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
1465 double memOth = sizeof(Vta_Man_t);
1466 memOth += Vec_IntCap(p->vOrder) * sizeof(int);
1467 memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
1468 memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
1469 memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
1470 memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
1471 memTot = memAig + memSat + memPro + memMap + memOth;
1472 ABC_PRMP( "Memory: AIG ", memAig, memTot );
1473 ABC_PRMP( "Memory: SAT ", memSat, memTot );
1474 ABC_PRMP( "Memory: Proof ", memPro, memTot );
1475 ABC_PRMP( "Memory: Map ", memMap, memTot );
1476 ABC_PRMP( "Memory: Other ", memOth, memTot );
1477 ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
1478}
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition abc_global.h:262
Vta_Obj_t
struct Vta_Obj_t_ Vta_Obj_t
DECLARATIONS ///.
Definition absVta.c:33
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
sat_solver2_memory_proof
double sat_solver2_memory_proof(sat_solver2 *s)
Definition satSolver2.c:1733
sat_solver2_memory
double sat_solver2_memory(sat_solver2 *s, int fAll)
Definition satSolver2.c:1692
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_VtaSendAbsracted()

void Gia_VtaSendAbsracted ( Vta_Man_t * p,
int fVerbose )

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1384 of file absVta.c.

1385{
1386 Gia_Man_t * pAbs;
1387 assert( Abc_FrameIsBridgeMode() );
1388// if ( fVerbose )
1389// Abc_Print( 1, "Sending abstracted model...\n" );
1390 // create obj classes
1391 Vec_IntFreeP( &p->pGia->vObjClasses );
1392 p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1393 // create gate classes
1394 Vec_IntFreeP( &p->pGia->vGateClasses );
1395 p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
1396 Vec_IntFreeP( &p->pGia->vObjClasses );
1397 // create abstrated model
1398 pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
1399 Vec_IntFreeP( &p->pGia->vGateClasses );
1400 // send it out
1401 Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1402 Gia_ManStop( pAbs );
1403}
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition utilBridge.c:192
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition abc_global.h:387
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_VtaSendCancel()

void Gia_VtaSendCancel ( Vta_Man_t * p,
int fVerbose )

Definition at line 1404 of file absVta.c.

1405{
1406 extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1407 assert( Abc_FrameIsBridgeMode() );
1408// if ( fVerbose )
1409// Abc_Print( 1, "Cancelling previously sent model...\n" );
1410 Gia_ManToBridgeBadAbs( stdout );
1411}
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition utilBridge.c:202
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vec_IntDoubleWidth()

int Vec_IntDoubleWidth ( Vec_Int_t * p,
int nWords )

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

Synopsis [Collect nodes/flops involved in different timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file absVta.c.

242{
243 int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 );
244 int i, w, nObjs = Vec_IntSize(p) / nWords;
245 assert( Vec_IntSize(p) % nWords == 0 );
246 for ( i = 0; i < nObjs; i++ )
247 for ( w = 0; w < nWords; w++ )
248 pArray[2 * nWords * i + w] = p->pArray[nWords * i + w];
249 ABC_FREE( p->pArray );
250 p->pArray = pArray;
251 p->nSize *= 2;
252 p->nCap = p->nSize;
253 return 2 * nWords;
254}
nWords
int nWords
Definition abcNpn.c:127
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Here is the caller graph for this function:

◆ Vga_ManAddClausesOne()

void Vga_ManAddClausesOne ( Vta_Man_t * p,
int iObj,
int iFrame )
extern

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1254 of file absVta.c.

1255{
1256 Vta_Obj_t * pThis0, * pThis1;
1257 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
1258 Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
1259 int iThis0, iMainVar = Vta_ObjId(p, pThis);
1260 assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
1261 if ( pThis->fAdded )
1262 return;
1263 pThis->fAdded = 1;
1264 Vec_IntPush( p->vAddedNew, iMainVar );
1265 if ( Gia_ObjIsAnd(pObj) )
1266 {
1267 pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
1268 iThis0 = Vta_ObjId(p, pThis0);
1269 pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
1270 sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1),
1271 Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
1272 }
1273 else if ( Gia_ObjIsRo(p->pGia, pObj) )
1274 {
1275 if ( iFrame == 0 )
1276 {
1277 if ( p->pPars->fUseTermVars )
1278 {
1279 pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
1280 sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
1281 }
1282 else
1283 {
1284 sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1285 }
1286 }
1287 else
1288 {
1289 pObj = Gia_ObjRoToRi( p->pGia, pObj );
1290 pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
1291 sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );
1292 }
1293 }
1294 else if ( Gia_ObjIsConst0(pObj) )
1295 {
1296 sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1297 }
1298 else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
1299 assert( 0 );
1300}
Vta_Obj_t_::iObj
int iObj
Definition absVta.c:36
Vta_Obj_t_::iFrame
int iFrame
Definition absVta.c:37
Vta_Obj_t_::fAdded
unsigned fAdded
Definition absVta.c:41
Here is the caller graph for this function:

◆ Vga_ManDeriveCex()

Abc_Cex_t * Vga_ManDeriveCex ( Vta_Man_t * p)

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

Synopsis [Derives counter-example using current assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file absVta.c.

343{
344 Abc_Cex_t * pCex;
345 Vta_Obj_t * pThis;
346 Gia_Obj_t * pObj;
347 int i;
348 pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
349 pCex->iPo = 0;
350 pCex->iFrame = p->pPars->iFrame;
351 Vta_ManForEachObjObj( p, pThis, pObj, i )
352 if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
353 Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
354 return pCex;
355}
Vta_ManForEachObjObj
#define Vta_ManForEachObjObj(p, pObjVta, pObjGia, i)
Definition absVta.c:109
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vga_ManLoadSlice()

void Vga_ManLoadSlice ( Vta_Man_t * p,
Vec_Int_t * vOne,
int Lift )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1313 of file absVta.c.

1314{
1315 int i, Entry;
1316 Vec_IntForEachEntry( vOne, Entry, i )
1317 Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
1318 sat_solver2_simplify( p->pSat );
1319}
sat_solver2_simplify
int sat_solver2_simplify(sat_solver2 *s)
Definition satSolver2.c:996
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vga_ManPrintCore()

void Vga_ManPrintCore ( Vta_Man_t * p,
Vec_Int_t * vCore,
int Lift )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1332 of file absVta.c.

1333{
1334 int i, Entry, iObj, iFrame;
1335 Vec_IntForEachEntry( vCore, Entry, i )
1336 {
1337 iObj = (Entry & p->nObjMask);
1338 iFrame = (Entry >> p->nObjBits);
1339 Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
1340 }
1341 Abc_Print( 1, "\n" );
1342}

◆ Vga_ManRollBack()

void Vga_ManRollBack ( Vta_Man_t * p,
int nObjOld )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1355 of file absVta.c.

1356{
1357 Vta_Obj_t * pThis = p->pObjs + nObjOld;
1358 Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
1359 int i, Entry;
1360 for ( ; pThis < pLimit; pThis++ )
1361 Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
1362 memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
1363 p->nObjs = nObjOld;
1364 Vec_IntForEachEntry( p->vAddedNew, Entry, i )
1365 if ( Entry < p->nObjs )
1366 {
1367 pThis = Vta_ManObj(p, Entry);
1368 assert( pThis->fAdded == 1 );
1369 pThis->fAdded = 0;
1370 }
1371}
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vga_ManStart()

Vta_Man_t * Vga_ManStart ( Gia_Man_t * pGia,
Abs_Par_t * pPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 983 of file absVta.c.

984{
985 Vta_Man_t * p;
986 p = ABC_CALLOC( Vta_Man_t, 1 );
987 p->pGia = pGia;
988 p->pPars = pPars;
989 // internal data
990 p->nObjsAlloc = (1 << 18);
991 p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
992 p->nObjs = 1;
993 p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc );
994 p->pBins = ABC_CALLOC( int, p->nBins );
995 p->vOrder = Vec_IntAlloc( 1013 );
996 // abstraction
997 p->nObjBits = Abc_Base2Log( Gia_ManObjNum(pGia) );
998 p->nObjMask = (1 << p->nObjBits) - 1;
999 assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
1000 p->nWords = 1;
1001 p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
1002 p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
1003 p->nSeenGla = 1;
1004 p->nSeenAll = 1;
1005 // other data
1006 p->vCores = Vec_PtrAlloc( 100 );
1007 p->pSat = sat_solver2_new();
1008 p->pSat->pPrf1 = Vec_SetAlloc( 20 );
1009// p->pSat->fVerbose = p->pPars->fVerbose;
1010// sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
1011 p->pSat->nLearntStart = p->pPars->nLearnedStart;
1012 p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1013 p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1014 p->pSat->nLearntMax = p->pSat->nLearntStart;
1015 // start the abstraction
1016 assert( pGia->vObjClasses != NULL );
1017 p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
1018 p->vAddedNew = Vec_IntAlloc( 1000 );
1019 return p;
1020}
Gia_VtaAbsToFrames
Vec_Ptr_t * Gia_VtaAbsToFrames(Vec_Int_t *vAbs)
FUNCTION DEFINITIONS ///.
Definition absVta.c:148
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition satSolver2.c:1109
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vga_ManStop()

void Vga_ManStop ( Vta_Man_t * p)

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

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1033 of file absVta.c.

1034{
1035 if ( p->pPars->fVerbose )
1036 Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
1037 sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
1038 sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
1039 Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
1040 Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
1041 Vec_BitFreeP( &p->vSeenGla );
1042 Vec_IntFreeP( &p->vSeens );
1043 Vec_IntFreeP( &p->vOrder );
1044 Vec_IntFreeP( &p->vAddedNew );
1045 sat_solver2_delete( p->pSat );
1046 ABC_FREE( p->pBins );
1047 ABC_FREE( p->pObjs );
1048 ABC_FREE( p );
1049}
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:

◆ Vta_ManAbsPrintFrame()

int Vta_ManAbsPrintFrame ( Vta_Man_t * p,
Vec_Int_t * vCore,
int nFrames,
int nConfls,
int nCexes,
abctime Time,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1143 of file absVta.c.

1144{
1145 unsigned * pInfo;
1146 int * pCountAll = NULL, * pCountUni = NULL;
1147 int i, iFrame, iObj, Entry, fChanges = 0;
1148 // print info about frames
1149 if ( vCore )
1150 {
1151 pCountAll = ABC_CALLOC( int, nFrames + 1 );
1152 pCountUni = ABC_CALLOC( int, nFrames + 1 );
1153 Vec_IntForEachEntry( vCore, Entry, i )
1154 {
1155 iObj = (Entry & p->nObjMask);
1156 iFrame = (Entry >> p->nObjBits);
1157 assert( iFrame < nFrames );
1158 pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
1159 if ( !Abc_InfoHasBit(pInfo, iFrame) )
1160 {
1161 Abc_InfoSetBit( pInfo, iFrame );
1162 pCountUni[iFrame+1]++;
1163 pCountUni[0]++;
1164 p->nSeenAll++;
1165 }
1166 pCountAll[iFrame+1]++;
1167 pCountAll[0]++;
1168 if ( !Vec_BitEntry(p->vSeenGla, iObj) )
1169 {
1170 Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
1171 p->nSeenGla++;
1172 fChanges = 1;
1173 }
1174 }
1175 }
1176 if ( !fVerbose )
1177 {
1178 ABC_FREE( pCountAll );
1179 ABC_FREE( pCountUni );
1180 return fChanges;
1181 }
1182
1183 if ( Abc_FrameIsBatchMode() && !vCore )
1184 return fChanges;
1185
1186// Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
1187 Abc_Print( 1, "%4d :", nFrames-1 );
1188 Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );
1189 Abc_Print( 1, "%6d", p->nSeenGla );
1190 Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
1191 Abc_Print( 1, "%8d", nConfls );
1192 if ( nCexes == 0 )
1193 Abc_Print( 1, "%5c", '-' );
1194 else
1195 Abc_Print( 1, "%5d", nCexes );
1196// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
1197 Abc_PrintInt( sat_solver2_nvars(p->pSat) );
1198 Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
1199 Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1200 if ( vCore == NULL )
1201 {
1202 Abc_Print( 1, " ..." );
1203// for ( k = 0; k < 7; k++ )
1204// Abc_Print( 1, " " );
1205 Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1206 Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1207 Abc_Print( 1, "\r" );
1208 }
1209 else
1210 {
1211 Abc_PrintInt( pCountAll[0] );
1212/*
1213 if ( nFrames > 7 )
1214 {
1215 for ( k = 0; k < 3; k++ )
1216 Abc_Print( 1, "%5d", pCountAll[k+1] );
1217 Abc_Print( 1, " ..." );
1218 for ( k = nFrames-3; k < nFrames; k++ )
1219 Abc_Print( 1, "%5d", pCountAll[k+1] );
1220 }
1221 else
1222 {
1223 for ( k = 0; k < nFrames; k++ )
1224 Abc_Print( 1, "%5d", pCountAll[k+1] );
1225 for ( k = nFrames; k < 7; k++ )
1226 Abc_Print( 1, " " );
1227 }
1228*/
1229 Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1230 Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1231 Abc_Print( 1, "\n" );
1232 }
1233 fflush( stdout );
1234
1235 if ( vCore )
1236 {
1237 ABC_FREE( pCountAll );
1238 ABC_FREE( pCountUni );
1239 }
1240 return fChanges;
1241}
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition mainFrame.c:110
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vta_ManCollectNodes()

Vec_Int_t * Vta_ManCollectNodes ( Vta_Man_t * p,
int f )

Definition at line 487 of file absVta.c.

488{
489 Vta_Obj_t * pThis;
490 Gia_Obj_t * pObj;
491 Vec_IntClear( p->vOrder );
492 pObj = Gia_ManPo( p->pGia, 0 );
493 pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
494 assert( pThis != NULL );
495 assert( !pThis->fVisit );
496 Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
497 assert( pThis->fVisit );
498 return p->vOrder;
499}
Vta_ManCollectNodes_rec
void Vta_ManCollectNodes_rec(Vta_Man_t *p, Vta_Obj_t *pThis, Vec_Int_t *vOrder)
Definition absVta.c:471
Vta_Obj_t_::fVisit
unsigned fVisit
Definition absVta.c:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vta_ManCollectNodes_rec()

void Vta_ManCollectNodes_rec ( Vta_Man_t * p,
Vta_Obj_t * pThis,
Vec_Int_t * vOrder )

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

Synopsis [Collect const/PI/RO/AND in a topological order.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file absVta.c.

472{
473 Gia_Obj_t * pObj;
474 Vta_Obj_t * pThis0, * pThis1;
475 if ( pThis->fVisit )
476 return;
477 pThis->fVisit = 1;
478 pObj = Gia_ManObj( p->pGia, pThis->iObj );
479 if ( pThis->fAdded )
480 {
481 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
482 if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
483 if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
484 }
485 Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
486}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vta_ManComputeDepthIncrease()

int Vta_ManComputeDepthIncrease ( Vta_Obj_t ** pp1,
Vta_Obj_t ** pp2 )

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

Synopsis [Compares two objects by their distance.]

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file absVta.c.

392{
393 int Diff = (*pp1)->Prio - (*pp2)->Prio;
394 if ( Diff < 0 )
395 return -1;
396 if ( Diff > 0 )
397 return 1;
398 Diff = (*pp1) - (*pp2);
399 if ( Diff < 0 )
400 return -1;
401 if ( Diff > 0 )
402 return 1;
403 return 0;
404}
Here is the caller graph for this function:

◆ Vta_ManObjIsUsed()

int Vta_ManObjIsUsed ( Vta_Man_t * p,
int iObj )

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

Synopsis [Returns 1 if the object is already used.]

Description []

SideEffects []

SeeAlso []

Definition at line 417 of file absVta.c.

418{
419 int i;
420 unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
421 for ( i = 0; i < p->nWords; i++ )
422 if ( pInfo[i] )
423 return 1;
424 return 0;
425}
Here is the caller graph for this function:

◆ Vta_ManProfileAddition()

void Vta_ManProfileAddition ( Vta_Man_t * p,
Vec_Int_t * vTermsToAdd )

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 557 of file absVta.c.

558{
559 Vta_Obj_t * pThis;
560 Gia_Obj_t * pObj;
561 // profile the added ones
562 int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
563 Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
564 pCounters[pThis->iFrame]++;
565 for ( i = 0; i <= p->pPars->iFrame; i++ )
566 Abc_Print( 1, "%2d", pCounters[i] );
567 Abc_Print( 1, "***\n" );
568}
Vta_ManForEachObjObjVec
#define Vta_ManForEachObjObjVec(vVec, p, pObj, pObjG, i)
Definition absVta.c:119

◆ Vta_ManRefineAbstraction()

Abc_Cex_t * Vta_ManRefineAbstraction ( Vta_Man_t * p,
int f )

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file absVta.c.

582{
583 int fVerify = 0;
584 Abc_Cex_t * pCex = NULL;
585 Vec_Int_t * vOrder, * vTermsToAdd;
586 Vec_Ptr_t * vTermsUsed, * vTermsUnused;
587 Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
588 Gia_Obj_t * pObj;
589 int i, Counter;
590
591 if ( fVerify )
592 Vta_ManSatVerify( p );
593
594 // collect nodes in a topological order
595 vOrder = Vta_ManCollectNodes( p, f );
596 Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
597 {
598 pThis->Prio = VTA_LARGE;
599 pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
600 pThis->fVisit = 0;
601 }
602
603 // verify
604 if ( fVerify )
605 Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
606 {
607 if ( !pThis->fAdded )
608 continue;
609 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
610 if ( Gia_ObjIsAnd(pObj) )
611 {
612 if ( pThis->Value == VTA_VAR1 )
613 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
614 else if ( pThis->Value == VTA_VAR0 )
615 assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
616 else assert( 0 );
617 }
618 else if ( Gia_ObjIsRo(p->pGia, pObj) )
619 {
620 pObj = Gia_ObjRoToRi( p->pGia, pObj );
621 if ( pThis->iFrame == 0 )
622 assert( pThis->Value == VTA_VAR0 );
623 else if ( pThis->Value == VTA_VAR0 )
624 assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
625 else if ( pThis->Value == VTA_VAR1 )
626 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
627 else assert( 0 );
628 }
629 }
630
631 // compute distance in reverse order
632 pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
633 pThis->Prio = 1;
634 // collect used and unused terms
635 vTermsUsed = Vec_PtrAlloc( 1015 );
636 vTermsUnused = Vec_PtrAlloc( 1016 );
637 Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
638 {
639 // there is no unreachable states
640 assert( pThis->Prio < VTA_LARGE );
641 // skip constants and PIs
642 if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
643 {
644 pThis->Prio = 0; // set highest priority
645 continue;
646 }
647 // collect terminals
648 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
649 if ( !pThis->fAdded )
650 {
651 assert( pThis->Prio > 0 );
652 if ( Vta_ManObjIsUsed(p, pThis->iObj) )
653 Vec_PtrPush( vTermsUsed, pThis );
654 else
655 Vec_PtrPush( vTermsUnused, pThis );
656 continue;
657 }
658 // propagate
659 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
660 if ( pThis0 )
661 pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
662 if ( pThis1 )
663 pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
664 }
665
666/*
667 Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
668 if ( pThis->Prio > 0 )
669 pThis->Prio = 10;
670*/
671/*
672 // update priorities according to reconvergence counters
673 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
674 {
675 Vta_Obj_t * pThis0, * pThis1;
676 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
677 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
678 pThis->Prio += 10000000;
679 if ( pThis0 )
680 pThis->Prio -= 1000000 * pThis0->fAdded;
681 if ( pThis1 )
682 pThis->Prio -= 1000000 * pThis1->fAdded;
683 }
684 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
685 {
686 Vta_Obj_t * pThis0, * pThis1;
687 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
688 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
689 pThis->Prio += 10000000;
690 if ( pThis0 )
691 pThis->Prio -= 1000000 * pThis0->fAdded;
692 if ( pThis1 )
693 pThis->Prio -= 1000000 * pThis1->fAdded;
694 }
695*/
696
697
698 // update priorities according to reconvergence counters
699 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
700 pThis->Prio = pThis->iObj;
701 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
702 pThis->Prio = pThis->iObj;
703
704
705 // objects with equal distance should receive priority based on number
706 // those objects whose prototypes have been added in other timeframes
707 // should have higher priority than the current object
708 Vec_PtrSort( vTermsUsed, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
709 Vec_PtrSort( vTermsUnused, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
710 if ( Vec_PtrSize(vTermsUsed) > 1 )
711 {
712 pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
713 pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
714 assert( pThis0->Prio <= pThis1->Prio );
715 }
716 // assign the priority based on these orders
717 Counter = 1;
718 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
719 pThis->Prio = Counter++;
720 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
721 pThis->Prio = Counter++;
722// Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
723
724
725 // propagate in the direct order
726 Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
727 {
728 assert( pThis->fVisit == 0 );
729 assert( pThis->Prio < VTA_LARGE );
730 // skip terminal objects
731 if ( !pThis->fAdded )
732 continue;
733 // assumes that values are assigned!!!
734 assert( pThis->Value != 0 );
735 // propagate
736 if ( Gia_ObjIsAnd(pObj) )
737 {
738 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
739 pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
740 assert( pThis0 && pThis1 );
741 if ( pThis->Value == VTA_VAR1 )
742 {
743 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
744 pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
745 }
746 else if ( pThis->Value == VTA_VAR0 )
747 {
748 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
749 pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
750 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
751 pThis->Prio = pThis0->Prio;
752 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
753 pThis->Prio = pThis1->Prio;
754 else assert( 0 );
755 }
756 else assert( 0 );
757 }
758 else if ( Gia_ObjIsRo(p->pGia, pObj) )
759 {
760 if ( pThis->iFrame > 0 )
761 {
762 pObj = Gia_ObjRoToRi( p->pGia, pObj );
763 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
764 assert( pThis0 );
765 pThis->Prio = pThis0->Prio;
766 }
767 else
768 pThis->Prio = 0;
769 }
770 else if ( Gia_ObjIsConst0(pObj) )
771 pThis->Prio = 0;
772 else
773 assert( 0 );
774 }
775
776 // select important values
777 pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
778 pTop->fVisit = 1;
779 vTermsToAdd = Vec_IntAlloc( 100 );
780 Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
781 {
782 if ( !pThis->fVisit )
783 continue;
784 pThis->fVisit = 0;
785 assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
786 // skip terminal objects
787 if ( !pThis->fAdded )
788 {
789 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
790 Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
791 continue;
792 }
793 // assumes that values are assigned!!!
794 assert( pThis->Value != 0 );
795 // propagate
796 if ( Gia_ObjIsAnd(pObj) )
797 {
798 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
799 pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
800 assert( pThis0 && pThis1 );
801 if ( pThis->Value == VTA_VAR1 )
802 {
803 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
804 assert( pThis0->Prio <= pThis->Prio );
805 assert( pThis1->Prio <= pThis->Prio );
806 pThis0->fVisit = 1;
807 pThis1->fVisit = 1;
808 }
809 else if ( pThis->Value == VTA_VAR0 )
810 {
811 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
812 {
813 if ( pThis0->fVisit )
814 {
815 }
816 else if ( pThis1->fVisit )
817 {
818 }
819 else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
820 {
821 pThis0->fVisit = 1;
822 assert( pThis0->Prio == pThis->Prio );
823 }
824 else
825 {
826 pThis1->fVisit = 1;
827 assert( pThis1->Prio == pThis->Prio );
828 }
829 }
830 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
831 {
832 pThis0->fVisit = 1;
833 assert( pThis0->Prio == pThis->Prio );
834 }
835 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
836 {
837 pThis1->fVisit = 1;
838 assert( pThis1->Prio == pThis->Prio );
839 }
840 else assert( 0 );
841 }
842 else assert( 0 );
843 }
844 else if ( Gia_ObjIsRo(p->pGia, pObj) )
845 {
846 if ( pThis->iFrame > 0 )
847 {
848 pObj = Gia_ObjRoToRi( p->pGia, pObj );
849 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
850 assert( pThis0 );
851 pThis0->fVisit = 1;
852 assert( pThis0->Prio == pThis->Prio );
853 }
854 }
855 else if ( !Gia_ObjIsConst0(pObj) )
856 assert( 0 );
857 }
858
859 if ( p->pPars->fAddLayer )
860 {
861 // mark those currently included
862 Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
863 {
864 assert( pThis->fVisit == 0 );
865 pThis->fVisit = 1;
866 }
867 // add used terms, which have close relationship
868 Counter = Vec_IntSize(vTermsToAdd);
869 Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
870 {
871 if ( pThis->fVisit )
872 continue;
873 // Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
874 // if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
875 Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
876 }
877 // remove those currenty included
878 Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
879 pThis->fVisit = 0;
880 }
881// printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
882//Vec_IntReverseOrder( vTermsToAdd );
883//Vec_IntSort( vTermsToAdd, 1 );
884
885
886 // cleanup
887 Vec_PtrFree( vTermsUsed );
888 Vec_PtrFree( vTermsUnused );
889
890
891 if ( fVerify )
892 {
893 // verify
894 Vta_ManForEachObjVec( vOrder, p, pThis, i )
895 pThis->Value = VTA_VARX;
896 Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
897 {
898 assert( !pThis->fAdded );
899 pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
900 }
901 // simulate
902 Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
903 {
904 assert( pThis->fVisit == 0 );
905 if ( !pThis->fAdded )
906 continue;
907 if ( Gia_ObjIsAnd(pObj) )
908 {
909 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
910 pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
911 assert( pThis0 && pThis1 );
912 if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
913 pThis->Value = VTA_VAR1;
914 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
915 pThis->Value = VTA_VAR0;
916 else
917 pThis->Value = VTA_VARX;
918 }
919 else if ( Gia_ObjIsRo(p->pGia, pObj) )
920 {
921 if ( pThis->iFrame > 0 )
922 {
923 pObj = Gia_ObjRoToRi( p->pGia, pObj );
924 pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
925 assert( pThis0 );
926 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
927 pThis->Value = VTA_VAR0;
928 else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
929 pThis->Value = VTA_VAR1;
930 else
931 pThis->Value = VTA_VARX;
932 }
933 else
934 {
935 pThis->Value = VTA_VAR0;
936 }
937 }
938 else if ( Gia_ObjIsConst0(pObj) )
939 {
940 pThis->Value = VTA_VAR0;
941 }
942 else assert( 0 );
943 // double check the solver
944 assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
945 }
946
947 // check the output
948 if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
949 Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
950// else
951// Abc_Print( 1, "Verification OK.\n" );
952 }
953
954
955 // produce true counter-example
956 if ( pTop->Prio == 0 )
957 pCex = Vga_ManDeriveCex( p );
958 else
959 {
960// Vta_ManProfileAddition( p, vTermsToAdd );
961
962 Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
963 if ( !Gia_ObjIsPi(p->pGia, pObj) )
964 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
965 sat_solver2_simplify( p->pSat );
966 }
967 p->nObjAdded += Vec_IntSize(vTermsToAdd);
968 Vec_IntFree( vTermsToAdd );
969 return pCex;
970}
VTA_VAR0
#define VTA_VAR0
Definition absVta.c:83
Vta_ManForEachObjVec
#define Vta_ManForEachObjVec(vVec, p, pObj, i)
Definition absVta.c:114
VTA_VARX
#define VTA_VARX
Definition absVta.c:85
Vta_ManObjIsUsed
int Vta_ManObjIsUsed(Vta_Man_t *p, int iObj)
Definition absVta.c:417
Vta_ManCollectNodes
Vec_Int_t * Vta_ManCollectNodes(Vta_Man_t *p, int f)
Definition absVta.c:487
Vta_ManForEachObjObjVecReverse
#define Vta_ManForEachObjObjVecReverse(vVec, p, pObj, pObjG, i)
Definition absVta.c:121
VTA_VAR1
#define VTA_VAR1
Definition absVta.c:84
Vta_ManComputeDepthIncrease
int Vta_ManComputeDepthIncrease(Vta_Obj_t **pp1, Vta_Obj_t **pp2)
Definition absVta.c:391
VTA_LARGE
#define VTA_LARGE
Definition absVta.c:27
Vta_Obj_t_::Prio
unsigned Prio
Definition absVta.c:39
Vta_Obj_t_::Value
unsigned Value
Definition absVta.c:40
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Vta_ManSatVerify()

void Vta_ManSatVerify ( Vta_Man_t * p)

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

Synopsis [Refines abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 512 of file absVta.c.

513{
514 Vta_Obj_t * pThis, * pThis0, * pThis1;
515 Gia_Obj_t * pObj;
516 int i;
517 Vta_ManForEachObj( p, pThis, i )
518 pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
519 Vta_ManForEachObjObj( p, pThis, pObj, i )
520 {
521 if ( !pThis->fAdded )
522 continue;
523 Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
524 if ( Gia_ObjIsAnd(pObj) )
525 {
526 if ( pThis->Value == VTA_VAR1 )
527 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
528 else if ( pThis->Value == VTA_VAR0 )
529 assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
530 else assert( 0 );
531 }
532 else if ( Gia_ObjIsRo(p->pGia, pObj) )
533 {
534 pObj = Gia_ObjRoToRi( p->pGia, pObj );
535 if ( pThis->iFrame == 0 )
536 assert( pThis->Value == VTA_VAR0 );
537 else if ( pThis->Value == VTA_VAR0 )
538 assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
539 else if ( pThis->Value == VTA_VAR1 )
540 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
541 else assert( 0 );
542 }
543 }
544}
Vta_ManForEachObj
#define Vta_ManForEachObj(p, pObj, i)
Definition absVta.c:107
Here is the caller graph for this function:

◆ Vta_ManUnsatCore()

Vec_Int_t * Vta_ManUnsatCore ( int iLit,
sat_solver2 * pSat,
int nConfMax,
int fVerbose,
int * piRetValue,
int * pnConfls )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1083 of file absVta.c.

1084{
1085 abctime clk = Abc_Clock();
1086 Vec_Int_t * vCore;
1087 int RetValue, nConfPrev = pSat->stats.conflicts;
1088 if ( piRetValue )
1089 *piRetValue = 1;
1090 // consider special case when PO points to the flop
1091 // this leads to immediate conflict in the first timeframe
1092 if ( iLit < 0 )
1093 {
1094 vCore = Vec_IntAlloc( 1 );
1095 Vec_IntPush( vCore, -iLit );
1096 return vCore;
1097 }
1098 // solve the problem
1099 RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1100 if ( pnConfls )
1101 *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
1102 if ( RetValue == l_Undef )
1103 {
1104 if ( piRetValue )
1105 *piRetValue = -1;
1106 return NULL;
1107 }
1108 if ( RetValue == l_True )
1109 {
1110 if ( piRetValue )
1111 *piRetValue = 0;
1112 return NULL;
1113 }
1114 if ( fVerbose )
1115 {
1116// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
1117// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
1118// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1119 }
1120 assert( RetValue == l_False );
1121 // derive the UNSAT core
1122 clk = Abc_Clock();
1123 vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
1124 if ( fVerbose )
1125 {
1126// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
1127// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1128 }
1129 return vCore;
1130}
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:

◆ Vta_ManUnsatCoreRemap()

void Vta_ManUnsatCoreRemap ( Vta_Man_t * p,
Vec_Int_t * vCore )

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

Synopsis [Remaps core into frame/node pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file absVta.c.

369{
370 Vta_Obj_t * pThis;
371 int i, Entry;
372 Vec_IntForEachEntry( vCore, Entry, i )
373 {
374 pThis = Vta_ManObj( p, Entry );
375 Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
376 Vec_IntWriteEntry( vCore, i, Entry );
377 }
378}
Here is the caller graph for this function: