diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-07-09 11:59:52 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-07-09 11:59:52 -0700 |
| commit | ea1e369fc296935ea7a9265a612e756d35086d5c (patch) | |
| tree | 171fcdf101e2d10bf76093480f0fdd365a74bb88 /src/aig/gia/giaFalse.c | |
| parent | b389f2054b90c9d3e53cce057b36758968a1e910 (diff) | |
| download | abc-ea1e369fc296935ea7a9265a612e756d35086d5c.tar.gz abc-ea1e369fc296935ea7a9265a612e756d35086d5c.tar.bz2 abc-ea1e369fc296935ea7a9265a612e756d35086d5c.zip | |
Improvements to false path detection.
Diffstat (limited to 'src/aig/gia/giaFalse.c')
| -rw-r--r-- | src/aig/gia/giaFalse.c | 46 |
1 files changed, 21 insertions, 25 deletions
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c index 0d609436..c3f26455 100644 --- a/src/aig/gia/giaFalse.c +++ b/src/aig/gia/giaFalse.c @@ -390,34 +390,30 @@ Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, in // add CNF for the path Gia_ManForEachObjVec( vPath, p, pObj, i ) { - if ( Gia_ObjIsAnd(pObj) ) + if ( !Gia_ObjIsAnd(pObj) ) + continue; + assert( i > 0 ); + pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) ); + if ( pFanin == Gia_ObjFanin0(pObj) ) { - assert( i > 0 ); - pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) ); - if ( pFanin == Gia_ObjFanin0(pObj) ) - { - sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), - i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0], - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), - i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1], - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - } - else if ( pFanin == Gia_ObjFanin1(pObj) ) - { - sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), - Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath), - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), - Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath), - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - } - else assert( 0 ); - sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 ); + sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), + i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0], + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), + i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1], + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + } + else if ( pFanin == Gia_ObjFanin1(pObj) ) + { + sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath), + Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath), + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath), + Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath), + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); } - else if ( Gia_ObjIsCi(pObj) ) - sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 ); else assert( 0 ); + sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 ); Vec_IntPush( vLits, Abc_Var2Lit(i, 0) ); } // call the SAT solver |