diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 12:08:55 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 12:08:55 +0700 |
| commit | 29cb71f98bccf50fe18d795f17a71790c6c59e05 (patch) | |
| tree | 89ed234561ef3e0fc3f23cd32df19aa946dd8f46 /src/proof/pdr/pdrUtil.c | |
| parent | 6ff66ed49e004900854fb3507385f3392240e1f5 (diff) | |
| download | abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.tar.gz abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.tar.bz2 abc-29cb71f98bccf50fe18d795f17a71790c6c59e05.zip | |
Integrating Satoko into pdr.
Diffstat (limited to 'src/proof/pdr/pdrUtil.c')
| -rw-r--r-- | src/proof/pdr/pdrUtil.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 986697ac..b2eaa2c7 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -234,7 +234,7 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun { if ( p->Lits[i] == -1 ) continue; - pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); + pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1'); } if ( vFlopCounts ) { @@ -351,7 +351,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF { if ( p->Lits[i] == -1 ) continue; - pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); + pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1'); } if ( vFlopCounts ) { @@ -465,7 +465,7 @@ int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove ) assert( pCube->Lits[i] != -1 ); if ( i == iRemove ) continue; - if ( lit_sign( pCube->Lits[i] ) == 0 ) + if ( Abc_LitIsCompl( pCube->Lits[i] ) == 0 ) return 0; } return 1; |