diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-07-11 16:49:06 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-07-11 16:49:06 -0700 |
| commit | b949436f4c99157397e16b23c3693fb5a99bd557 (patch) | |
| tree | 7b15b5005db8a12b8afbf757d7abbe648eb84f66 /src/proof | |
| parent | 05ca4afb770ffffca62e913f4e2fd4fd56085281 (diff) | |
| download | abc-b949436f4c99157397e16b23c3693fb5a99bd557.tar.gz abc-b949436f4c99157397e16b23c3693fb5a99bd557.tar.bz2 abc-b949436f4c99157397e16b23c3693fb5a99bd557.zip | |
Adding new Python API 'is_func_iso'.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCec.c | 21 |
2 files changed, 22 insertions, 0 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 805a5d73..a0b92b52 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -197,6 +197,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_ManVerifySimple( Gia_Man_t * p ); /*=== cecChoice.c ==========================================================*/ extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ); /*=== cecCorr.c ==========================================================*/ diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index 1465a721..77a6ed4a 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -415,6 +415,27 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) /**Function************************************************************* + Synopsis [Simple SAT run to check equivalence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifySimple( Gia_Man_t * p ) +{ + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Cec_ManCecSetDefaultParams( pPars ); + pPars->fSilent = 1; + assert( Gia_ManCoNum(p) == 2 ); + assert( Gia_ManRegNum(p) == 0 ); + return Cec_ManVerify( p, pPars ); +} + +/**Function************************************************************* + Synopsis [New CEC engine applied to two circuits.] Description [] |