diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-30 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-30 08:01:00 -0700 |
| commit | fefd8b901d89ad0d977db8896c12123cc747e3d7 (patch) | |
| tree | 1e35b5d52cafdff284e08163136d9a61e1a09235 /src/aig/fra/fraSat.c | |
| parent | a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f (diff) | |
| download | abc-fefd8b901d89ad0d977db8896c12123cc747e3d7.tar.gz abc-fefd8b901d89ad0d977db8896c12123cc747e3d7.tar.bz2 abc-fefd8b901d89ad0d977db8896c12123cc747e3d7.zip | |
Version abc70730
Diffstat (limited to 'src/aig/fra/fraSat.c')
| -rw-r--r-- | src/aig/fra/fraSat.c | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 418e9fee..a728d860 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -44,6 +44,7 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); + int status; // make sure the nodes are not complemented assert( !Aig_IsComplement(pNew) ); @@ -54,7 +55,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit nBTLimit = p->pPars->nBTLimitNode; - if ( !p->pPars->fSpeculate && p->pPars->nTimeFrames == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) + if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) { p->nSatFails++; // fail immediately @@ -77,6 +78,13 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // if the nodes do not have SAT variables, allocate them Fra_NodeAddToSolver( p, pOld, pNew ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + // prepare variable activity if ( p->pPars->fConeBias ) Fra_SetActivityFactors( p, pOld, pNew ); |