Commit 1343b8a8 by Alan Mishchenko

Fixes and adjustments for the edge computation flow.

parent 3f8b5cd8
......@@ -881,7 +881,7 @@ void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMappin
if ( !sat_solver_var_value(p->pSat, iObj) )
continue;
Vec_IntForEachEntry( vCutFans, iFanin, i )
if ( sat_solver_var_value(p->pSat, iEdgeVar0 + i) )
if ( sat_solver_var_value(p->pSat, iFanin) && sat_solver_var_value(p->pSat, iEdgeVar0 + i) )
Vec_IntPushTwo( vEdge2, iFanin, iObj );
}
}
......@@ -1029,6 +1029,7 @@ void Sle_ManExplore( Gia_Man_t * pGia, int nBTLimit, int DelayInit, int fDynamic
Vec_IntFree( vEdges2 );
Vec_IntFree( vMapping );
}
Vec_IntFreeP( &p->pGia->vPacking );
Sle_ManStop( p );
}
......
......@@ -1019,7 +1019,7 @@ sat_solver* sat_solver_new(void)
sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
// Vec_SetAlloc_(&s->Mem, 15);
Sat_MemAlloc_(&s->Mem, 15);
Sat_MemAlloc_(&s->Mem, 17);
s->hLearnts = -1;
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
s->binary = clause_read( s, s->hBinary );
......
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