From ddb22f3bed7cb457576b4b80e55d47eabf3a1308 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2022 14:21:47 -0700 Subject: Various changes. --- src/proof/cec/cecChoice.c | 1 - 1 file changed, 1 deletion(-) (limited to 'src/proof/cec') diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index db0059fd..13923511 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -418,7 +418,6 @@ Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose ) Aig_Man_t * pAig; Cec4_ManSimulateTest2( pGia, nConfs, fVerbose ); pGia = Gia_ManEquivToChoices( pGia, 3 ); - Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); pAig = Gia_ManToAig( pGia, 1 ); Gia_ManStop( pGia ); return pAig; -- cgit v1.2.3 From b69f439609c248db1f17408d550693fec30cbea5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 10:48:41 -0700 Subject: Adding args to command %yosys. --- src/proof/cec/cecClass.c | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'src/proof/cec') diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c index be88b9be..60fdbc89 100644 --- a/src/proof/cec/cecClass.c +++ b/src/proof/cec/cecClass.c @@ -265,10 +265,13 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) SeeAlso [] ***********************************************************************/ -int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) +static int s_Count = 0; + +int Cec_ManSimClassRefineOne_rec( Cec_ManSim_t * p, int i ) { unsigned * pSim0, * pSim1; int Ent; + s_Count++; Vec_IntClear( p->vClassOld ); Vec_IntClear( p->vClassNew ); Vec_IntPush( p->vClassOld, i ); @@ -290,9 +293,22 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) Cec_ManSimClassCreate( p->pAig, p->vClassOld ); Cec_ManSimClassCreate( p->pAig, p->vClassNew ); if ( Vec_IntSize(p->vClassNew) > 1 ) - return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) ); + return 1 + Cec_ManSimClassRefineOne_rec( p, Vec_IntEntry(p->vClassNew,0) ); return 1; } +int Cec_ManSimClassRefineOne_( Cec_ManSim_t * p, int i ) +{ + int Res; + s_Count = 0; + Res = Cec_ManSimClassRefineOne_rec( p, i ); + if ( s_Count > 10 ) + printf( "%d ", s_Count ); + return Res; +} +int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) +{ + return Cec_ManSimClassRefineOne_rec( p, i ); +} /**Function************************************************************* -- cgit v1.2.3