diff options
-rw-r--r-- | src/aig/bdc/bdcSpfd.c | 11 | ||||
-rw-r--r-- | src/aig/llb/llb4Cex.c | 18 | ||||
-rw-r--r-- | src/aig/llb/llb4Nonlin.c | 2 | ||||
-rw-r--r-- | src/aig/llb/llbInt.h | 2 |
4 files changed, 21 insertions, 12 deletions
diff --git a/src/aig/bdc/bdcSpfd.c b/src/aig/bdc/bdcSpfd.c index 1ffc6fc7..25790983 100644 --- a/src/aig/bdc/bdcSpfd.c +++ b/src/aig/bdc/bdcSpfd.c @@ -811,22 +811,21 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights ) void Bdc_SpfdDecomposeTest() { // word t = 0x5052585a0002080a; - word t = 0x9ef7a8d9c7193a0f; // word t = 0x6BFDA276C7193A0F; // word t = 0xA3756AFE0B1DF60B; - int clk = clock(); -// Vec_Int_t * vWeights; -// Vec_Wrd_t * vDivs = Bdc_SpfdDecomposeTest__( &vWeights ); Vec_Int_t * vWeights; - Vec_Wrd_t * vDivs = Bdc_SpfdReadFiles( &vWeights ); - + Vec_Wrd_t * vDivs; word c0, c1, s, tt, ttt, tbest; int i, j, k, n, Cost, CostBest = 100000; + int clk = clock(); return; + // vDivs = Bdc_SpfdDecomposeTest__( &vWeights ); + vDivs = Bdc_SpfdReadFiles( &vWeights ); + Abc_Show6VarFunc( ~t, t ); /* for ( i = 0; i < 6; i++ ) diff --git a/src/aig/llb/llb4Cex.c b/src/aig/llb/llb4Cex.c index 6c4cedfb..603c6e59 100644 --- a/src/aig/llb/llb4Cex.c +++ b/src/aig/llb/llb4Cex.c @@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose ) +Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose ) { Abc_Cex_t * pCex; Cnf_Dat_t * pCnf; @@ -124,8 +124,18 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int // add the last frame when the property fails Vec_IntClear( vAssumps ); - Saig_ManForEachPo( pAig, pObj, k ) - Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + if ( iCexPo >= 0 ) + { + Saig_ManForEachPo( pAig, pObj, k ) + if ( k == iCexPo ) + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + } + else + { + Saig_ManForEachPo( pAig, pObj, k ) + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + } + // add clause status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) ); if ( status == 0 ) @@ -292,7 +302,7 @@ Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm, return NULL; } // derive updated counter-example - pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, 0 ); + pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, pCexRpm->iPo, 0 ); Vec_PtrFree( vStates ); return pCexOrg; } diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c index 69d741a5..0d78b15a 100644 --- a/src/aig/llb/llb4Nonlin.c +++ b/src/aig/llb/llb4Nonlin.c @@ -742,7 +742,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) Vec_Ptr_t * vStates; assert( p->pAig->pSeqModel == NULL ); vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose ); - p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, p->pPars->fVerbose ); + p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose ); Vec_PtrFreeP( &vStates ); if ( !p->pPars->fSilent ) { diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 93165159..4bc2496d 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -186,7 +186,7 @@ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * /*=== llb4Cex.c =======================================================*/ -extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose ); +extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose ); /*=== llb4Cluster.c =======================================================*/ //extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ); /*=== llb4Image.c =======================================================*/ |