luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding timeout to the interpolant computation procedure.

This commit is contained in:
Alan Mishchenko 2013-06-28 10:42:31 -07:00
parent e93cfb18ee
commit 184c5d4ea4
4 changed files with 23 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/aig/aigInter.c
View File

@ -271,7 +271,7 @@ timeSat += Abc_Clock() - clk;
// create the resulting manager
clk = Abc_Clock();
pManInter = Inta_ManAlloc();
pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, vVarsAB, fVerbose );
pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, 0, vVarsAB, fVerbose );
Inta_ManFree( pManInter );
timeInt += Abc_Clock() - clk;
/*

4
src/proof/int/intM114.c
View File

@ -304,11 +304,13 @@ clk = Abc_Clock();
*/
pManInterA = Inta_ManAlloc();
p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 );
p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
Inta_ManFree( pManInterA );
p->timeInt += Abc_Clock() - clk;
Sto_ManFree( (Sto_Man_t *)pSatCnf );
if ( p->pInterNew == NULL )
RetValue = -1;
return RetValue;
}

19
src/sat/bsat/satInterA.c
View File

@ -948,7 +948,7 @@ void Inta_ManPrepareInter( Inta_Man_t * p )
SeeAlso []
***********************************************************************/
void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose )
{
Aig_Man_t * pRes;
Aig_Obj_t * pObj;
@ -956,6 +956,9 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
int RetValue = 1;
abctime clkTotal = Abc_Clock();
if ( Abc_Clock() > TimeToStop )
return NULL;
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
p->pCnf = pCnf;
@ -980,7 +983,15 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
// write the root clauses
Sto_ManForEachClauseRoot( p->pCnf, pClause )
{
Inta_ManProofWriteOne( p, pClause );
if ( TimeToStop && Abc_Clock() > TimeToStop )
{
Aig_ManStop( pRes );
p->pAig = NULL;
return NULL;
}
}
// propagate root level assignments
if ( Inta_ManProcessRoots( p ) )
@ -995,6 +1006,12 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
RetValue = 0;
break;
}
if ( TimeToStop && Abc_Clock() > TimeToStop )
{
Aig_ManStop( pRes );
p->pAig = NULL;
return NULL;
}
}
}

2
src/sat/bsat/satStore.h
View File

@ -130,7 +130,7 @@ extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVe
typedef struct Inta_Man_t_ Inta_Man_t;
extern Inta_Man_t * Inta_ManAlloc();
extern void Inta_ManFree( Inta_Man_t * p );
extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose );
/*=== satInterB.c ==========================================================*/
typedef struct Intb_Man_t_ Intb_Man_t;