diff options
Diffstat (limited to 'src/aig/gia/giaSweeper.c')
-rw-r--r-- | src/aig/gia/giaSweeper.c | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 4cad0bdc..838b9978 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -784,7 +784,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) { iLitAig = Gia_SweeperProbeLit( pGia, ProbeId ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) ); - Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) ); + Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) ); } Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) ); @@ -969,6 +969,27 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * /**Function************************************************************* + Synopsis [Verification of the sweeper.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC ) +{ + Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 ); + Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 ); + + Gia_ManStop( pConstr ); + Gia_ManStop( pMiter ); + return 1; +} + +/**Function************************************************************* + Synopsis [Performs conditional sweeping of the cone.] Description [Returns the result as a new GIA manager with as many inputs @@ -995,7 +1016,7 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); Gia_ManSetPhase( pGiaOuts ); - // if there is no conditions, define constant true constrain (constant 0 output) + // if there is no conditions, define constant true constraint (constant 0 output) if ( Gia_ManPoNum(pGiaCond) == 0 ) Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() ); // perform sweeping under constraints |