diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2022-03-06 00:09:35 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2022-03-06 00:09:35 -0800 |
| commit | d86e8d9ed858d2ab081fe1ca5bfacdfb7aa28018 (patch) | |
| tree | 3980ad382d827e074ef3dae0823d0bc6f3fe2f91 /src/proof/cec | |
| parent | 32693e9857c21c03257ec620fb2439ad36d381e3 (diff) | |
| download | abc-d86e8d9ed858d2ab081fe1ca5bfacdfb7aa28018.tar.gz abc-d86e8d9ed858d2ab081fe1ca5bfacdfb7aa28018.tar.bz2 abc-d86e8d9ed858d2ab081fe1ca5bfacdfb7aa28018.zip | |
Experiments with word-level data structures.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCec.c | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 7c101570..40aa9799 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -206,6 +206,7 @@ struct Cec_ParSeq_t_ /*=== cecCec.c ==========================================================*/ extern int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ); extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ); +extern int Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ); extern int Cec_ManVerifySimple( Gia_Man_t * p ); /*=== cecChoice.c ==========================================================*/ extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ); diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index cfa07ff8..f6a1ab52 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -465,6 +465,21 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) Gia_ManStop( pMiter ); return RetValue; } +int Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) +{ + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Gia_Man_t * pMiter; + int RetValue; + Cec_ManCecSetDefaultParams( pPars ); + pPars->fVerbose = fVerbose; + pMiter = Gia_ManMiterInverse( p0, p1, 1, pPars->fVerbose ); + if ( pMiter == NULL ) + return -1; + RetValue = Cec_ManVerify( pMiter, pPars ); + p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL; + Gia_ManStop( pMiter ); + return RetValue; +} /**Function************************************************************* |