summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/aig/bdc/bdcSpfd.c11
-rw-r--r--src/aig/llb/llb4Cex.c18
-rw-r--r--src/aig/llb/llb4Nonlin.c2
-rw-r--r--src/aig/llb/llbInt.h2
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 =======================================================*/