From bc39220df48d09ce7eb08c3839638b5030e31016 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 18 Jun 2013 17:46:37 -0700
Subject: [PATCH] Performance improvements in 'pdr'.
---
src/proof/pdr/pdrCore.c | 13 +++++++++----
src/proof/pdr/pdrInt.h | 1 +
2 files changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index d3084f2..009e9f5 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -136,6 +136,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
int Counter = 0;
abctime clk = Abc_Clock();
+ assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
{
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
@@ -427,7 +428,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
abctime clk;
p->nBlocks++;
// create first proof obligation
- assert( p->pQueue == NULL );
+// assert( p->pQueue == NULL );
pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
Pdr_QueuePush( p, pThis );
// try to solve it recursively
@@ -437,6 +438,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 )
return 0; // SAT
+ if ( pThis->iFrame > kMax ) // finished this level
+ return 1;
if ( p->nQueLim && p->nQueCur >= p->nQueLim )
{
p->nQueLim = p->nQueLim * 3 / 2;
@@ -446,6 +449,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
pThis = Pdr_QueuePop( p );
assert( pThis->iFrame > 0 );
assert( !Pdr_SetIsInit(pThis->pState, -1) );
+ p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame );
clk = Abc_Clock();
if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
@@ -458,7 +462,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
// check if the cube is already contained
RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
- if ( RetValue == -1 ) // cube is blocked by clauses in this frame
+ if ( RetValue == -1 ) // resource limit is reached
{
Pdr_OblDeref( pThis );
return -1;
@@ -472,7 +476,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
// check if the cube holds with relative induction
pCubeMin = NULL;
RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
- if ( RetValue == -1 )
+ if ( RetValue == -1 ) // resource limit is reached
{
Pdr_OblDeref( pThis );
return -1;
@@ -511,7 +515,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
for ( i = 1; i <= k; i++ )
Pdr_ManSolverAddClause( p, i, pCubeMin );
// schedule proof obligation
- if ( k < kMax && !p->pPars->fShortest )
+ if ( !p->pPars->fShortest )
{
pThis->iFrame = k+1;
pThis->prio = Prio--;
@@ -574,6 +578,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
p->nFrames = k;
assert( k == Vec_PtrSize(p->vSolvers)-1 );
+ p->iUseFrame = ABC_INFINITY;
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
// skip disproved outputs
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 7239307..8e5f55b 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -83,6 +83,7 @@ struct Pdr_Man_t_
Pdr_Obl_t * pQueue; // proof obligations
int * pOrder; // ordering of the lits
Vec_Int_t * vActVars; // the counter of activation variables
+ int iUseFrame; // the first used frame
// internal use
Vec_Int_t * vPrio; // priority flops
Vec_Int_t * vLits; // array of literals
--
libgit2 0.26.0