diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-14 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-14 08:01:00 -0700 |
| commit | a4bca405978e500b7ef2b987d159e3b11b95905f (patch) | |
| tree | e94a9b0c2c252ffdd0f56d287e71526aba53aa36 /src/aig/ssw/sswSat.c | |
| parent | e917dda1d363cf56274d0595c97cecf3c59eca75 (diff) | |
| download | abc-a4bca405978e500b7ef2b987d159e3b11b95905f.tar.gz abc-a4bca405978e500b7ef2b987d159e3b11b95905f.tar.bz2 abc-a4bca405978e500b7ef2b987d159e3b11b95905f.zip | |
Version abc81014
Diffstat (limited to 'src/aig/ssw/sswSat.c')
| -rw-r--r-- | src/aig/ssw/sswSat.c | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index fc902560..2fd0fba3 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -44,6 +44,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) int nBTLimit = p->pPars->nBTLimit; int pLits[3], nLits, RetValue, RetValue1, clk;//, status; p->nSatCalls++; + p->pMSat->nSolverCalls++; // sanity checks assert( !Aig_IsComplement(pOld) ); @@ -231,7 +232,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // consider the constant 1 case if ( pOld == Aig_ManConst1(p->pFrames) ) { - // add constaint A = 1 ----> A + // add constraint A = 1 ----> A pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew ); if ( p->pPars->fPolarFlip ) { @@ -242,7 +243,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } else { - // add constaint A = B ----> (A v !B)(!A v B) + // add constraint A = B ----> (A v !B)(!A v B) // (A v !B) pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 ); |