From 760c1f60d2dc0f980053e666b53dfb7390f85823 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 May 2013 11:50:16 -0700 Subject: Adding new command &mprove for proving groups of properties. --- src/aig/gia/gia.h | 3 + src/aig/gia/giaUtil.c | 89 ++++++++++++++++++++++++++++++ src/base/abci/abc.c | 138 +++++++++++++++++++++++++++++++++++++++++----- src/base/main/main.h | 6 ++ src/base/main/mainFrame.c | 2 + src/base/main/mainInt.h | 1 + src/proof/pdr/pdr.h | 2 +- src/proof/pdr/pdrCore.c | 19 ++++--- src/proof/pdr/pdrMan.c | 6 +- 9 files changed, 240 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index ed38806e..d9d885e3 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -372,6 +372,9 @@ static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; } static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); } +static inline int Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); } +static inline int Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); } + static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) ); } static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5288bf35..cb97e0bf 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1393,6 +1393,95 @@ void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues ) pObj->Value = Vec_IntEntry(vValues, i); } + +#include "base/main/mainInt.h" + +/**Function************************************************************* + + Synopsis [Proving multi-output properties.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose ) +{ + Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame(); + Gia_Man_t * p = Gia_ManDup( pInit ); + Gia_Man_t * pGroup; + Vec_Int_t * vOuts; + Vec_Int_t * vOutMap; + Vec_Ptr_t * vCexes; + int i, k, nGroupCur, nGroups; + clock_t clk, timeComm = 0; + clock_t timeStart = clock(); + // pre-conditions + assert( nGroupSize > 0 ); + assert( pCommLine != NULL ); + assert( p->nConstrs == 0 ); + Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine ); + // create output map + vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) ); + vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) ); + vCexes = Vec_PtrAlloc( Gia_ManPoNum(p) ); + nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0); + for ( i = 0; i < nGroups; i++ ) + { + // derive the group + nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize; + pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 ); + Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur ); + // set the current GIA + Abc_FrameUpdateGia( pAbc, pGroup ); + // solve the group + clk = clock(); + Cmd_CommandExecute( pAbc, pCommLine ); + timeComm += clock() - clk; + // get the solution status + if ( nGroupSize == 1 ) + { + Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) ); + Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) ); + } + else // if ( nGroupSize > 1 ) + { + Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc ); + Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc ); + assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr" + assert( vCexesCur != NULL ); + for ( k = 0; k < nGroupCur; k++ ) + { + Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) ); + Vec_PtrPush( vCexes, Vec_PtrEntry(vCexesCur, k) ); + } + } + } + assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) ); + assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) ); + // set CEXes + if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) ) + Abc_FrameReplaceCexVec( pAbc, &vCexes ); + else // there is no CEXes + Vec_PtrFree( vCexes ); + // report the result + Abc_Print( 1, "SUMMARY: " ); + Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) ); + Abc_Print( 1, "UNSAT = %6d. ", Vec_IntCountEntry(vOutMap, 1) ); + Abc_Print( 1, "SAT = %6d. ", Vec_IntCountEntry(vOutMap, 0) ); + Abc_Print( 1, "UNDEC = %6d. ", Vec_IntCountEntry(vOutMap, -1) ); + Abc_Print( 1, "\n" ); + Abc_PrintTime( 1, "Command time", timeComm ); + Abc_PrintTime( 1, "Total time ", clock() - timeStart ); + // cleanup + Vec_IntFree( vOuts ); + Gia_ManStop( p ); + return vOutMap; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6da8b17c..a30a2e55 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -382,6 +382,7 @@ static int Abc_CommandAbc9CexInfo ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -474,13 +475,57 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec ) ***********************************************************************/ void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs ) { - // update the array vector if ( pAbc->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs ); pAbc->vPoEquivs = *pvPoEquivs; *pvPoEquivs = NULL; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses ) +{ + if ( pAbc->vStatuses ) + Vec_IntFree( pAbc->vStatuses ); + pAbc->vStatuses = *pvStatuses; + *pvStatuses = NULL; +} + +/**Function************************************************************* + + Synopsis [Derives array of statuses from the array of CEXes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes ) +{ + Vec_Int_t * vStatuses; + Abc_Cex_t * pCex; + int i; + if ( vCexes == NULL ) + return NULL; + vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) ); + Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC + Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i ) + if ( pCex != NULL ) + Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT + return vStatuses; +} + /**Function************************************************************* Synopsis [] @@ -882,6 +927,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&cycle", Abc_CommandAbc9Cycle, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -21194,6 +21240,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Saig_ParBmc_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); Vec_Ptr_t * vSeqModelVec = NULL; + Vec_Int_t * vStatuses = NULL; char * pLogFileName = NULL; int fOrDecomp = 0; int c; @@ -21356,7 +21403,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); - pAbc->nFrames = pPars->iFrame; + pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); if ( pLogFileName ) Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" ); @@ -21380,11 +21427,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } } - if ( vSeqModelVec ) - { - Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); - pAbc->nFrames = -1; - } + vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); return 0; usage: @@ -22929,14 +22974,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the procedure pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); - pAbc->nFrames = pPars->iFrame; + pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); - if ( pNtk->vSeqModelVec ) - { - Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); - pAbc->nFrames = -1; - } - ABC_FREE( pPars->pOutMap ); // cleanup after PDR + Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); return 0; usage: @@ -30470,6 +30511,75 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose ); + Vec_Int_t * vStatus; + char * pCommLine = NULL; + int c, nGroupSize = 1, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "GSvh" ) ) != EOF ) + { + switch ( c ) + { + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + nGroupSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nGroupSize <= 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" ); + goto usage; + } + pCommLine = argv[globalUtilOptind]; + globalUtilOptind++; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); + return 1; + } + vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose ); + Vec_IntFree( vStatus ); + return 0; + +usage: + Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" ); + Abc_Print( -2, "\t proves multi-output testcase by splitting outputs into groups\n" ); + Abc_Print( -2, "\t (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" ); + Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize ); + Abc_Print( -2, "\t-S str : the command line to be executed for each group [default = %s]\n", pCommLine ? pCommLine : "none" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* diff --git a/src/base/main/main.h b/src/base/main/main.h index 34678479..722f5465 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -116,6 +116,7 @@ extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ); +extern ABC_DLL Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p ); extern ABC_DLL Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p ); @@ -138,6 +139,11 @@ extern ABC_DLL void Abc_FrameSetStatus( int Status ); extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum ); +extern ABC_DLL void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex ); +extern ABC_DLL void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec ); +extern ABC_DLL void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs ); +extern ABC_DLL void Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses ); + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index a525afb6..035a8df3 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -65,6 +65,7 @@ int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFr Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; } Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; } +Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; } Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; } int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; } @@ -177,6 +178,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) if ( p->vAbcObjIds) Vec_IntFree( p->vAbcObjIds ); if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec ); if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs ); + if ( p->vStatuses ) Vec_IntFree( p->vStatuses ); if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL ); if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec ); if ( p->dd ) Extra_StopManager( p->dd ); diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 2d5bf4c8..acd8bbd3 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -101,6 +101,7 @@ struct Abc_Frame_t_ Abc_Cex_t * pCex2; // copy of the above Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs + Vec_Int_t * vStatuses; // problem status for each output Vec_Int_t * vAbcObjIds; // object IDs int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1) int nFrames; // the number of time frames completed by BMC diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 97a71512..10d2af3b 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -67,7 +67,7 @@ struct Pdr_Par_t_ int(*pFuncStop)(int); // callback to terminate int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode clock_t timeLastSolved; // the time when the last output was solved - int * pOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) + Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index afcb45b4..f2ba7ba6 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -592,7 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); 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 ) @@ -684,7 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); @@ -719,7 +719,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) { p->pPars->nDropOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); // printf( "Dropping output %d.\n", p->iOutCur ); } } @@ -765,10 +765,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // count the number of UNSAT outputs p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' - if ( p->pPars->pOutMap ) + if ( p->pPars->vOutMap ) for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ ) - if ( p->pPars->pOutMap[k] == -2 ) // unknown - p->pPars->pOutMap[k] = 1; // unsat + if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown + Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat return p->vCexes ? 0 : 1; // UNSAT } if ( p->pPars->fVerbose ) @@ -836,7 +836,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; - int RetValue; + int k, RetValue; clock_t clk = clock(); if ( pPars->nTimeOutOne ) pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1; @@ -871,6 +871,11 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p->tTotal += clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; + // convert all -2 (unknown) entries into -1 (undec) + if ( pPars->vOutMap ) + for ( k = 0; k < Saig_ManPoNum(pAig); k++ ) + if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown + Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec return RetValue; } diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index ef930beb..36a62029 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -83,10 +83,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio } if ( pPars->fSolveAll ) { - int i; - pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) ); - for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) - pPars->pOutMap[i] = -2; // unknown + p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) ); + Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 ); } return p; } -- cgit v1.2.3