From 06094ade87fbec6000619bf007aaad596e8bc0a2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 16 Dec 2020 00:06:31 -0800 Subject: Adding switch to replace proved outputs by const0. --- src/proof/cec/cec.h | 2 +- src/proof/cec/cecChoice.c | 2 +- src/proof/cec/cecCore.c | 8 ++++---- src/proof/cec/cecCorr.c | 2 +- src/proof/cec/cecInt.h | 2 +- src/proof/cec/cecSolve.c | 7 +++++-- 6 files changed, 13 insertions(+), 10 deletions(-) (limited to 'src/proof') diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 3414842c..791955e4 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -219,7 +219,7 @@ extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ); extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ); extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent ); -extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); +extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved ); extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); /*=== cecSeq.c ==========================================================*/ extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ); diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 47d6a478..780a1196 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) // found counter-examples to speculation clk2 = Abc_Clock(); if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); Gia_ManStop( pSrm ); diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 51debba6..4e8e5497 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -232,14 +232,14 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved ) { Gia_Man_t * pNew; Cec_ManPat_t * pPat; pPat = Cec_ManPatStart(); - Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL ); + Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved ); // pNew = Gia_ManDupDfsSkip( pAig ); - pNew = Gia_ManDup( pAig ); + pNew = Gia_ManCleanup( pAig ); Cec_ManPatStop( pPat ); pNew->vSeqModelVec = pAig->vSeqModelVec; pAig->vSeqModelVec = NULL; @@ -445,7 +445,7 @@ clk = Abc_Clock(); if ( pPars->fRunCSat ) Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); else - Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); + Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv, 0 ); p->timeSat += Abc_Clock() - clk; if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) { diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 8f708910..ce7e0885 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -996,7 +996,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // found counter-examples to speculation clk2 = Abc_Clock(); if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); Gia_ManStop( pSrm ); diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index d5456897..80663db9 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -204,7 +204,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); -extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ); +extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved ); extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index af6a4fdb..f8342859 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -696,7 +696,7 @@ Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut ) } return pCex; } -void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) +void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved ) { Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; @@ -747,6 +747,9 @@ clk2 = Abc_Clock(); if ( pPars->fSaveCexes && status != -1 ) Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) ); + if ( f0Proved && status == 1 ) + Gia_ManPatchCoDriver( pAig, i, 0 ); + /* if ( status == -1 ) { @@ -807,7 +810,7 @@ void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * { Vec_Str_t * vStatus; Vec_Int_t * vPat = Vec_IntAlloc( 1000 ); - Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 ); + Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0, 0 ); Gia_Obj_t * pObj; int i, status, iStart = 0; assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) ); -- cgit v1.2.3