diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-15 19:56:34 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-15 19:56:34 -0700 |
| commit | 1343b8a80c7c59c7cc2b14490151de4e5d883734 (patch) | |
| tree | e6ee59cb7053ab04b941069248b684da56ecf209 /src | |
| parent | 3f8b5cd890e788fcc17ff382d80a8c4a48b16a06 (diff) | |
| download | abc-1343b8a80c7c59c7cc2b14490151de4e5d883734.tar.gz abc-1343b8a80c7c59c7cc2b14490151de4e5d883734.tar.bz2 abc-1343b8a80c7c59c7cc2b14490151de4e5d883734.zip | |
Fixes and adjustments for the edge computation flow.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaSatLE.c | 3 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/aig/gia/giaSatLE.c b/src/aig/gia/giaSatLE.c index c1588571..ec243423 100644 --- a/src/aig/gia/giaSatLE.c +++ b/src/aig/gia/giaSatLE.c @@ -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 ); } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 9d885701..88a05093 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -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 ); |