diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 16 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 6 | ||||
| -rw-r--r-- | src/proof/pdr/pdr.h | 4 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 258 | ||||
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 2 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 5 | ||||
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 20 | ||||
| -rw-r--r-- | src/proof/pdr/pdrTsim.c | 5 |
8 files changed, 183 insertions, 133 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 22e018ab..e7fe63e9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -22321,10 +22321,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCRTrmsdgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF ) { switch ( c ) { +/* case 'O': if ( globalUtilOptind >= argc ) { @@ -22336,6 +22337,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->iOutput < 0 ) goto usage; break; +*/ case 'M': if ( globalUtilOptind >= argc ) { @@ -22391,6 +22393,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nTimeOut < 0 ) goto usage; break; + case 'a': + pPars->fSolveAll ^= 1; + break; case 'r': pPars->fTwoRounds ^= 1; break; @@ -22432,12 +22437,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); return 0; } +/* if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) ) { Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n", pPars->iOutput, Abc_NtkPoNum(pNtk)-1 ); return 0; } +*/ +/* if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose ) { if ( pPars->iOutput == -1 ) @@ -22446,6 +22454,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n", pPars->iOutput, Abc_NtkPoNum(pNtk) ); } +*/ // run the procedure pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); pAbc->nFrames = pPars->iFrame; @@ -22453,16 +22462,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-OMFCRT<num] [-rmsdgvwh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); - Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" ); +// Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" ); Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle ); Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index cc703490..e427524a 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2717,6 +2717,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Converting network into AIG has failed.\n" ); return -1; } +/* // perform ORing the primary outputs if ( pPars->iOutput == -1 ) { @@ -2728,6 +2729,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) } else RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); +*/ + RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); + // output the result if ( !pPars->fSilent ) { @@ -2739,7 +2743,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Property UNDECIDED. " ); else assert( 0 ); - ABC_PRT( "Time", clock() - clk ); + ABC_PRT( "Time", clock() - clk ); } if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 491477dd..3c40d2d5 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -40,7 +40,7 @@ ABC_NAMESPACE_HEADER_START typedef struct Pdr_Par_t_ Pdr_Par_t; struct Pdr_Par_t_ { - int iOutput; // zero-based number of primary output to solve +// int iOutput; // zero-based number of primary output to solve int nRecycle; // limit on vars for recycling int nFrameMax; // limit on frame count int nConfLimit; // limit on SAT solver conflicts @@ -54,6 +54,8 @@ struct Pdr_Par_t_ int fVerbose; // verbose output` int fVeryVerbose; // very verbose output int fSilent; // totally silent execution + int fSolveAll; // do not stop when found a SAT output + int nFailOuts; // the number of failed outputs int iFrame; // explored up to this frame int RunId; // PDR id in this run int(*pFuncStop)(int); // callback to terminate diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index ca2ca5a0..f72983da 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) { memset( pPars, 0, sizeof(Pdr_Par_t) ); - pPars->iOutput = -1; // zero-based output number +// pPars->iOutput = -1; // zero-based output number pPars->nRecycle = 300; // limit on vars for recycling pPars->nFrameMax = 10000; // limit on number of timeframes pPars->nTimeOut = 0; // timeout in seconds @@ -552,7 +552,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { int fPrintClauses = 0; Pdr_Set_t * pCube; + Aig_Obj_t * pObj; int k, RetValue = -1; + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); clock_t clkStart = clock(); p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); @@ -562,87 +564,132 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { p->nFrames = k; assert( k == Vec_PtrSize(p->vSolvers)-1 ); - RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); - if ( RetValue == -1 ) - { - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - if ( p->pPars->nConfLimit ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); - else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; - return -1; - } - if ( RetValue == 0 ) + Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { - RetValue = Pdr_ManBlockCube( p, pCube ); - if ( RetValue == -1 ) + // skip solved outputs + if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) ) + continue; + // check if the output is trivially solved + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) + continue; + // check if the output is trivially solved + if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) ) { - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - if ( p->pPars->nConfLimit ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); - else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; - return -1; + if ( !p->pPars->fSolveAll ) + { + p->pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ); + return 0; // SAT + } + p->pPars->nFailOuts++; + Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + if ( p->vCexes == NULL ) + p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); + assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); + if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) + return 0; // all SAT + continue; } - if ( RetValue == 0 ) + // try to solve this output + while ( 1 ) { - if ( fPrintClauses ) + RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); + if ( RetValue == 1 ) + break; + if ( RetValue == -1 ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); - Pdr_ManPrintClauses( p, 0 ); + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback.\n" ); + p->pPars->iFrame = k; + return -1; } - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - p->pPars->iFrame = k; - return 0; // SAT - } - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 0, clock() - clkStart ); + if ( RetValue == 0 ) + { + RetValue = Pdr_ManBlockCube( p, pCube ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback.\n" ); + p->pPars->iFrame = k; + return -1; + } + if ( RetValue == 0 ) + { + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + p->pPars->iFrame = k; + + if ( !p->pPars->fSolveAll ) + { + p->pAig->pSeqModel = Pdr_ManDeriveCex( p ); + return 0; // SAT + } + p->pPars->nFailOuts++; + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + if ( p->vCexes == NULL ) + p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); + assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); + if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) + return 0; // all SAT + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 0, clock() - clkStart ); + } + } } - else + + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + // open a new timeframe + p->nQueLim = p->pPars->nRestLimit; + assert( pCube == NULL ); + Pdr_ManSetPropertyOutput( p, k ); + Pdr_ManCreateSolver( p, ++k ); + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + // push clauses into this timeframe + RetValue = Pdr_ManPushClauses( p ); + if ( RetValue == -1 ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - // open a new timeframe - p->nQueLim = p->pPars->nRestLimit; - assert( pCube == NULL ); - Pdr_ManSetPropertyOutput( p, k ); - Pdr_ManCreateSolver( p, ++k ); - if ( fPrintClauses ) - { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); - Pdr_ManPrintClauses( p, 0 ); - } - // push clauses into this timeframe - RetValue = Pdr_ManPushClauses( p ); - if ( RetValue == -1 ) - { - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); - p->pPars->iFrame = k; - return -1; - } - if ( RetValue ) - { - if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - if ( !p->pPars->fSilent ) - Pdr_ManReportInvariant( p ); - if ( !p->pPars->fSilent ) - Pdr_ManVerifyInvariant( p ); - p->pPars->iFrame = k; - return 1; // UNSAT - } + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + p->pPars->iFrame = k; + return -1; + } + if ( RetValue ) + { if ( p->pPars->fVerbose ) - Pdr_ManPrintProgress( p, 0, clock() - clkStart ); -// clkStart = clock(); + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( !p->pPars->fSilent ) + Pdr_ManReportInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManVerifyInvariant( p ); + p->pPars->iFrame = k; + return 1; // UNSAT } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 0, clock() - clkStart ); // check termination if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) @@ -688,72 +735,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex ) +int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) { Pdr_Man_t * p; int RetValue; clock_t clk = clock(); - p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL ); + if ( pPars->fVerbose ) + { +// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); + Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", + pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut ); + Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", + pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" ); + } + ABC_FREE( pAig->pSeqModel ); + p = Pdr_ManStart( pAig, pPars, NULL ); RetValue = Pdr_ManSolveInt( p ); - if ( ppCex ) - *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); +// if ( ppCex ) +// *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p ); + if ( RetValue == 0 ) + assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); + if ( p->vCexes ) + { + assert( p->pAig->vSeqModelVec == NULL ); + p->pAig->vSeqModelVec = p->vCexes; + p->vCexes = NULL; + } if ( p->pPars->fDumpInv ) Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 ); // if ( *ppCex && pPars->fVerbose ) // Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n", // (*ppCex)->iFrame, p->nFrames ); p->tTotal += clock() - clk; - if ( pvPrioInit ) - { - *pvPrioInit = p->vPrio; - p->vPrio = NULL; - } Pdr_ManStop( p ); pPars->iFrame--; return RetValue; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) -{ - if ( pPars->fVerbose ) - { -// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); - Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", - pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut ); - if ( pPars->iOutput >= 0 ) - Abc_Print( 1, "Output = %d. ", pPars->iOutput ); - Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", - pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" ); - } - -/* - Vec_Int_t * vPrioInit = NULL; - int RetValue, nTimeOut; - if ( pPars->nTimeOut > 0 ) - return Pdr_ManSolve_( pAig, pPars, NULL, ppCex ); - nTimeOut = pPars->nTimeOut; - pPars->nTimeOut = 10; - RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex ); - pPars->nTimeOut = nTimeOut; - if ( RetValue == -1 ) - RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex ); - Vec_IntFree( vPrioInit ); - return RetValue; -*/ - return Pdr_ManSolve_( pAig, pPars, NULL, ppCex ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 36cea069..abc8f12b 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -76,6 +76,8 @@ struct Pdr_Man_t_ Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId // data representation + int iOutCur; // current output + Vec_Ptr_t * vCexes; // counter-examples for each output Vec_Ptr_t * vSolvers; // SAT solvers Vec_Vec_t * vClauses; // clauses by timeframe Pdr_Obl_t * pQueue; // proof obligations diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 41941a37..78aa2b69 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -144,6 +144,8 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_IntFree( p->vRes ); // final result Vec_IntFree( p->vSuppLits ); // support literals ABC_FREE( p->pCubeJust ); + if ( p->vCexes ) + Vec_PtrFreeFree( p->vCexes ); // additional AIG data-members if ( p->pAig->pFanData != NULL ) Aig_ManFanoutStop( p->pAig ); @@ -173,7 +175,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) nFrames++; // create the counter-example pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); - pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; +// pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; + pCex->iPo = p->iOutCur; pCex->iFrame = nFrames-1; for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 50402ee5..f0aff8bb 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -45,6 +45,8 @@ ABC_NAMESPACE_IMPL_START sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) { sat_solver * pSat; + Aig_Obj_t * pObj; + int i; assert( Vec_PtrSize(p->vSolvers) == k ); assert( Vec_VecSize(p->vClauses) == k ); assert( Vec_IntSize(p->vActVars) == k ); @@ -55,7 +57,9 @@ 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 ) ); +// 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 ); return pSat; } @@ -173,11 +177,15 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) { sat_solver * pSat; - int Lit, RetValue; + Aig_Obj_t * pObj; + int Lit, RetValue, i; pSat = Pdr_ManSolver(p, k); - 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 ); + Saig_ManForEachPo( p->pAig, pObj, i ) + { + Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal + RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue == 1 ); + } sat_solver_compress( pSat ); } @@ -279,7 +287,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_ManCo(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->iOutCur)) ); // pos literal (property fails) RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); if ( RetValue == l_Undef ) return -1; diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index fa65edea..fcd17fad 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -368,7 +368,10 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) // collect CO objects Vec_IntClear( vCoObjs ); if ( pCube == NULL ) // the target is the property output - Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); + { +// Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); + Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) ); + } else // the target is the cube { for ( i = 0; i < pCube->nLits; i++ ) |