diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 15:52:26 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 15:52:26 -0500 |
| commit | 88c273c25e3bbf9f5117d06fb8dbb1108c6c0225 (patch) | |
| tree | 10b86fa2aaf6b440f80b7964ddef2941c0d868cc /src/aig/gia/giaSweeper.c | |
| parent | ceca5da3e9fba95ed5d01e3f7b53ad585cc87f0b (diff) | |
| download | abc-88c273c25e3bbf9f5117d06fb8dbb1108c6c0225.tar.gz abc-88c273c25e3bbf9f5117d06fb8dbb1108c6c0225.tar.bz2 abc-88c273c25e3bbf9f5117d06fb8dbb1108c6c0225.zip | |
User-controlable SAT sweeper.
Diffstat (limited to 'src/aig/gia/giaSweeper.c')
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 88ae44b6..e08f0ab9 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -193,6 +193,7 @@ void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ) Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p ) { Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; + assert( pSwp->vCexUser == NULL || Vec_IntSize(pSwp->vCexUser) == Gia_ManPiNum(p) ); return pSwp->vCexUser; } @@ -605,6 +606,11 @@ static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_sol Gia_ManForEachPi( pGia, pObj, i ) { LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) ); + if ( LitSat == 0 ) + { + Vec_IntPush( vCex, 2 ); + continue; + } assert( LitSat > 0 ); Value = sat_solver_var_value(pSat, Abc_Lit2Var(LitSat)) ^ Abc_LitIsCompl(LitSat); Vec_IntPush( vCex, Value ); |