diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 01:25:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 01:25:29 -0700 |
| commit | b09926e8e26de8df20a3973a3c9a1c63b06952cb (patch) | |
| tree | cd38678012538f93611262f680e00d7f12a83ba4 /src/proof/ssc/sscCore.c | |
| parent | 17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a (diff) | |
| download | abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.tar.gz abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.tar.bz2 abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.zip | |
SAT sweeping under constraints.
Diffstat (limited to 'src/proof/ssc/sscCore.c')
| -rw-r--r-- | src/proof/ssc/sscCore.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index 00491e31..b29a0193 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -313,6 +313,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) pAig = Gia_ManDupLevelized( pResult = pAig ); Gia_ManStop( pResult ); pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); + if ( pPars->fAppend ) + { + Gia_ManDupAppendShare( pResult, pCare ); + pResult->nConstrs = Gia_ManPoNum(pCare); + } Gia_ManStop( pAig ); Gia_ManStop( pCare ); return pResult; |