Commit 3552d39b by Alan Mishchenko

Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.

parent d80f43a1
...@@ -137,6 +137,13 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap ) ...@@ -137,6 +137,13 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
*pvMap = Vec_IntAlloc( 100 ); *pvMap = Vec_IntAlloc( 100 );
Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkForEachPo( pNtk, pObj, i )
{ {
if ( pNtk->nConstrs && i >= pNtk->nConstrs )
{
Vec_PtrPush( vDrivers, Abc_ObjNot(Abc_ObjChild0(pObj)) );
if ( pvMap )
Vec_IntPush( *pvMap, i );
continue;
}
Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper ); Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k ) Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment