diff options
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 ); |