diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-07-19 21:01:06 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-07-19 21:01:06 -0700 |
commit | 3d01abf481c0115beb5f2aea48ea9007a3e29c39 (patch) | |
tree | b0c60b6cbd06b76b4745d675a19af7a01591cb33 /src/proof/pdr/pdrSat.c | |
parent | 35273eaebaf9b8594c30898dad055578dfa81538 (diff) | |
download | abc-3d01abf481c0115beb5f2aea48ea9007a3e29c39.tar.gz abc-3d01abf481c0115beb5f2aea48ea9007a3e29c39.tar.bz2 abc-3d01abf481c0115beb5f2aea48ea9007a3e29c39.zip |
Experiment with 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdrSat.c')
-rw-r--r-- | src/proof/pdr/pdrSat.c | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 663a0e2f..31c05ce6 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -57,9 +57,8 @@ 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_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); Saig_ManForEachPo( p->pAig, pObj, i ) - Pdr_ObjSatVar( p, k, pObj ); + Pdr_ObjSatVar( p, k, 1, pObj ); return pSat; } @@ -146,6 +145,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom int i, iVar, iVarMax = 0; abctime clk = Abc_Clock(); Vec_IntClear( p->vLits ); + assert( !(fNext && fCompl) ); for ( i = 0; i < pCube->nLits; i++ ) { if ( pCube->Lits[i] == -1 ) @@ -154,7 +154,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) ); else pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) ); - iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 ); iVarMax = Abc_MaxInt( iVarMax, iVar ); Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) ); } @@ -185,7 +185,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; - Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal + Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); assert( RetValue == 1 ); } @@ -235,7 +235,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t pSat = Pdr_ManSolver(p, k); Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i ) { - iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 ); + iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 ); Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); } } @@ -293,7 +293,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 = Abc_Clock(); - Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails) + Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails) Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); sat_solver_set_runtime_limit( pSat, Limit ); |