mirror of https://github.com/YosysHQ/abc.git
1454 lines
55 KiB
C
1454 lines
55 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [pdrCore.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Property driven reachability.]
|
|
|
|
Synopsis [Core procedures.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - November 20, 2010.]
|
|
|
|
Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "pdrInt.h"
|
|
#include "base/main/main.h"
|
|
#include "misc/hash/hash.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
|
|
extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns 1 if the state could be blocked.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
|
|
{
|
|
memset( pPars, 0, sizeof(Pdr_Par_t) );
|
|
// 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
|
|
pPars->nTimeOutGap = 0; // timeout in seconds since the last solved
|
|
pPars->nConfLimit = 0; // limit on SAT solver conflicts
|
|
pPars->nConfGenLimit = 0; // limit on SAT solver conflicts during generalization
|
|
pPars->nRestLimit = 0; // limit on the number of proof-obligations
|
|
pPars->nRandomSeed = 91648253; // value to seed the SAT solver with
|
|
pPars->fTwoRounds = 0; // use two rounds for generalization
|
|
pPars->fMonoCnf = 0; // monolythic CNF
|
|
pPars->fNewXSim = 0; // updated X-valued simulation
|
|
pPars->fFlopPrio = 0; // use structural flop priorities
|
|
pPars->fFlopOrder = 0; // order flops for 'analyze_final' during generalization
|
|
pPars->fDumpInv = 0; // dump inductive invariant
|
|
pPars->fUseSupp = 1; // using support variables in the invariant
|
|
pPars->fShortest = 0; // forces bug traces to be shortest
|
|
pPars->fUsePropOut = 1; // use property output
|
|
pPars->fSkipDown = 1; // apply down in generalization
|
|
pPars->fCtgs = 0; // handle CTGs in down
|
|
pPars->fUseAbs = 0; // use abstraction
|
|
pPars->fUseSimpleRef = 0; // simplified CEX refinement
|
|
pPars->fVerbose = 0; // verbose output
|
|
pPars->fVeryVerbose = 0; // very verbose output
|
|
pPars->fNotVerbose = 0; // not printing line-by-line progress
|
|
pPars->iFrame = -1; // explored up to this frame
|
|
pPars->nFailOuts = 0; // the number of disproved outputs
|
|
pPars->nDropOuts = 0; // the number of timed out outputs
|
|
pPars->timeLastSolved = 0; // last one solved
|
|
pPars->pInvFileName = NULL; // invariant file name
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Reduces clause using analyzeFinal.]
|
|
|
|
Description [Assumes that the SAT solver just terminated an UNSAT call.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
|
|
{
|
|
Pdr_Set_t * pCubeMin;
|
|
Vec_Int_t * vLits;
|
|
int i, Entry, nCoreLits, * pCoreLits;
|
|
// get relevant SAT literals
|
|
nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
|
|
// translate them into register literals and remove auxiliary
|
|
vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
|
|
// skip if there is no improvement
|
|
if ( Vec_IntSize(vLits) == pCube->nLits )
|
|
return NULL;
|
|
assert( Vec_IntSize(vLits) < pCube->nLits );
|
|
// if the cube overlaps with init, add any literal
|
|
Vec_IntForEachEntry( vLits, Entry, i )
|
|
if ( Abc_LitIsCompl(Entry) == 0 ) // positive literal
|
|
break;
|
|
if ( i == Vec_IntSize(vLits) ) // only negative literals
|
|
{
|
|
// add the first positive literal
|
|
for ( i = 0; i < pCube->nLits; i++ )
|
|
if ( Abc_LitIsCompl(pCube->Lits[i]) == 0 ) // positive literal
|
|
{
|
|
Vec_IntPush( vLits, pCube->Lits[i] );
|
|
break;
|
|
}
|
|
assert( i < pCube->nLits );
|
|
}
|
|
// generate a starting cube
|
|
pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
|
|
assert( !Pdr_SetIsInit(pCubeMin, -1) );
|
|
/*
|
|
// make sure the cube works
|
|
{
|
|
int RetValue;
|
|
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
|
|
assert( RetValue );
|
|
}
|
|
*/
|
|
return pCubeMin;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns 1 if the state could be blocked.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManPushClauses( Pdr_Man_t * p )
|
|
{
|
|
Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
|
|
Vec_Ptr_t * vArrayK, * vArrayK1;
|
|
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
|
|
int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
|
|
int Counter = 0;
|
|
abctime clk = Abc_Clock();
|
|
assert( p->iUseFrame > 0 );
|
|
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
|
|
{
|
|
Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
|
|
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
|
|
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
|
|
{
|
|
Counter++;
|
|
|
|
// remove cubes in the same frame that are contained by pCubeK
|
|
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
|
|
{
|
|
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
|
|
continue;
|
|
Pdr_SetDeref( pTemp );
|
|
Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
|
|
Vec_PtrPop(vArrayK);
|
|
m--;
|
|
}
|
|
|
|
// check if the clause can be moved to the next frame
|
|
RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
|
|
if ( RetValue2 == -1 )
|
|
return -1;
|
|
if ( !RetValue2 )
|
|
continue;
|
|
|
|
{
|
|
Pdr_Set_t * pCubeMin;
|
|
pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
|
|
if ( pCubeMin != NULL )
|
|
{
|
|
// Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
|
|
Pdr_SetDeref( pCubeK );
|
|
pCubeK = pCubeMin;
|
|
}
|
|
}
|
|
|
|
// if it can be moved, add it to the next frame
|
|
Pdr_ManSolverAddClause( p, k+1, pCubeK );
|
|
// check if the clause subsumes others
|
|
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
|
|
{
|
|
if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
|
|
continue;
|
|
Pdr_SetDeref( pCubeK1 );
|
|
Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
|
|
Vec_PtrPop(vArrayK1);
|
|
i--;
|
|
}
|
|
// add the last clause
|
|
Vec_PtrPush( vArrayK1, pCubeK );
|
|
Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
|
|
Vec_PtrPop(vArrayK);
|
|
j--;
|
|
}
|
|
if ( Vec_PtrSize(vArrayK) == 0 )
|
|
RetValue = 1;
|
|
}
|
|
|
|
// clean up the last one
|
|
vArrayK = Vec_VecEntry( p->vClauses, kMax );
|
|
Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
|
|
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
|
|
{
|
|
// remove cubes in the same frame that are contained by pCubeK
|
|
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
|
|
{
|
|
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
|
|
continue;
|
|
/*
|
|
Abc_Print( 1, "===\n" );
|
|
Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
|
|
Abc_Print( 1, "\n" );
|
|
Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
|
|
Abc_Print( 1, "\n" );
|
|
*/
|
|
Pdr_SetDeref( pTemp );
|
|
Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
|
|
Vec_PtrPop(vArrayK);
|
|
m--;
|
|
}
|
|
}
|
|
p->tPush += Abc_Clock() - clk;
|
|
return RetValue;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns 1 if the clause is contained in higher clauses.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
|
|
{
|
|
Pdr_Set_t * pThis;
|
|
Vec_Ptr_t * vArrayK;
|
|
int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
|
|
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
|
|
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
|
|
if ( Pdr_SetContains( pSet, pThis ) )
|
|
return 1;
|
|
return 0;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Sorts literals by priority.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
|
|
{
|
|
int * pPrios = Vec_IntArray(p->vPrio);
|
|
int * pArray = p->pOrder;
|
|
int temp, i, j, best_i, nSize = pCube->nLits;
|
|
// initialize variable order
|
|
for ( i = 0; i < nSize; i++ )
|
|
pArray[i] = i;
|
|
for ( i = 0; i < nSize-1; i++ )
|
|
{
|
|
best_i = i;
|
|
for ( j = i+1; j < nSize; j++ )
|
|
// if ( pArray[j] < pArray[best_i] )
|
|
if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
|
|
best_i = j;
|
|
temp = pArray[i];
|
|
pArray[i] = pArray[best_i];
|
|
pArray[best_i] = temp;
|
|
}
|
|
/*
|
|
for ( i = 0; i < pCube->nLits; i++ )
|
|
Abc_Print( 1, "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
|
|
Abc_Print( 1, "\n" );
|
|
*/
|
|
return pArray;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
|
|
{
|
|
int * pOrder;
|
|
int i, j, Lit, RetValue;
|
|
Pdr_Set_t * pCubeTmp;
|
|
// perform generalization
|
|
if ( p->pPars->fSkipGeneral )
|
|
return 0;
|
|
|
|
// sort literals by their occurences
|
|
pOrder = Pdr_ManSortByPriority( p, *ppCube );
|
|
// try removing literals
|
|
for ( j = 0; j < (*ppCube)->nLits; j++ )
|
|
{
|
|
// use ordering
|
|
// i = j;
|
|
i = pOrder[j];
|
|
|
|
assert( (*ppCube)->Lits[i] != -1 );
|
|
// check init state
|
|
if ( Pdr_SetIsInit(*ppCube, i) )
|
|
continue;
|
|
// try removing this literal
|
|
Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1;
|
|
RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0, 1 );
|
|
if ( RetValue == -1 )
|
|
return -1;
|
|
(*ppCube)->Lits[i] = Lit;
|
|
if ( RetValue == 0 )
|
|
continue;
|
|
|
|
// success - update the cube
|
|
*ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i );
|
|
Pdr_SetDeref( pCubeTmp );
|
|
assert( (*ppCube)->nLits > 0 );
|
|
|
|
// get the ordering by decreasing priority
|
|
pOrder = Pdr_ManSortByPriority( p, *ppCube );
|
|
j--;
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added )
|
|
{
|
|
int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
|
|
int kMax = Vec_PtrSize(p->vSolvers)-1;
|
|
Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
|
|
while ( RetValue == 0 )
|
|
{
|
|
ctgAttempts = 0;
|
|
while ( p->pPars->fCtgs && RetValue == 0 && k > 1 && ctgAttempts < 3 )
|
|
{
|
|
pCtg = Pdr_SetDup( pPred );
|
|
//Check CTG for inductiveness
|
|
if ( Pdr_SetIsInit( pCtg, -1 ) )
|
|
{
|
|
Pdr_SetDeref( pCtg );
|
|
break;
|
|
}
|
|
if (*added == 0)
|
|
{
|
|
for ( i = 1; i <= k; i++ )
|
|
Pdr_ManSolverAddClause( p, i, pIndCube);
|
|
*added = 1;
|
|
}
|
|
ctgAttempts++;
|
|
CtgRetValue = Pdr_ManCheckCube( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0, 1 );
|
|
if ( CtgRetValue != 1 )
|
|
{
|
|
Pdr_SetDeref( pCtg );
|
|
break;
|
|
}
|
|
pCubeMin = Pdr_ManReduceClause( p, k-1, pCtg );
|
|
if ( pCubeMin == NULL )
|
|
pCubeMin = Pdr_SetDup ( pCtg );
|
|
|
|
for ( l = k; l < kMax; l++ )
|
|
if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0, 1 ) )
|
|
break;
|
|
micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
|
|
assert ( micResult != -1 );
|
|
|
|
// add new clause
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
Abc_Print( 1, "Adding cube " );
|
|
Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
|
|
Abc_Print( 1, " to frame %d.\n", l );
|
|
}
|
|
// set priority flops
|
|
for ( i = 0; i < pCubeMin->nLits; i++ )
|
|
{
|
|
assert( pCubeMin->Lits[i] >= 0 );
|
|
assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
|
|
if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
|
|
p->nAbsFlops++;
|
|
Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
|
|
}
|
|
|
|
Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref
|
|
p->nCubes++;
|
|
// add clause
|
|
for ( i = 1; i <= l; i++ )
|
|
Pdr_ManSolverAddClause( p, i, pCubeMin );
|
|
Pdr_SetDeref( pPred );
|
|
RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
|
|
assert( RetValue >= 0 );
|
|
Pdr_SetDeref( pCtg );
|
|
if ( RetValue == 1 )
|
|
{
|
|
//printf ("IT'S A ONE\n");
|
|
return 1;
|
|
}
|
|
}
|
|
|
|
//join
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
printf("Cube:\n");
|
|
ZPdr_SetPrint( *ppCube );
|
|
printf("\nPred:\n");
|
|
ZPdr_SetPrint( pPred );
|
|
}
|
|
*ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
|
|
Pdr_SetDeref( pCubeTmp );
|
|
Pdr_SetDeref( pPred );
|
|
if ( *ppCube == NULL )
|
|
return 0;
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
printf("Intersection:\n");
|
|
ZPdr_SetPrint( *ppCube );
|
|
}
|
|
if ( Pdr_SetIsInit( *ppCube, -1 ) )
|
|
{
|
|
if ( p->pPars->fVeryVerbose )
|
|
printf ("Failed initiation\n");
|
|
return 0;
|
|
}
|
|
RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
|
|
if ( RetValue == -1 )
|
|
return -1;
|
|
if ( RetValue == 1 )
|
|
{
|
|
//printf ("*********IT'S A ONE\n");
|
|
break;
|
|
}
|
|
if ( RetValue == 0 && (*ppCube)->nLits == 1)
|
|
{
|
|
Pdr_SetDeref( pPred ); // fixed memory leak
|
|
// A workaround for the incomplete assignment returned by the SAT
|
|
// solver
|
|
return 0;
|
|
}
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Specialized sorting of flops based on priority.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
|
|
{
|
|
int i, j, best_i;
|
|
for ( i = 0; i < nSize-1; i++ )
|
|
{
|
|
best_i = i;
|
|
for ( j = i+1; j < nSize; j++ )
|
|
if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
|
|
best_i = j;
|
|
ABC_SWAP( int, pArray[i], pArray[best_i] );
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Performs generalization using a different idea.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
|
|
{
|
|
#if 0
|
|
int fUseMinAss = 0;
|
|
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
|
|
int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
|
|
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
|
|
int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
|
|
// create free variables
|
|
int i, iUseVar, iAndVar;
|
|
iAndVar = Pdr_ManFreeVar(p, k);
|
|
for ( i = 1; i < nLits; i++ )
|
|
Pdr_ManFreeVar(p, k);
|
|
iUseVar = Pdr_ManFreeVar(p, k);
|
|
for ( i = 1; i < nLits; i++ )
|
|
Pdr_ManFreeVar(p, k);
|
|
assert( iUseVar == iAndVar + nLits );
|
|
// if there is only one positive literal, put it in front and always assume
|
|
if ( fUseMinAss )
|
|
{
|
|
for ( i = 0; i < pCube->nLits && Count < 2; i++ )
|
|
Count += !Abc_LitIsCompl(pCube->Lits[i]);
|
|
if ( Count == 1 )
|
|
{
|
|
for ( i = 0; i < pCube->nLits; i++ )
|
|
if ( !Abc_LitIsCompl(pCube->Lits[i]) )
|
|
break;
|
|
assert( i < pCube->nLits );
|
|
iLit = pCube->Lits[i];
|
|
for ( ; i > 0; i-- )
|
|
pCube->Lits[i] = pCube->Lits[i-1];
|
|
pCube->Lits[0] = iLit;
|
|
}
|
|
}
|
|
// add clauses for the additional AND-gates
|
|
Vec_IntForEachEntry( vLits1, iLit, i )
|
|
{
|
|
sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
|
|
Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
|
|
}
|
|
// add clauses for the additional OR-gate
|
|
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
|
|
assert( RetValue == 1 );
|
|
// add implications
|
|
vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
|
|
assert( Vec_IntSize(vLits1) == nLits );
|
|
Vec_IntForEachEntry( vLits1, iLit, i )
|
|
{
|
|
Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
|
|
Lits[1] = iLit;
|
|
RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
|
|
assert( RetValue == 1 );
|
|
Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
|
|
}
|
|
sat_solver_compress( pSat );
|
|
// perform minimization
|
|
if ( fUseMinAss )
|
|
{
|
|
if ( Count == 1 ) // always assume the only positive literal
|
|
{
|
|
if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
|
|
nLits = 1;
|
|
else
|
|
nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
|
|
sat_solver_pop(pSat); // unassume the first literal
|
|
}
|
|
else
|
|
nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
|
|
Vec_IntShrink( vLits1, nLits );
|
|
}
|
|
else
|
|
{
|
|
// try removing one literal at a time in the old-fashioned way
|
|
int k, Entry;
|
|
Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
|
|
for ( i = nLits - 1; i >= 0; i-- )
|
|
{
|
|
// if we are about to remove a positive lit, make sure at least one positive lit remains
|
|
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
|
|
{
|
|
Vec_IntForEachEntry( vLits1, iLit, k )
|
|
if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
|
|
break;
|
|
if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
|
|
continue;
|
|
}
|
|
// load remaining literals
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntForEachEntry( vLits1, Entry, k )
|
|
if ( Entry != -1 && k != i )
|
|
Vec_IntPush( vTemp, Entry );
|
|
else if ( Entry != -1 ) // assume opposite literal
|
|
Vec_IntPush( vTemp, Abc_LitNot(Entry) );
|
|
// solve with assumptions
|
|
RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
|
|
// commit the literal
|
|
if ( RetValue == l_False )
|
|
{
|
|
int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
|
|
int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
|
|
assert( RetValue );
|
|
}
|
|
// update the clause
|
|
if ( RetValue == l_False )
|
|
Vec_IntWriteEntry( vLits1, i, -1 );
|
|
}
|
|
Vec_IntFree( vTemp );
|
|
// compact
|
|
k = 0;
|
|
Vec_IntForEachEntry( vLits1, Entry, i )
|
|
if ( Entry != -1 )
|
|
Vec_IntWriteEntry( vLits1, k++, Entry );
|
|
Vec_IntShrink( vLits1, k );
|
|
}
|
|
// remap auxiliary literals into original literals
|
|
Vec_IntForEachEntry( vLits1, iLit, i )
|
|
Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
|
|
// make sure the cube has at least one positive literal
|
|
if ( fUseMinAss )
|
|
{
|
|
Vec_IntForEachEntry( vLits1, iLit, i )
|
|
if ( !Abc_LitIsCompl(iLit) )
|
|
break;
|
|
if ( i == Vec_IntSize(vLits1) ) // has no positive literals
|
|
{
|
|
// find positive lit in the cube
|
|
for ( i = 0; i < pCube->nLits; i++ )
|
|
if ( !Abc_LitIsCompl(pCube->Lits[i]) )
|
|
break;
|
|
assert( i < pCube->nLits );
|
|
Vec_IntPush( vLits1, pCube->Lits[i] );
|
|
// printf( "-" );
|
|
}
|
|
// else
|
|
// printf( "+" );
|
|
}
|
|
// create a subset cube
|
|
*ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
|
|
assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
|
|
Order = 0;
|
|
#endif
|
|
return 0;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns 1 if the state could be blocked.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
|
|
{
|
|
Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL;
|
|
int i, j, Lit, RetValue;
|
|
abctime clk = Abc_Clock();
|
|
int * pOrder;
|
|
int added = 0;
|
|
Hash_Int_t * keep = NULL;
|
|
// if there is no induction, return
|
|
*ppCubeMin = NULL;
|
|
if ( p->pPars->fFlopOrder )
|
|
Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
|
|
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
|
|
if ( p->pPars->fFlopOrder )
|
|
Vec_IntSelectSort( pCube->Lits, pCube->nLits );
|
|
if ( RetValue == -1 )
|
|
return -1;
|
|
if ( RetValue == 0 )
|
|
{
|
|
p->tGeneral += Abc_Clock() - clk;
|
|
return 0;
|
|
}
|
|
|
|
// reduce clause using assumptions
|
|
// pCubeMin = Pdr_SetDup( pCube );
|
|
pCubeMin = Pdr_ManReduceClause( p, k, pCube );
|
|
if ( pCubeMin == NULL )
|
|
pCubeMin = Pdr_SetDup( pCube );
|
|
|
|
// perform simplified generalization
|
|
if ( p->pPars->fSimpleGeneral )
|
|
{
|
|
assert( pCubeMin->nLits > 0 );
|
|
if ( pCubeMin->nLits > 1 )
|
|
{
|
|
RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
|
|
Pdr_SetDeref( pCubeMin );
|
|
assert( ppCubeMin != NULL );
|
|
pCubeMin = *ppCubeMin;
|
|
}
|
|
*ppCubeMin = pCubeMin;
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
printf("Cube:\n");
|
|
for ( i = 0; i < pCubeMin->nLits; i++)
|
|
printf ("%d ", pCubeMin->Lits[i]);
|
|
printf("\n");
|
|
}
|
|
p->tGeneral += Abc_Clock() - clk;
|
|
return 1;
|
|
}
|
|
|
|
keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
|
|
|
|
// perform generalization
|
|
if ( !p->pPars->fSkipGeneral )
|
|
{
|
|
// assume the unminimized cube
|
|
if ( p->pPars->fSimpleGeneral )
|
|
{
|
|
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
|
|
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
|
|
int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
|
|
assert( RetValue1 == 1 );
|
|
sat_solver_compress( pSat );
|
|
}
|
|
|
|
// sort literals by their occurences
|
|
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
|
// try removing literals
|
|
for ( j = 0; j < pCubeMin->nLits; j++ )
|
|
{
|
|
// use ordering
|
|
// i = j;
|
|
i = pOrder[j];
|
|
|
|
assert( pCubeMin->Lits[i] != -1 );
|
|
if ( keep && Hash_IntExists( keep, pCubeMin->Lits[i] ) )
|
|
{
|
|
//printf("Undroppable\n");
|
|
continue;
|
|
}
|
|
|
|
// check init state
|
|
if ( Pdr_SetIsInit(pCubeMin, i) )
|
|
continue;
|
|
|
|
// try removing this literal
|
|
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
|
|
if ( p->pPars->fSkipDown )
|
|
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
|
|
else
|
|
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
|
|
if ( RetValue == -1 )
|
|
{
|
|
Pdr_SetDeref( pCubeMin );
|
|
return -1;
|
|
}
|
|
pCubeMin->Lits[i] = Lit;
|
|
if ( RetValue == 0 )
|
|
{
|
|
if ( p->pPars->fSkipDown )
|
|
continue;
|
|
pCubeCpy = Pdr_SetCreateFrom( pCubeMin, i );
|
|
RetValue = ZPdr_ManDown( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
|
|
if ( p->pPars->fCtgs )
|
|
//CTG handling code messes up with the internal order array
|
|
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
|
if ( RetValue == -1 )
|
|
{
|
|
Pdr_SetDeref( pCubeMin );
|
|
Pdr_SetDeref( pCubeCpy );
|
|
Pdr_SetDeref( pPred );
|
|
return -1;
|
|
}
|
|
if ( RetValue == 0 )
|
|
{
|
|
if ( keep )
|
|
Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
|
|
if ( pCubeCpy )
|
|
Pdr_SetDeref( pCubeCpy );
|
|
continue;
|
|
}
|
|
//Inductive subclause
|
|
added = 0;
|
|
Pdr_SetDeref( pCubeMin );
|
|
pCubeMin = pCubeCpy;
|
|
assert( pCubeMin->nLits > 0 );
|
|
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
|
j = -1;
|
|
continue;
|
|
}
|
|
added = 0;
|
|
|
|
// success - update the cube
|
|
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
|
|
Pdr_SetDeref( pCubeTmp );
|
|
assert( pCubeMin->nLits > 0 );
|
|
|
|
// assume the minimized cube
|
|
if ( p->pPars->fSimpleGeneral )
|
|
{
|
|
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
|
|
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
|
|
int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
|
|
assert( RetValue1 == 1 );
|
|
sat_solver_compress( pSat );
|
|
}
|
|
|
|
// get the ordering by decreasing priority
|
|
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
|
j--;
|
|
}
|
|
|
|
if ( p->pPars->fTwoRounds )
|
|
for ( j = 0; j < pCubeMin->nLits; j++ )
|
|
{
|
|
// use ordering
|
|
// i = j;
|
|
i = pOrder[j];
|
|
|
|
// check init state
|
|
assert( pCubeMin->Lits[i] != -1 );
|
|
if ( Pdr_SetIsInit(pCubeMin, i) )
|
|
continue;
|
|
// try removing this literal
|
|
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
|
|
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 );
|
|
if ( RetValue == -1 )
|
|
{
|
|
Pdr_SetDeref( pCubeMin );
|
|
return -1;
|
|
}
|
|
pCubeMin->Lits[i] = Lit;
|
|
if ( RetValue == 0 )
|
|
continue;
|
|
|
|
// success - update the cube
|
|
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
|
|
Pdr_SetDeref( pCubeTmp );
|
|
assert( pCubeMin->nLits > 0 );
|
|
|
|
// get the ordering by decreasing priority
|
|
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
|
j--;
|
|
}
|
|
}
|
|
|
|
assert( ppCubeMin != NULL );
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
printf("Cube:\n");
|
|
for ( i = 0; i < pCubeMin->nLits; i++)
|
|
printf ("%d ", pCubeMin->Lits[i]);
|
|
printf("\n");
|
|
}
|
|
*ppCubeMin = pCubeMin;
|
|
p->tGeneral += Abc_Clock() - clk;
|
|
if ( keep ) Hash_IntFree( keep );
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns 1 if the state could be blocked.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
|
|
{
|
|
Pdr_Obl_t * pThis;
|
|
Pdr_Set_t * pPred, * pCubeMin;
|
|
int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
|
|
int kMax = Vec_PtrSize(p->vSolvers)-1;
|
|
abctime clk;
|
|
p->nBlocks++;
|
|
// create first proof obligation
|
|
// assert( p->pQueue == NULL );
|
|
pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
|
|
Pdr_QueuePush( p, pThis );
|
|
// try to solve it recursively
|
|
while ( !Pdr_QueueIsEmpty(p) )
|
|
{
|
|
Counter++;
|
|
pThis = Pdr_QueueHead( p );
|
|
if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
|
|
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;
|
|
Pdr_QueueStop( p );
|
|
return 1; // restart
|
|
}
|
|
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 ) )
|
|
{
|
|
p->tContain += Abc_Clock() - clk;
|
|
Pdr_OblDeref( pThis );
|
|
continue;
|
|
}
|
|
p->tContain += Abc_Clock() - clk;
|
|
|
|
// check if the cube is already contained
|
|
RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
|
|
if ( RetValue == -1 ) // resource limit is reached
|
|
{
|
|
Pdr_OblDeref( pThis );
|
|
return -1;
|
|
}
|
|
if ( RetValue ) // cube is blocked by clauses in this frame
|
|
{
|
|
Pdr_OblDeref( pThis );
|
|
continue;
|
|
}
|
|
|
|
// check if the cube holds with relative induction
|
|
pCubeMin = NULL;
|
|
RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
|
|
if ( RetValue == -1 ) // resource limit is reached
|
|
{
|
|
Pdr_OblDeref( pThis );
|
|
return -1;
|
|
}
|
|
if ( RetValue ) // cube is blocked inductively in this frame
|
|
{
|
|
assert( pCubeMin != NULL );
|
|
// k is the last frame where pCubeMin holds
|
|
k = pThis->iFrame;
|
|
// check other frames
|
|
assert( pPred == NULL );
|
|
for ( k = pThis->iFrame; k < kMax; k++ )
|
|
{
|
|
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
|
|
if ( RetValue == -1 )
|
|
{
|
|
Pdr_OblDeref( pThis );
|
|
return -1;
|
|
}
|
|
if ( !RetValue )
|
|
break;
|
|
}
|
|
// add new clause
|
|
if ( p->pPars->fVeryVerbose )
|
|
{
|
|
Abc_Print( 1, "Adding cube " );
|
|
Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
|
|
Abc_Print( 1, " to frame %d.\n", k );
|
|
}
|
|
// set priority flops
|
|
for ( i = 0; i < pCubeMin->nLits; i++ )
|
|
{
|
|
assert( pCubeMin->Lits[i] >= 0 );
|
|
assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
|
|
if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
|
|
p->nAbsFlops++;
|
|
Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
|
|
}
|
|
Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
|
|
p->nCubes++;
|
|
// add clause
|
|
for ( i = 1; i <= k; i++ )
|
|
Pdr_ManSolverAddClause( p, i, pCubeMin );
|
|
// schedule proof obligation
|
|
if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
|
|
{
|
|
pThis->iFrame = k+1;
|
|
pThis->prio = Prio--;
|
|
Pdr_QueuePush( p, pThis );
|
|
}
|
|
else
|
|
{
|
|
Pdr_OblDeref( pThis );
|
|
}
|
|
}
|
|
else
|
|
{
|
|
assert( pCubeMin == NULL );
|
|
assert( pPred != NULL );
|
|
pThis->prio = Prio--;
|
|
Pdr_QueuePush( p, pThis );
|
|
pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
|
|
Pdr_QueuePush( p, pThis );
|
|
}
|
|
|
|
// check termination
|
|
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
|
|
return -1;
|
|
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
|
|
return -1;
|
|
if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
|
|
return -1;
|
|
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
|
|
return -1;
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManSolveInt( Pdr_Man_t * p )
|
|
{
|
|
int fPrintClauses = 0;
|
|
Pdr_Set_t * pCube = NULL;
|
|
Aig_Obj_t * pObj;
|
|
Abc_Cex_t * pCexNew;
|
|
int iFrame, RetValue = -1;
|
|
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
|
|
abctime clkStart = Abc_Clock(), clkOne = 0;
|
|
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
|
|
assert( Vec_PtrSize(p->vSolvers) == 0 );
|
|
// in the multi-output mode, mark trivial POs (those fed by const0) as solved
|
|
if ( p->pPars->fSolveAll )
|
|
Saig_ManForEachPo( p->pAig, pObj, iFrame )
|
|
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
|
|
{
|
|
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
|
|
p->pPars->nProveOuts++;
|
|
if ( p->pPars->fUseBridge )
|
|
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
|
|
}
|
|
// create the first timeframe
|
|
p->pPars->timeLastSolved = Abc_Clock();
|
|
Pdr_ManCreateSolver( p, (iFrame = 0) );
|
|
while ( 1 )
|
|
{
|
|
int fRefined = 0;
|
|
if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
|
|
{
|
|
// int i, Prio;
|
|
assert( p->vAbsFlops == NULL );
|
|
p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
|
|
p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
|
|
p->vMapPpi2Ff = Vec_IntAlloc( 100 );
|
|
// Vec_IntForEachEntry( p->vPrio, Prio, i )
|
|
// if ( Prio >> p->nPrioShift )
|
|
// Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
|
|
}
|
|
//if ( p->pPars->fUseAbs && p->vAbsFlops )
|
|
// printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
|
|
p->nFrames = iFrame;
|
|
assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
|
|
p->iUseFrame = Abc_MaxInt(iFrame, 1);
|
|
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
|
|
{
|
|
// skip disproved outputs
|
|
if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
|
|
continue;
|
|
// skip output whose time has run out
|
|
if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
|
|
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->fSolveAll )
|
|
{
|
|
pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
|
|
p->pAig->pSeqModel = pCexNew;
|
|
return 0; // SAT
|
|
}
|
|
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
|
|
p->pPars->nFailOuts++;
|
|
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
|
|
if ( !p->pPars->fNotVerbose )
|
|
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
|
|
nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
|
|
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
|
|
if ( p->pPars->fUseBridge )
|
|
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
|
|
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
|
|
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
|
|
return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
|
|
p->pPars->timeLastSolved = Abc_Clock();
|
|
continue;
|
|
}
|
|
// try to solve this output
|
|
if ( p->pTime4Outs )
|
|
{
|
|
assert( p->pTime4Outs[p->iOutCur] > 0 );
|
|
clkOne = Abc_Clock();
|
|
p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
|
|
}
|
|
while ( 1 )
|
|
{
|
|
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
|
|
if ( RetValue == 1 )
|
|
break;
|
|
if ( RetValue == -1 )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
|
|
else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
|
|
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
|
|
else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
|
|
{
|
|
Pdr_QueueClean( p );
|
|
pCube = NULL;
|
|
break; // keep solving
|
|
}
|
|
else if ( p->pPars->nConfLimit )
|
|
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
|
|
else if ( p->pPars->fVerbose )
|
|
Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( RetValue == 0 )
|
|
{
|
|
RetValue = Pdr_ManBlockCube( p, pCube );
|
|
if ( RetValue == -1 )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
|
|
else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
|
|
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
|
|
else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
|
|
{
|
|
Pdr_QueueClean( p );
|
|
pCube = NULL;
|
|
break; // keep solving
|
|
}
|
|
else if ( p->pPars->nConfLimit )
|
|
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
|
|
else if ( p->pPars->fVerbose )
|
|
Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( RetValue == 0 )
|
|
{
|
|
if ( fPrintClauses )
|
|
{
|
|
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
|
|
Pdr_ManPrintClauses( p, 0 );
|
|
}
|
|
if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
|
|
Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
|
|
p->pPars->iFrame = iFrame;
|
|
if ( !p->pPars->fSolveAll )
|
|
{
|
|
abctime clk = Abc_Clock();
|
|
Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
|
|
p->tAbs += Abc_Clock() - clk;
|
|
if ( pCex == NULL )
|
|
{
|
|
assert( p->pPars->fUseAbs );
|
|
Pdr_QueueClean( p );
|
|
pCube = NULL;
|
|
fRefined = 1;
|
|
break; // keep solving
|
|
}
|
|
p->pAig->pSeqModel = pCex;
|
|
return 0; // SAT
|
|
}
|
|
p->pPars->nFailOuts++;
|
|
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
|
|
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
|
|
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
|
|
if ( p->pPars->fUseBridge )
|
|
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
|
|
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
|
|
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( !p->pPars->fNotVerbose )
|
|
Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
|
|
nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
|
|
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
|
|
return 0; // all SAT
|
|
Pdr_QueueClean( p );
|
|
pCube = NULL;
|
|
break; // keep solving
|
|
}
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
|
|
}
|
|
}
|
|
if ( fRefined )
|
|
break;
|
|
if ( p->pTime4Outs )
|
|
{
|
|
abctime timeSince = Abc_Clock() - clkOne;
|
|
assert( p->pTime4Outs[p->iOutCur] > 0 );
|
|
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
|
|
if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
|
|
{
|
|
p->pPars->nDropOuts++;
|
|
if ( p->pPars->vOutMap )
|
|
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
|
|
if ( !p->pPars->fNotVerbose )
|
|
Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
|
|
}
|
|
p->timeToStopOne = 0;
|
|
}
|
|
}
|
|
if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
|
|
{
|
|
int i, Used;
|
|
Vec_IntForEachEntry( p->vAbsFlops, Used, i )
|
|
if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
|
|
Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
|
|
}
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
|
|
if ( fRefined )
|
|
continue;
|
|
//if ( p->pPars->fUseAbs && p->vAbsFlops )
|
|
// printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
|
|
// open a new timeframe
|
|
p->nQueLim = p->pPars->nRestLimit;
|
|
assert( pCube == NULL );
|
|
Pdr_ManSetPropertyOutput( p, iFrame );
|
|
Pdr_ManCreateSolver( p, ++iFrame );
|
|
if ( fPrintClauses )
|
|
{
|
|
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
|
|
Pdr_ManPrintClauses( p, 0 );
|
|
}
|
|
// push clauses into this timeframe
|
|
RetValue = Pdr_ManPushClauses( p );
|
|
if ( RetValue == -1 )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
{
|
|
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
|
|
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
|
|
else
|
|
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
|
|
}
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( RetValue )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Pdr_ManReportInvariant( p );
|
|
if ( !p->pPars->fSilent )
|
|
Pdr_ManVerifyInvariant( p );
|
|
p->pPars->iFrame = iFrame;
|
|
// 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->vOutMap )
|
|
for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
|
|
if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
|
|
{
|
|
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
|
|
if ( p->pPars->fUseBridge )
|
|
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
|
|
}
|
|
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
|
|
return 1; // UNSAT
|
|
if ( p->pPars->nFailOuts > 0 )
|
|
return 0; // SAT
|
|
return -1;
|
|
}
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
|
|
|
|
// check termination
|
|
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
|
|
{
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
|
|
{
|
|
if ( fPrintClauses )
|
|
{
|
|
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
|
|
Pdr_ManPrintClauses( p, 0 );
|
|
}
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
|
|
{
|
|
if ( fPrintClauses )
|
|
{
|
|
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
|
|
Pdr_ManPrintClauses( p, 0 );
|
|
}
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
|
|
{
|
|
if ( p->pPars->fVerbose )
|
|
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
|
|
if ( !p->pPars->fSilent )
|
|
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
|
|
p->pPars->iFrame = iFrame;
|
|
return -1;
|
|
}
|
|
}
|
|
assert( 0 );
|
|
return -1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
|
|
{
|
|
Pdr_Man_t * p;
|
|
int k, RetValue;
|
|
abctime clk = Abc_Clock();
|
|
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
|
|
pPars->nTimeOutOne = 0;
|
|
if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
|
|
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
|
|
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. QueMax = %d. TimeMax = %d. ",
|
|
pPars->nRecycle,
|
|
pPars->nFrameMax,
|
|
pPars->nRestLimit,
|
|
pPars->nTimeOut );
|
|
Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
|
|
pPars->fMonoCnf ? "yes" : "no",
|
|
pPars->fSkipGeneral ? "yes" : "no",
|
|
pPars->fSolveAll ? "yes" : "no" );
|
|
}
|
|
ABC_FREE( pAig->pSeqModel );
|
|
p = Pdr_ManStart( pAig, pPars, NULL );
|
|
RetValue = Pdr_ManSolveInt( 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 )
|
|
{
|
|
char * pFileName = pPars->pInvFileName ? pPars->pInvFileName : Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
|
|
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
|
|
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
|
|
printf( "Dumped inductive invariant in file \"%s\".\n", pFileName );
|
|
}
|
|
else if ( RetValue == 1 )
|
|
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
|
|
p->tTotal += Abc_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
|
|
if ( pPars->fUseBridge )
|
|
Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
|
|
return RetValue;
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|