From c46c957a0721004eb21c5f3d3f316ba1c8ab8df1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 9 Mar 2012 19:50:18 -0800 Subject: Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)... --- src/proof/pdr/pdrSat.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/proof/pdr/pdrSat.c') diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index c191654a..de661905 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -55,7 +55,7 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) Vec_VecExpand( p->vClauses, k ); Vec_IntPush( p->vActVars, 0 ); // add property cone - Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); + Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); return pSat; } @@ -175,7 +175,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) sat_solver * pSat; int Lit, RetValue; pSat = Pdr_ManSolver(p, k); - Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal + Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); assert( RetValue == 1 ); sat_solver_compress( pSat ); @@ -278,7 +278,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr if ( pCube == NULL ) // solve the property { clk = clock(); - Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails) + Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails) RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); if ( RetValue == l_Undef ) return -1; -- cgit v1.2.3