diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
| commit | 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (patch) | |
| tree | fe4ae0c41d0481c1c3f9eec7689f49cba58cd4e8 /src/aig/ivy | |
| parent | 73c8aa7c400bab320cea56529241e1d396f1e0f5 (diff) | |
| download | abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.gz abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.bz2 abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.zip | |
Version abc80905
Diffstat (limited to 'src/aig/ivy')
| -rw-r--r-- | src/aig/ivy/ivyFraig.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index c306c394..25f7a3ef 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk; int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) { int pLits[2], RetValue1, clk; -// int RetValue; + int RetValue; // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); @@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk; { p->timeSatUnsat += clock() - clk; pLits[0] = lit_neg( pLits[0] ); -// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); -// assert( RetValue ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + assert( RetValue ); // continue solving the other implication p->nSatCallsUnsat++; } @@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * Ivy_ObjSetFaninVec( pNode, vFanins ); } Vec_PtrFree( vFrontier ); + sat_solver_simplify( p->pSat ); } /**Function************************************************************* |