diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 00:06:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 00:06:31 -0800 |
| commit | 06094ade87fbec6000619bf007aaad596e8bc0a2 (patch) | |
| tree | fc05149c4488137f0ccdde3373602d8d3f4327ac /src/proof/cec/cecCore.c | |
| parent | 901560bb238f8c4e4dafc4d2489eaa77df4defb3 (diff) | |
| download | abc-06094ade87fbec6000619bf007aaad596e8bc0a2.tar.gz abc-06094ade87fbec6000619bf007aaad596e8bc0a2.tar.bz2 abc-06094ade87fbec6000619bf007aaad596e8bc0a2.zip | |
Adding switch to replace proved outputs by const0.
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 8 |
1 files changed, 4 insertions, 4 deletions
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 ) ) { |