summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/module.make4
-rw-r--r--src/proof/pdr/pdr.h9
-rw-r--r--src/proof/pdr/pdrCore.c502
-rw-r--r--src/proof/pdr/pdrIncr.c760
-rw-r--r--src/proof/pdr/pdrInt.h32
-rw-r--r--src/proof/pdr/pdrInv.c376
-rw-r--r--src/proof/pdr/pdrMan.c341
-rw-r--r--src/proof/pdr/pdrSat.c39
-rw-r--r--src/proof/pdr/pdrTsim.c134
-rw-r--r--src/proof/pdr/pdrTsim2.c550
-rw-r--r--src/proof/pdr/pdrUtil.c137
11 files changed, 2637 insertions, 247 deletions
diff --git a/src/proof/pdr/module.make b/src/proof/pdr/module.make
index 5bee83f8..1dee93aa 100644
--- a/src/proof/pdr/module.make
+++ b/src/proof/pdr/module.make
@@ -1,7 +1,9 @@
SRC += src/proof/pdr/pdrCnf.c \
src/proof/pdr/pdrCore.c \
+ src/proof/pdr/pdrIncr.c \
src/proof/pdr/pdrInv.c \
src/proof/pdr/pdrMan.c \
src/proof/pdr/pdrSat.c \
src/proof/pdr/pdrTsim.c \
- src/proof/pdr/pdrUtil.c
+ src/proof/pdr/pdrTsim2.c \
+ src/proof/pdr/pdrUtil.c
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 529a161f..51b04606 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -49,14 +49,23 @@ struct Pdr_Par_t_
int nTimeOut; // timeout in seconds
int nTimeOutGap; // approximate timeout in seconds since the last change
int nTimeOutOne; // approximate timeout in seconds per one output
+ int nRandomSeed; // value to seed the SAT solver with
int fTwoRounds; // use two rounds for generalization
int fMonoCnf; // monolythic CNF
+ int fNewXSim; // updated X-valued simulation
+ int fFlopPrio; // use structural flop priorities
+ int fFlopOrder; // order flops for 'analyze_final' during generalization
int fDumpInv; // dump inductive invariant
int fUseSupp; // use support in the invariant
int fShortest; // forces bug traces to be shortest
int fShiftStart; // allows clause pushing to start from an intermediate frame
int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
+ int fSimpleGeneral; // simplified generalization
int fSkipGeneral; // skips expensive generalization step
+ int fSkipDown; // skips the application of down
+ int fCtgs; // handle CTGs in down
+ int fUseAbs; // use abstraction
+ int fUseSimpleRef; // simplified CEX refinement
int fVerbose; // verbose output`
int fVeryVerbose; // very verbose output
int fNotVerbose; // not printing line by line progress
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index c020c56a..501f9be6 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -20,6 +20,7 @@
#include "pdrInt.h"
#include "base/main/main.h"
+#include "misc/hash/hash.h"
ABC_NAMESPACE_IMPL_START
@@ -57,12 +58,20 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
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
@@ -118,7 +127,7 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
// make sure the cube works
{
int RetValue;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
assert( RetValue );
}
*/
@@ -165,7 +174,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
}
// check if the clause can be moved to the next frame
- RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0 );
+ RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
if ( RetValue2 == -1 )
return -1;
if ( !RetValue2 )
@@ -296,6 +305,213 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
/**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 cost.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
+{
+ 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(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) )
+ best_i = j;
+ ABC_SWAP( int, pArray[i], pArray[best_i] );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if the state could be blocked.]
Description []
@@ -307,20 +523,28 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
***********************************************************************/
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;
- int i, j, n, Lit, RetValue;
+ 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;
- RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
+ if ( p->pPars->fFlopOrder )
+ Vec_IntSelectSortCostReverseLit( 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;
+ p->tGeneral += clock() - clk;
return 0;
}
+
+ keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
// reduce clause using assumptions
// pCubeMin = Pdr_SetDup( pCube );
@@ -331,6 +555,16 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// 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
@@ -340,13 +574,23 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// i = j;
i = pOrder[j];
- // check init state
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;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
+ 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 );
@@ -354,21 +598,58 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
}
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;
-
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
+ }
+ added = 0;
// success - update the cube
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
Pdr_SetDeref( pCubeTmp );
assert( pCubeMin->nLits > 0 );
- i--;
- // get the ordering by decreasing priorit
+ // 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 )
@@ -383,8 +664,8 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
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 );
+ 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 );
@@ -394,25 +675,30 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
if ( RetValue == 0 )
continue;
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
-
// success - update the cube
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
Pdr_SetDeref( pCubeTmp );
assert( pCubeMin->nLits > 0 );
- i--;
- // get the ordering by decreasing priorit
+ // 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;
}
@@ -444,7 +730,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
{
Counter++;
pThis = Pdr_QueueHead( p );
- if ( pThis->iFrame == 0 )
+ if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
return 0; // SAT
if ( pThis->iFrame > kMax ) // finished this level
return 1;
@@ -497,7 +783,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
assert( pPred == NULL );
for ( k = pThis->iFrame; k < kMax; k++ )
{
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
if ( RetValue == -1 )
{
Pdr_OblDeref( pThis );
@@ -518,7 +804,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
{
assert( pCubeMin->Lits[i] >= 0 );
assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
- Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
+ 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++;
@@ -577,29 +865,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_Set_t * pCube = NULL;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew;
- int k, RetValue = -1;
+ 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, k )
+ Saig_ManForEachPo( p->pAig, pObj, iFrame )
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
{
- Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
+ Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge )
- Gia_ManToBridgeResult( stdout, 1, NULL, k );
+ Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
}
// create the first timeframe
p->pPars->timeLastSolved = Abc_Clock();
- Pdr_ManCreateSolver( p, (k = 0) );
+ Pdr_ManCreateSolver( p, (iFrame = 0) );
while ( 1 )
{
- p->nFrames = k;
- assert( k == Vec_PtrSize(p->vSolvers)-1 );
- p->iUseFrame = Abc_MaxInt(k, 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
@@ -616,16 +918,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( !p->pPars->fSolveAll )
{
- pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
+ 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), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
+ 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, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+ 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 );
@@ -635,8 +937,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
- Abc_Print( 1, "Quitting due to callback on fail.\n" );
- p->pPars->iFrame = k;
+ 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) )
@@ -658,11 +960,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
- Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
- p->pPars->iFrame = k;
+ 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, k, NULL, &pCube, p->pPars->nConfLimit, 0 );
+ RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == 1 )
break;
if ( RetValue == -1 )
@@ -670,9 +972,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
- Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ 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).\n", p->pPars->nTimeOutGap );
+ 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 );
@@ -680,10 +982,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
break; // keep solving
}
else if ( p->pPars->nConfLimit )
- Abc_Print( 1, "Reached conflict limit (%d).\n", 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.\n" );
- p->pPars->iFrame = k;
+ Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
+ p->pPars->iFrame = iFrame;
return -1;
}
if ( RetValue == 0 )
@@ -694,9 +996,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
- Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ 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).\n", p->pPars->nTimeOutGap );
+ 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 );
@@ -704,25 +1006,36 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
break; // keep solving
}
else if ( p->pPars->nConfLimit )
- Abc_Print( 1, "Reached conflict limit (%d).\n", 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.\n" );
- p->pPars->iFrame = k;
+ 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", k );
+ Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
- if ( p->pPars->fVerbose )
+ if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
- p->pPars->iFrame = k;
+ p->pPars->iFrame = iFrame;
if ( !p->pPars->fSolveAll )
{
- p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
+ 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++;
@@ -737,13 +1050,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
- Abc_Print( 1, "Quitting due to callback on fail.\n" );
- p->pPars->iFrame = k;
+ 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, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+ 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 );
@@ -754,6 +1067,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
}
}
+ if ( fRefined )
+ break;
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
@@ -765,22 +1080,32 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->vOutMap )
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( !p->pPars->fNotVerbose )
- Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
+ 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, 1, Abc_Clock() - clkStart );
+ 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, k );
- Pdr_ManCreateSolver( p, ++k );
+ Pdr_ManSetPropertyOutput( p, iFrame );
+ Pdr_ManCreateSolver( p, ++iFrame );
if ( fPrintClauses )
{
- Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+ Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
// push clauses into this timeframe
@@ -792,11 +1117,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
{
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
- Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else
- Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame );
}
- p->pPars->iFrame = k;
+ p->pPars->iFrame = iFrame;
return -1;
}
if ( RetValue )
@@ -807,17 +1132,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
- p->pPars->iFrame = k;
+ 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 ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
- if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
+ for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
+ if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
{
- Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
+ Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
if ( p->pPars->fUseBridge )
- Gia_ManToBridgeResult( stdout, 1, NULL, k );
+ Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
}
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT
@@ -831,44 +1156,44 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
// check termination
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
{
- p->pPars->iFrame = k;
+ p->pPars->iFrame = iFrame;
return -1;
}
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
{
if ( fPrintClauses )
{
- Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+ 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).\n", p->pPars->nTimeOut );
- p->pPars->iFrame = k;
+ 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", k );
+ 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).\n", p->pPars->nTimeOutGap );
- p->pPars->iFrame = k;
+ 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 && k >= p->pPars->nFrameMax )
+ 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 = k;
+ p->pPars->iFrame = iFrame;
return -1;
}
}
@@ -922,11 +1247,12 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
}
if ( p->pPars->fDumpInv )
{
- Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
- Abc_FrameSetStr( Pdr_ManDumpString(p) );
- Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
- Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
+ char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
+ Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
+ else if ( RetValue == 1 )
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
p->tTotal += Abc_Clock() - clk;
Pdr_ManStop( p );
pPars->iFrame--;
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
new file mode 100644
index 00000000..3fcd3d31
--- /dev/null
+++ b/src/proof/pdr/pdrIncr.c
@@ -0,0 +1,760 @@
+/**CFile****************************************************************
+
+ FileName [pdrIncr.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Property driven reachability.]
+
+ Synopsis [PDR with incremental solving.]
+
+ Author [Yen-Sheng Ho, Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Feb. 17, 2017.]
+
+ Revision [$Id: pdrIncr.c$]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+#include "base/main/main.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+extern int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube );
+extern int Pdr_ManPushClauses( Pdr_Man_t * p );
+extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
+extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
+{
+ Vec_Ptr_t * vArrayK;
+ Pdr_Set_t * pCube;
+ int i, k, Counter = 0;
+ Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
+ {
+ Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
+ {
+ Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
+ Pdr_SetPrint( stdout, pCube, nRegs, NULL );
+ Abc_Print( 1, "\n" );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [ Check if each cube c_k in frame k satisfies the query
+ R_{k-1} && T && !c_k && c_k' (must be UNSAT).
+ Return True if all cubes pass the check. ]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IPdr_ManCheckClauses( Pdr_Man_t * p )
+{
+ Pdr_Set_t * pCubeK;
+ Vec_Ptr_t * vArrayK;
+ int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers);
+ int iStartFrame = 1;
+ int counter = 0;
+
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
+ {
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
+ {
+ ++counter;
+ RetValue = Pdr_ManCheckCube( p, k - 1, pCubeK, NULL, 0, 0, 1 );
+
+ if ( !RetValue ) {
+ printf( "Cube[%d][%d] not inductive!\n", k, j );
+ }
+
+ assert( RetValue == 1 );
+ }
+ }
+
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
+{
+ int i, k;
+ Vec_Vec_t * vClausesSaved;
+ Pdr_Set_t * pCla;
+
+ if ( Vec_VecSize( p->vClauses ) == 1 )
+ return NULL;
+ if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast )
+ return NULL;
+
+ if ( fDropLast )
+ vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
+ else
+ vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) );
+
+ Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) )
+ Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla));
+
+ return vClausesSaved;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal )
+{
+ sat_solver * pSat;
+ Vec_Ptr_t * vArrayK;
+ Pdr_Set_t * pCube;
+ int i, j;
+
+ assert( Vec_PtrSize(p->vSolvers) == k );
+ assert( Vec_IntSize(p->vActVars) == k );
+
+ pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
+ pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
+ Vec_PtrPush( p->vSolvers, pSat );
+ Vec_IntPush( p->vActVars, 0 );
+
+ // set the property output
+ if ( k < nTotal - 1 )
+ Pdr_ManSetPropertyOutput( p, k );
+
+ if (k == 0)
+ return pSat;
+
+ // add the clauses
+ Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
+ Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
+ Pdr_ManSolverAddClause( p, k, pCube );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap )
+{
+ int i;
+
+ assert(vClauses);
+
+ Vec_VecFree(p->vClauses);
+ p->vClauses = vClauses;
+
+ // remap clause literals using mapping (old flop -> new flop) found in array vMap
+ if ( vMap )
+ {
+ Pdr_Set_t * pSet; int j, k;
+ Vec_VecForEachEntry( Pdr_Set_t *, vClauses, pSet, i, j )
+ for ( k = 0; k < pSet->nLits; k++ )
+ pSet->Lits[k] = Abc_Lit2LitV( Vec_IntArray(vMap), pSet->Lits[k] );
+ }
+
+ for ( i = 0; i < Vec_VecSize(p->vClauses); ++i )
+ IPdr_ManSetSolver( p, i, Vec_VecSize( p->vClauses ) );
+
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
+{
+ 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();
+
+ if ( Vec_VecSize(p->vClauses) == 0 )
+ Pdr_ManCreateSolver( p, (iFrame = 0) );
+ else {
+ iFrame = Vec_VecSize(p->vClauses) - 1;
+
+ if ( fCheckClauses )
+ {
+ if ( p->pPars->fVerbose )
+ Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
+ IPdr_ManCheckClauses( p );
+ if ( p->pPars->fVerbose )
+ Abc_Print( 1, " Passed!\n" ) ;
+ }
+
+ if ( fPushClauses )
+ {
+ p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+ if ( p->pPars->fVerbose )
+ {
+ Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+ }
+
+ RetValue = Pdr_ManPushClauses( p );
+
+ if ( p->pPars->fVerbose )
+ {
+ Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+ }
+
+ if ( RetValue )
+ {
+ Pdr_ManReportInvariant( p );
+ Pdr_ManVerifyInvariant( p );
+ return 1;
+ }
+ }
+ }
+ 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 )
+ 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 )
+ 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.\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 IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
+{
+ Pdr_Man_t * p;
+ int k, RetValue;
+ Vec_Vec_t * vClausesSaved;
+
+ 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 );
+ while ( 1 ) {
+ RetValue = IPdr_ManSolveInt( p, 1, 0 );
+
+ if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
+ vClausesSaved = IPdr_ManSaveClauses( p, 1 );
+
+ Pdr_ManStop( p );
+
+ p = Pdr_ManStart( pAig, pPars, NULL );
+ IPdr_ManRestore( p, vClausesSaved, NULL );
+
+ pPars->nFrameMax = pPars->nFrameMax << 1;
+
+ continue;
+ }
+
+ 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 = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
+ Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
+ }
+ else if ( RetValue == 1 )
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
+
+ p->tTotal += Abc_Clock() - clk;
+ Pdr_ManStop( p );
+
+ break;
+ }
+
+
+ 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;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarIPdr ( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
+{
+ int RetValue = -1;
+ abctime clk = Abc_Clock();
+ Aig_Man_t * pMan;
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+
+ RetValue = IPdr_ManSolve( pMan, pPars );
+
+ if ( RetValue == 1 )
+ Abc_Print( 1, "Property proved. " );
+ else
+ {
+ if ( RetValue == 0 )
+ {
+ if ( pMan->pSeqModel == NULL )
+ Abc_Print( 1, "Counter-example is not available.\n" );
+ else
+ {
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+ if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
+ Abc_Print( 1, "Counter-example verification has FAILED.\n" );
+ }
+ }
+ else if ( RetValue == -1 )
+ Abc_Print( 1, "Property UNDECIDED. " );
+ else
+ assert( 0 );
+ }
+ ABC_PRT( "Time", Abc_Clock() - clk );
+
+
+ ABC_FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel;
+ pMan->pSeqModel = NULL;
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
+ pNtk->vSeqModelVec = pMan->vSeqModelVec;
+ pMan->vSeqModelVec = NULL;
+ Aig_ManStop( pMan );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 6a08a150..e5b04339 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -30,6 +30,8 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "pdr.h"
+#include "misc/hash/hashInt.h"
+#include "aig/gia/giaAig.h"
ABC_NAMESPACE_HEADER_START
@@ -41,6 +43,8 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
+typedef struct Txs_Man_t_ Txs_Man_t;
+
typedef struct Pdr_Set_t_ Pdr_Set_t;
struct Pdr_Set_t_
{
@@ -68,6 +72,7 @@ struct Pdr_Man_t_
// input problem
Pdr_Par_t * pPars; // parameters
Aig_Man_t * pAig; // user's AIG
+ Gia_Man_t * pGia; // user's AIG
// static CNF representation
Cnf_Man_t * pCnfMan; // CNF manager
Cnf_Dat_t * pCnf1; // CNF for this AIG
@@ -79,6 +84,7 @@ struct Pdr_Man_t_
Vec_Wec_t * vVLits; // CNF literals
// data representation
int iOutCur; // current output
+ int nPrioShift;// priority shift
Vec_Ptr_t * vCexes; // counter-examples for each output
Vec_Ptr_t * vSolvers; // SAT solvers
Vec_Vec_t * vClauses; // clauses by timeframe
@@ -86,6 +92,14 @@ struct Pdr_Man_t_
int * pOrder; // ordering of the lits
Vec_Int_t * vActVars; // the counter of activation variables
int iUseFrame; // the first used frame
+ int nAbsFlops; // the number of flops used
+ Vec_Int_t * vAbsFlops; // flops currently used
+ Vec_Int_t * vMapFf2Ppi;
+ Vec_Int_t * vMapPpi2Ff;
+ int nCexes;
+ int nCexesTotal;
+ // terminary simulation
+ Txs_Man_t * pTxs;
// internal use
Vec_Int_t * vPrio; // priority flops
Vec_Int_t * vLits; // array of literals
@@ -98,8 +112,6 @@ struct Pdr_Man_t_
Vec_Int_t * vVisits; // intermediate
Vec_Int_t * vCi2Rem; // CIs to be removed
Vec_Int_t * vRes; // final result
- Vec_Int_t * vSuppLits; // support literals
- Pdr_Set_t * pCubeJust; // justification
abctime * pTime4Outs;// timeout per output
Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
// statistics
@@ -118,6 +130,8 @@ struct Pdr_Man_t_
int nQueCur;
int nQueMax;
int nQueLim;
+ int nXsimRuns;
+ int nXsimLits;
// runtime
abctime timeToStop;
abctime timeToStopOne;
@@ -130,6 +144,7 @@ struct Pdr_Man_t_
abctime tTsim;
abctime tContain;
abctime tCnf;
+ abctime tAbs;
abctime tTotal;
};
@@ -154,8 +169,6 @@ static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== pdrCex.c ==========================================================*/
-extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
/*=== pdrCnf.c ==========================================================*/
extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
@@ -176,6 +189,7 @@ extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce
extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
extern void Pdr_ManStop( Pdr_Man_t * p );
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
+extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p );
/*=== pdrSat.c ==========================================================*/
extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
@@ -185,9 +199,13 @@ extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, in
extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf );
+extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit );
/*=== pdrTsim.c ==========================================================*/
extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
+/*=== pdrTsim2.c ==========================================================*/
+extern Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio );
+extern void Txs_ManStop( Txs_Man_t * );
+extern Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrUtil.c ==========================================================*/
extern Pdr_Set_t * Pdr_SetAlloc( int nSize );
extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
@@ -196,10 +214,13 @@ extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int n
extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
extern void Pdr_SetDeref( Pdr_Set_t * p );
+extern Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep );
extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
+extern int ZPdr_SetIsInit( Pdr_Set_t * p );
extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
+extern void ZPdr_SetPrint( Pdr_Set_t * p );
extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
@@ -212,7 +233,6 @@ extern void Pdr_QueueClean( Pdr_Man_t * p );
extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
extern void Pdr_QueuePrint( Pdr_Man_t * p );
extern void Pdr_QueueStop( Pdr_Man_t * p );
-extern int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 02b90a36..baade033 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
+ {
+ printf( "Frame " );
+ printf( "Clauses " );
+ printf( "Max Queue " );
+ printf( "Flops " );
+ printf( "Cex " );
+ printf( "Time" );
+ printf( "\n" );
return;
+ }
if ( Abc_FrameIsBatchMode() && !fClose )
return;
// count the total length of the printout
@@ -80,7 +89,10 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
}
for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " );
- Abc_Print( 1, "%6d", p->nQueMax );
+ Abc_Print( 1, "%5d", p->nQueMax );
+ Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
+ if ( p->pPars->fUseAbs )
+ Abc_Print( 1, "%4d", p->nCexes );
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
@@ -88,7 +100,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts );
Abc_Print( 1, "%s", fClose ? "\n":"\r" );
if ( fClose )
- p->nQueMax = 0;
+ p->nQueMax = 0, p->nCexes = 0;
fflush( stdout );
}
@@ -467,8 +479,10 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p )
Vec_Ptr_t * vCubes;
int kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart );
- Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
- kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
+ Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n",
+ kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns );
+// Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
+// kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
Vec_PtrFree( vCubes );
}
@@ -605,9 +619,363 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
//Vec_PtrFree( vCubes );
Vec_PtrFreeP( &p->vInfCubes );
p->vInfCubes = vCubes;
+ Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
return vResult;
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Remove clauses while maintaining the invariant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+#define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
+
+Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
+{
+ int i, k = 0, Count;
+ Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
+ Vec_IntForEachEntry( vCounts, Count, i )
+ if ( Count )
+ Vec_IntWriteEntry( vMap, i, k++ );
+ return vMap;
+}
+Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
+{
+ int i, k, * pCube, * pList = Vec_IntArray(vInv);
+ Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
+ Pdr_ForEachCube( pList, pCube, i )
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
+ return vCounts;
+}
+int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
+{
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ int nZeros = Vec_IntCountZero( vCounts );
+ Vec_IntFree( vCounts );
+ return Vec_IntEntryLast(vInv) - nZeros;
+}
+
+Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
+{
+ Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
+ Vec_Int_t * vMap = Pdr_InvMap( vCounts );
+ int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
+ int i, k, * pCube, * pList = Vec_IntArray(vInv);
+ char * pBuffer = ABC_ALLOC( char, nVars );
+ for ( i = 0; i < nVars; i++ )
+ pBuffer[i] = '-';
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ for ( k = 0; k < pCube[0]; k++ )
+ pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
+ for ( k = 0; k < nVars; k++ )
+ Vec_StrPush( vStr, pBuffer[k] );
+ Vec_StrPush( vStr, ' ' );
+ Vec_StrPush( vStr, '1' );
+ Vec_StrPush( vStr, '\n' );
+ for ( k = 0; k < pCube[0]; k++ )
+ pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
+ }
+ Vec_StrPush( vStr, '\0' );
+ ABC_FREE( pBuffer );
+ Vec_IntFree( vMap );
+ return vStr;
+}
+void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose )
+{
+ printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
+ if ( fVerbose )
+ {
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
+ printf( "%s", Vec_StrArray( vStr ) );
+ Vec_IntFree( vCounts );
+ Vec_StrFree( vStr );
+ }
+}
+
+int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver * pSat, int fSkip )
+{
+ int nBTLimit = 0;
+ int fCheckProperty = 1;
+ int i, k, status, nFailed = 0, nFailedOuts = 0;
+ // collect cubes
+ int * pCube, * pList = Vec_IntArray(vInv);
+ // create variables
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ int iFoVarBeg = sat_solver_nvars(pSat) - Gia_ManRegNum(p);
+ int iFiVarBeg = 1 + Gia_ManPoNum(p);
+ // add cubes
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect literals
+ Vec_IntClear( vLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ if ( pCube[k+1] != -1 )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+ if ( Vec_IntSize(vLits) == 0 )
+ {
+ Vec_IntFree( vLits );
+ return 1;
+ }
+ // add it to the solver
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ assert( status == 1 );
+ }
+ // verify property output
+ if ( fCheckProperty )
+ {
+ for ( i = 0; i < Gia_ManPoNum(p); i++ )
+ {
+ Vec_IntFill( vLits, 1, Abc_Var2Lit(1+i, 0) );
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef ) // timeout
+ break;
+ if ( status == l_True ) // sat - property fails
+ {
+ if ( fVerbose )
+ printf( "Coverage check failed for output %d.\n", i );
+ nFailedOuts++;
+ if ( fSkip )
+ {
+ Vec_IntFree( vLits );
+ return 1;
+ }
+ continue;
+ }
+ assert( status == l_False ); // unsat - property holds
+ }
+ }
+ // iterate through cubes in the direct order
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect cube
+ Vec_IntClear( vLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ if ( pCube[k+1] != -1 )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+ // check if this cube intersects with the complement of other cubes in the solver
+ // if it does not intersect, then it is redundant and can be skipped
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status != l_True && fVerbose )
+ printf( "Finished checking clause %d (out of %d)...\r", i, pList[0] );
+ if ( status == l_Undef ) // timeout
+ break;
+ if ( status == l_False ) // unsat -- correct
+ continue;
+ assert( status == l_True );
+ if ( fVerbose )
+ printf( "Inductiveness check failed for clause %d.\n", i );
+ nFailed++;
+ if ( fSkip )
+ {
+ Vec_IntFree( vLits );
+ return 1;
+ }
+ }
+ Vec_IntFree( vLits );
+ return nFailed + nFailedOuts;
+}
+
+int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
+{
+ int RetValue;
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ assert( sat_solver_nvars(pSat) == pCnf->nVars );
+ Cnf_DataFree( pCnf );
+ RetValue = Pdr_InvCheck_int( p, vInv, fVerbose, pSat, 0 );
+ sat_solver_delete( pSat );
+ return RetValue;
+}
+
+Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
+{
+ int nBTLimit = 0;
+ int fCheckProperty = 1;
+ abctime clk = Abc_Clock();
+ int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
+ Vec_Int_t * vRes = NULL;
+ // create SAT solver
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
+ // create variables
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
+ int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
+ int iFiVarBeg = 1 + Gia_ManPoNum(p);
+ int iAuxVarBeg = sat_solver_nvars(pSat);
+ // allocate auxiliary variables
+ assert( sat_solver_nvars(pSat) == pCnf->nVars );
+ sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
+ // add clauses
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect literals
+ Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+ // add it to the solver
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ assert( status == 1 );
+ }
+ // iterate through clauses
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ if ( Vec_BitEntry(vRemoved, i) )
+ continue;
+ // collect aux literals for remaining clauses
+ Vec_IntClear( vLits );
+ for ( k = 0; k < nCubes; k++ )
+ if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
+ Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
+ nLits = Vec_IntSize( vLits );
+ // check if the property still holds
+ if ( fCheckProperty )
+ {
+ for ( k = 0; k < Gia_ManPoNum(p); k++ )
+ {
+ Vec_IntShrink( vLits, nLits );
+ Vec_IntPush( vLits, Abc_Var2Lit(1+k, 0) );
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef ) // timeout
+ {
+ fFailed = 1;
+ break;
+ }
+ if ( status == l_True ) // sat - property fails
+ break;
+ assert( status == l_False ); // unsat - property holds
+ }
+ if ( fFailed )
+ break;
+ if ( k < Gia_ManPoNum(p) )
+ continue;
+ }
+ // check other clauses
+ fCannot = 0;
+ Pdr_ForEachCube( pList, pCube, n )
+ {
+ if ( Vec_BitEntry(vRemoved, n) || n == i )
+ continue;
+ // collect cube
+ Vec_IntShrink( vLits, nLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+ // check if this cube intersects with the complement of other cubes in the solver
+ // if it does not intersect, then it is redundant and can be skipped
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef ) // timeout
+ {
+ fFailed = 1;
+ break;
+ }
+ if ( status == l_False ) // unsat -- correct
+ continue;
+ assert( status == l_True );
+ // cannot remove
+ fCannot = 1;
+ break;
+ }
+ if ( fFailed )
+ break;
+ if ( fCannot )
+ continue;
+ if ( fVerbose )
+ printf( "Removing clause %d.\n", i );
+ Vec_BitWriteEntry( vRemoved, i, 1 );
+ nRemoved++;
+ }
+ if ( nRemoved )
+ printf( "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes );
+ else
+ printf( "Invariant minimization did not change the invariant. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ // cleanup cover
+ if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
+ {
+ vRes = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vRes, nCubes-nRemoved );
+ Pdr_ForEachCube( pList, pCube, i )
+ if ( !Vec_BitEntry(vRemoved, i) )
+ for ( k = 0; k <= pCube[0]; k++ )
+ Vec_IntPush( vRes, pCube[k] );
+ Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
+ }
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ Vec_BitFree( vRemoved );
+ Vec_IntFree( vLits );
+ return vRes;
+}
+
+Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
+{
+ Vec_Int_t * vRes = NULL;
+ abctime clk = Abc_Clock();
+ int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
+ sat_solver * pSat;
+// sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ nLits += pCube[0];
+ for ( k = 0; k < pCube[0]; k++ )
+ {
+ int Save = pCube[k+1];
+ pCube[k+1] = -1;
+ //sat_solver_bookmark( pSat );
+ pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( Pdr_InvCheck_int(p, vInv, 0, pSat, 1) )
+ pCube[k+1] = Save;
+ else
+ {
+ if ( fVerbose )
+ printf( "Removing lit %d from clause %d.\n", k, i );
+ nRemoved++;
+ }
+ sat_solver_delete( pSat );
+ //sat_solver_rollback( pSat );
+ //sat_solver_bookmark( pSat );
+ }
+ }
+ Cnf_DataFree( pCnf );
+ //sat_solver_delete( pSat );
+ if ( nRemoved )
+ printf( "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits );
+ else
+ printf( "Invariant minimization did not change the invariant. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( nRemoved > 0 ) // finished without timeout and removed some lits
+ {
+ vRes = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vRes, pList[0] );
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ int nLits = 0;
+ for ( k = 0; k < pCube[0]; k++ )
+ if ( pCube[k+1] != -1 )
+ nLits++;
+ Vec_IntPush( vRes, nLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ if ( pCube[k+1] != -1 )
+ Vec_IntPush( vRes, pCube[k+1] );
+ }
+ Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
+ }
+ return vRes;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index b58c479b..a076223b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
@@ -33,6 +34,208 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
+ Synopsis [Structural analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManDeriveFlopPriorities3( Gia_Man_t * p, int fMuxCtrls )
+{
+ int fDiscount = 0;
+ Vec_Wec_t * vLevels;
+ Vec_Int_t * vRes, * vLevel, * vCosts;
+ Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
+ int i, k, Entry, MaxEntry = 0;
+ Gia_ManCreateRefs(p);
+ // discount references
+ if ( fDiscount )
+ {
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
+ pData0 = Gia_Regular(pData0);
+ pData1 = Gia_Regular(pData1);
+ p->pRefs[Gia_ObjId(p, pCtrl)]--;
+ if ( pData0 == pData1 )
+ p->pRefs[Gia_ObjId(p, pData0)]--;
+ }
+ }
+ // create flop costs
+ vCosts = Vec_IntAlloc( Gia_ManRegNum(p) );
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ Vec_IntPush( vCosts, Gia_ObjRefNum(p, pObj) );
+ MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
+ //printf( "%d(%d) ", i, Gia_ObjRefNum(p, pObj) );
+ }
+ //printf( "\n" );
+ MaxEntry++;
+ // add costs due to MUX inputs
+ if ( fMuxCtrls )
+ {
+ int fVerbose = 0;
+ Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
+ Gia_Obj_t * pCtrl, * pData1, * pData0;
+ int nCtrls = 0, nDatas = 0, nBoth = 0;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
+ pCtrl = Gia_Regular(pCtrl);
+ pData1 = Gia_Regular(pData1);
+ pData0 = Gia_Regular(pData0);
+ Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
+ Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
+ Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
+ }
+ Gia_ManForEachRo( p, pObj, i )
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+ Vec_IntAddToEntry( vCosts, i, MaxEntry );
+ //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ // Vec_IntAddToEntry( vCosts, i, MaxEntry );
+ MaxEntry = 2*MaxEntry + 1;
+ // print out
+ if ( fVerbose )
+ {
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+ nCtrls++;
+ if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ nDatas++;
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ nBoth++;
+ }
+ printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
+ }
+ Vec_BitFree( vCtrls );
+ Vec_BitFree( vDatas );
+ }
+ // create levelized structure
+ vLevels = Vec_WecStart( MaxEntry );
+ Vec_IntForEachEntry( vCosts, Entry, i )
+ Vec_WecPush( vLevels, Entry, i );
+ // collect in this order
+ MaxEntry = 0;
+ vRes = Vec_IntStart( Gia_ManRegNum(p) );
+ Vec_WecForEachLevel( vLevels, vLevel, i )
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ Vec_IntWriteEntry( vRes, Entry, MaxEntry++ );
+ //printf( "%d ", Gia_ObjRefNum(p, Gia_ManCi(p, Gia_ManPiNum(p)+Entry)) );
+ //printf( "\n" );
+ assert( MaxEntry == Gia_ManRegNum(p) );
+ Vec_WecFree( vLevels );
+ Vec_IntFree( vCosts );
+ ABC_FREE( p->pRefs );
+//Vec_IntPrint( vRes );
+ return vRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Structural analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls )
+{
+ int fDiscount = 0;
+ Vec_Int_t * vRes = NULL;
+ Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
+ int MaxEntry = 0;
+ int i, * pPerm;
+ // create flop costs
+ Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) );
+ Gia_ManCreateRefs(p);
+ // discount references
+ if ( fDiscount )
+ {
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
+ pData0 = Gia_Regular(pData0);
+ pData1 = Gia_Regular(pData1);
+ p->pRefs[Gia_ObjId(p, pCtrl)]--;
+ if ( pData0 == pData1 )
+ p->pRefs[Gia_ObjId(p, pData0)]--;
+ }
+ }
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) );
+ MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
+ }
+ MaxEntry++;
+ ABC_FREE( p->pRefs );
+ // add costs due to MUX inputs
+ if ( fMuxCtrls )
+ {
+ int fVerbose = 0;
+ Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
+ Gia_Obj_t * pCtrl, * pData1, * pData0;
+ int nCtrls = 0, nDatas = 0, nBoth = 0;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
+ pCtrl = Gia_Regular(pCtrl);
+ pData1 = Gia_Regular(pData1);
+ pData0 = Gia_Regular(pData0);
+ Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
+ Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
+ Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
+ }
+ Gia_ManForEachRo( p, pObj, i )
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+ Vec_IntAddToEntry( vCosts, i, MaxEntry );
+ //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ // Vec_IntAddToEntry( vCosts, i, MaxEntry );
+ // print out
+ if ( fVerbose )
+ {
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
+ nCtrls++;
+ if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ nDatas++;
+ if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
+ nBoth++;
+ }
+ printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
+ }
+ Vec_BitFree( vCtrls );
+ Vec_BitFree( vDatas );
+ }
+ // create ordering based on costs
+ pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
+ vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) );
+ Vec_IntFree( vCosts );
+ vCosts = Vec_IntInvert( vRes, -1 );
+ Vec_IntFree( vRes );
+//Vec_IntPrint( vCosts );
+ return vCosts;
+}
+
+/**Function*************************************************************
+
Synopsis [Creates manager.]
Description []
@@ -48,6 +251,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
p = ABC_CALLOC( Pdr_Man_t, 1 );
p->pPars = pPars;
p->pAig = pAig;
+ p->pGia = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
p->vSolvers = Vec_PtrAlloc( 0 );
p->vClauses = Vec_VecAlloc( 0 );
p->pQueue = NULL;
@@ -56,7 +260,15 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
if ( !p->pPars->fMonoCnf )
p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
// internal use
- p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops
+ p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig));
+ if ( vPrioInit )
+ p->vPrio = vPrioInit;
+ else if ( pPars->fFlopPrio )
+ p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
+ else if ( p->pPars->fNewXSim )
+ p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
+ else
+ p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
p->vLits = Vec_IntAlloc( 100 ); // array of literals
p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves
p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots
@@ -67,9 +279,9 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
p->vVisits = Vec_IntAlloc( 100 ); // intermediate
p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed
p->vRes = Vec_IntAlloc( 100 ); // final result
- p->vSuppLits= Vec_IntAlloc( 100 ); // support literals
- p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
p->pCnfMan = Cnf_ManStart();
+ // ternary simulation
+ p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL;
// additional AIG data-members
if ( pAig->pFanData == NULL )
Aig_ManFanoutStart( pAig );
@@ -108,11 +320,12 @@ void Pdr_ManStop( Pdr_Man_t * p )
Pdr_Set_t * pCla;
sat_solver * pSat;
int i, k;
+ Gia_ManStopP( &p->pGia );
Aig_ManCleanMarkAB( p->pAig );
if ( p->pPars->fVerbose )
{
- Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
- p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
+ Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Cex =%4d Start =%4d\n",
+ p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
ABC_PRTP( " sat ", p->tSatSat, p->tTotal );
@@ -121,6 +334,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal );
ABC_PRTP( "Containment", p->tContain, p->tTotal );
ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
+ ABC_PRTP( "Refinement ", p->tAbs, p->tTotal );
ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
fflush( stdout );
}
@@ -150,6 +364,12 @@ void Pdr_ManStop( Pdr_Man_t * p )
Vec_WecFreeP( &p->vVLits );
// CNF manager
Cnf_ManStop( p->pCnfMan );
+ Vec_IntFreeP( &p->vAbsFlops );
+ Vec_IntFreeP( &p->vMapFf2Ppi );
+ Vec_IntFreeP( &p->vMapPpi2Ff );
+ // terminary simulation
+ if ( p->pPars->fNewXSim )
+ Txs_ManStop( p->pTxs );
// internal use
Vec_IntFreeP( &p->vPrio ); // priority flops
Vec_IntFree( p->vLits ); // array of literals
@@ -162,9 +382,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
Vec_IntFree( p->vVisits ); // intermediate
Vec_IntFree( p->vCi2Rem ); // CIs to be removed
Vec_IntFree( p->vRes ); // final result
- Vec_IntFree( p->vSuppLits ); // support literals
Vec_PtrFreeP( &p->vInfCubes );
- ABC_FREE( p->pCubeJust );
ABC_FREE( p->pTime4Outs );
if ( p->vCexes )
Vec_PtrFreeFree( p->vCexes );
@@ -197,7 +415,6 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
nFrames++;
// create the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
-// pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
pCex->iPo = p->iOutCur;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
@@ -206,6 +423,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
Lit = pObl->pState->Lits[i];
if ( lit_sign(Lit) )
continue;
+ if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
+ continue;
assert( lit_var(Lit) < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
}
@@ -215,6 +434,112 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
return pCex;
}
+/**Function*************************************************************
+
+ Synopsis [Derives counter-example when abstraction is used.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
+{
+ extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
+
+ Gia_Man_t * pAbs;
+ Abc_Cex_t * pCex, * pCexCare;
+ Pdr_Obl_t * pObl;
+ int i, f, Lit, Flop, nFrames = 0;
+ int nPis = Saig_ManPiNum(p->pAig);
+ int nFfRefined = 0;
+ if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
+ return Pdr_ManDeriveCex(p);
+ // restore previous map
+ Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
+ {
+ assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
+ Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
+ }
+ Vec_IntClear( p->vMapPpi2Ff );
+ // count the number of frames
+ for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
+ {
+ for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
+ {
+ Lit = pObl->pState->Lits[i];
+ if ( lit_var(Lit) < nPis ) // PI literal
+ continue;
+ Flop = lit_var(Lit) - nPis;
+ if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
+ continue;
+ Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
+ Vec_IntPush( p->vMapPpi2Ff, Flop );
+ }
+ nFrames++;
+ }
+ if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
+ return Pdr_ManDeriveCex(p);
+ if ( p->pPars->fUseSimpleRef )
+ {
+ // rely on ternary simulation to perform refinement
+ Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
+ {
+ assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
+ Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
+ nFfRefined++;
+ }
+ }
+ else
+ {
+ // create the counter-example
+ pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
+ pCex->iPo = p->iOutCur;
+ pCex->iFrame = nFrames-1;
+ for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
+ for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
+ {
+ Lit = pObl->pState->Lits[i];
+ if ( lit_sign(Lit) )
+ continue;
+ if ( lit_var(Lit) < nPis ) // PI literal
+ Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+ else
+ {
+ int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
+ assert( iPPI < pCex->nPis );
+ Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
+ }
+ }
+ assert( f == nFrames );
+ // perform CEX minimization
+ pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
+ pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
+ Gia_ManStop( pAbs );
+ assert( pCexCare->nPis == pCex->nPis );
+ Abc_CexFree( pCex );
+ // detect care PPIs
+ for ( f = 0; f < nFrames; f++ )
+ {
+ for ( i = nPis; i < pCexCare->nPis; i++ )
+ if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+ {
+ if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
+ Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
+ }
+ }
+ Abc_CexFree( pCexCare );
+ if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
+ return Pdr_ManDeriveCex(p);
+ }
+ //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
+ p->nCexesTotal++;
+ p->nCexes++;
+ return NULL;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 2e6130aa..ab582d9e 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -51,7 +51,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
assert( Vec_VecSize(p->vClauses) == k );
assert( Vec_IntSize(p->vActVars) == k );
// create new solver
- pSat = sat_solver_new();
+// pSat = sat_solver_new();
+ pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
Vec_PtrPush( p->vSolvers, pSat );
Vec_VecExpand( p->vClauses, k );
@@ -86,7 +87,8 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
p->nStarts++;
// sat_solver_delete( pSat );
// pSat = sat_solver_new();
- sat_solver_restart( pSat );
+// sat_solver_restart( pSat );
+ zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
// create new SAT solver
pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
// write new SAT solver
@@ -285,9 +287,9 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
SeeAlso []
***********************************************************************/
-int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf )
+int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )
{
- int fUseLit = 1;
+ //int fUseLit = 0;
int fLitUsed = 0;
sat_solver * pSat;
Vec_Int_t * vLits;
@@ -340,24 +342,6 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
else
return -1;
}
-/*
- if ( RetValue == l_True )
- {
- int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
- if ( RetValue2 )
- p->nCasesSS++;
- else
- p->nCasesSU++;
- }
- else
- {
- int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
- if ( RetValue2 )
- p->nCasesUS++;
- else
- p->nCasesUU++;
- }
-*/
}
clk = Abc_Clock() - clk;
p->tSat += clk;
@@ -375,7 +359,16 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
p->tSatSat += clk;
p->nCallsS++;
if ( ppPred )
- *ppPred = Pdr_ManTernarySim( p, k, pCube );
+ {
+ abctime clk = Abc_Clock();
+ if ( p->pPars->fNewXSim )
+ *ppPred = Txs_ManTernarySim( p->pTxs, k, pCube );
+ else
+ *ppPred = Pdr_ManTernarySim( p, k, pCube );
+ p->tTsim += Abc_Clock() - clk;
+ p->nXsimLits += (*ppPred)->nLits;
+ p->nXsimRuns++;
+ }
RetValue = 0;
}
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 32d1c857..acbf70f5 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -364,7 +364,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
Vec_Int_t * vRes = p->vRes; // final result (flop literals)
Aig_Obj_t * pObj;
int i, Entry, RetValue;
- abctime clk = Abc_Clock();
+ //abctime clk = Abc_Clock();
// collect CO objects
Vec_IntClear( vCoObjs );
@@ -404,67 +404,65 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
assert( RetValue );
-#if 1
- // try removing high-priority flops
- Vec_IntClear( vCi2Rem );
- Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ // iteratively remove flops
+ if ( p->pPars->fFlopPrio )
{
- if ( !Saig_ObjIsLo( p->pAig, pObj ) )
- continue;
- Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
- if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
- continue;
- Vec_IntClear( vUndo );
- if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
- Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
- else
- Pdr_ManExtendUndo( p->pAig, vUndo );
- }
- // try removing low-priority flops
- Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
- {
- if ( !Saig_ObjIsLo( p->pAig, pObj ) )
- continue;
- Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
- if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
- continue;
- Vec_IntClear( vUndo );
- if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
- Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
- else
- Pdr_ManExtendUndo( p->pAig, vUndo );
- }
-#else
- // try removing low-priority flops
- Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
- {
- if ( !Saig_ObjIsLo( p->pAig, pObj ) )
- continue;
- Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
- if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
- continue;
- Vec_IntClear( vUndo );
- if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
- Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
- else
- Pdr_ManExtendUndo( p->pAig, vUndo );
+ // collect flops and sort them by priority
+ Vec_IntClear( vRes );
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+ Vec_IntPush( vRes, Entry );
+ }
+ Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio );
+
+ // try removing flops starting from low-priority to high-priority
+ Vec_IntClear( vCi2Rem );
+ Vec_IntForEachEntry( vRes, Entry, i )
+ {
+ pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry );
+ assert( Saig_ObjIsLo( p->pAig, pObj ) );
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
}
- // try removing high-priority flops
- Vec_IntClear( vCi2Rem );
- Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ else
{
- if ( !Saig_ObjIsLo( p->pAig, pObj ) )
- continue;
- Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
- if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
- continue;
- Vec_IntClear( vUndo );
- if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
- Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
- else
- Pdr_ManExtendUndo( p->pAig, vUndo );
+ // try removing low-priority flops first
+ Vec_IntClear( vCi2Rem );
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+ if ( Vec_IntEntry(vPrio, Entry) )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
+ // try removing high-priority flops next
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+ {
+ if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+ continue;
+ Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+ if ( !Vec_IntEntry(vPrio, Entry) )
+ continue;
+ Vec_IntClear( vUndo );
+ if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
+ Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
+ else
+ Pdr_ManExtendUndo( p->pAig, vUndo );
+ }
}
-#endif
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
@@ -474,9 +472,25 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
// derive the set of resulting registers
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
assert( Vec_IntSize(vRes) > 0 );
- p->tTsim += Abc_Clock() - clk;
+ //p->tTsim += Abc_Clock() - clk;
+
+ // move abstracted literals from flops to inputs
+ if ( p->pPars->fUseAbs && p->vAbsFlops )
+ {
+ int i, iLit, k = 0;
+ Vec_IntForEachEntry( vRes, iLit, i )
+ {
+ if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
+ Vec_IntWriteEntry( vRes, k++, iLit );
+ else
+ Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
+ }
+ Vec_IntShrink( vRes, k );
+ }
pRes = Pdr_SetCreate( vRes, vPiLits );
- assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+ //ZH: Disabled assertion because this invariant doesn't hold with down
+ //because of the join operation which can bring in initial states
+ //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
return pRes;
}
diff --git a/src/proof/pdr/pdrTsim2.c b/src/proof/pdr/pdrTsim2.c
new file mode 100644
index 00000000..8a86eecc
--- /dev/null
+++ b/src/proof/pdr/pdrTsim2.c
@@ -0,0 +1,550 @@
+/**CFile****************************************************************
+
+ FileName [pdrTsim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Property driven reachability.]
+
+ Synopsis [Improved ternary simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 20, 2010.]
+
+ Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct Txs_Man_t_
+{
+ Gia_Man_t * pGia; // user's AIG
+ Vec_Int_t * vPrio; // priority of each flop
+ Vec_Int_t * vCiObjs; // cone leaves (CI obj IDs)
+ Vec_Int_t * vCoObjs; // cone roots (CO obj IDs)
+ Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values)
+ Vec_Int_t * vCoVals; // cone root values (0/1 CO values)
+ Vec_Int_t * vNodes; // cone nodes (node obj IDs)
+ Vec_Int_t * vTemp; // cone nodes (node obj IDs)
+ Vec_Int_t * vPiLits; // resulting array of PI literals
+ Vec_Int_t * vFfLits; // resulting array of flop literals
+ Pdr_Man_t * pMan; // calling manager
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Start and stop the ternary simulation engine.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
+{
+ Txs_Man_t * p;
+// Aig_Obj_t * pObj;
+// int i;
+ assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
+ p = ABC_CALLOC( Txs_Man_t, 1 );
+ p->pGia = Gia_ManFromAigSimple(pAig); // user's AIG
+// Aig_ManForEachObj( pAig, pObj, i )
+// assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
+ p->vPrio = vPrio; // priority of each flop
+ p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves (CI obj IDs)
+ p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots (CO obj IDs)
+ p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values)
+ p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values)
+ p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
+ p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
+ p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals
+ p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals
+ p->pMan = pMan; // calling manager
+ return p;
+}
+void Txs_ManStop( Txs_Man_t * p )
+{
+ Gia_ManStop( p->pGia );
+ Vec_IntFree( p->vCiObjs );
+ Vec_IntFree( p->vCoObjs );
+ Vec_IntFree( p->vCiVals );
+ Vec_IntFree( p->vCoVals );
+ Vec_IntFree( p->vNodes );
+ Vec_IntFree( p->vTemp );
+ Vec_IntFree( p->vPiLits );
+ Vec_IntFree( p->vFfLits );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cone and collects CIs and nodes.]
+
+ Description [For this procedure to work Value should not be ~0
+ at the beginning.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Txs_ManCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+ if ( !~pObj->Value )
+ return;
+ pObj->Value = ~0;
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ Vec_IntPush( vCiObjs, Gia_ObjId(p, pObj) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
+ Txs_ManCollectCone_rec( p, Gia_ObjFanin1(pObj), vCiObjs, vNodes );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+void Txs_ManCollectCone( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
+{
+ Gia_Obj_t * pObj; int i;
+// printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
+ Vec_IntClear( vCiObjs );
+ Vec_IntClear( vNodes );
+ Gia_ManConst0(p)->Value = ~0;
+ Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+ Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate values and assign priority.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Txs_ManForwardPass( Gia_Man_t * p,
+ Vec_Int_t * vPrio, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals,
+ Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
+{
+ Gia_Obj_t * pObj, * pFan0, * pFan1;
+ int i, value0, value1;
+ pObj = Gia_ManConst0(p);
+ pObj->fMark0 = 0;
+ pObj->fMark1 = 0;
+ Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+ {
+ pObj->fMark0 = Vec_IntEntry(vCiVals, i);
+ pObj->fMark1 = 0;
+ pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Vec_IntEntry(vPrio, Gia_ObjCioId(pObj)-Gia_ManPiNum(p));
+ assert( ~pObj->Value );
+ }
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ {
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+ value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+ pObj->fMark0 = value0 && value1;
+ pObj->fMark1 = 0;
+ if ( pObj->fMark0 )
+ pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
+ else if ( value0 )
+ pObj->Value = pFan1->Value;
+ else if ( value1 )
+ pObj->Value = pFan0->Value;
+ else // if ( value0 == 0 && value1 == 0 )
+ pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
+ assert( ~pObj->Value );
+ }
+ Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+ {
+ pFan0 = Gia_ObjFanin0(pObj);
+ pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj));
+ pFan0->fMark1 = 1;
+ assert( (int)pObj->fMark0 == Vec_IntEntry(vCoVals, i) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate requirements and collect results.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Txs_ObjIsJust( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
+ Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
+ int value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+ int value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ if ( pObj->fMark0 )
+ return pFan0->fMark1 && pFan1->fMark1;
+ assert( !pObj->fMark0 );
+ assert( !value0 || !value1 );
+ if ( value0 )
+ return pFan1->fMark1 || Gia_ObjIsPi(p, pFan1);
+ if ( value1 )
+ return pFan0->fMark1 || Gia_ObjIsPi(p, pFan0);
+ assert( !value0 && !value1 );
+ return pFan0->fMark1 || pFan1->fMark1 || Gia_ObjIsPi(p, pFan0) || Gia_ObjIsPi(p, pFan1);
+}
+void Txs_ManBackwardPass( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits )
+{
+ Gia_Obj_t * pObj, * pFan0, * pFan1; int i, value0, value1;
+ Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
+ {
+ if ( !pObj->fMark1 )
+ continue;
+ pObj->fMark1 = 0;
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( pObj->fMark0 )
+ {
+ pFan0->fMark1 = 1;
+ pFan1->fMark1 = 1;
+ continue;
+ }
+ value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+ value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+ assert( !value0 || !value1 );
+ if ( value0 )
+ pFan1->fMark1 = 1;
+ else if ( value1 )
+ pFan0->fMark1 = 1;
+ else // if ( !value0 && !value1 )
+ {
+ if ( pFan0->fMark1 || pFan1->fMark1 )
+ continue;
+ if ( Gia_ObjIsPi(p, pFan0) )
+ pFan0->fMark1 = 1;
+ else if ( Gia_ObjIsPi(p, pFan1) )
+ pFan1->fMark1 = 1;
+ else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
+ pFan0->fMark1 = 1;
+ else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
+ pFan1->fMark1 = 1;
+ else
+ {
+ if ( pFan0->Value >= pFan1->Value )
+ pFan0->fMark1 = 1;
+ else
+ pFan1->fMark1 = 1;
+ }
+ }
+ }
+ Vec_IntClear( vPiLits );
+ Vec_IntClear( vFfLits );
+ Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+ {
+ if ( !pObj->fMark1 )
+ continue;
+ if ( Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) );
+ else
+ Vec_IntPush( vFfLits, Abc_Var2Lit(Gia_ObjCioId(pObj)-Gia_ManPiNum(p), !pObj->fMark0) );
+ }
+ assert( Vec_IntSize(vFfLits) > 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects justification path.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Txs_ManSelectJustPath( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vRes )
+{
+ Gia_Obj_t * pObj, * pFan0, * pFan1;
+ int i, value0, value1;
+ // mark CO drivers
+ Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+ Gia_ObjFanin0(pObj)->fMark1 = 1;
+ // collect just paths
+ Vec_IntClear( vRes );
+ Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
+ {
+ if ( !pObj->fMark1 )
+ continue;
+ pObj->fMark1 = 0;
+ Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( pObj->fMark0 )
+ {
+ pFan0->fMark1 = 1;
+ pFan1->fMark1 = 1;
+ continue;
+ }
+ value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+ value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+ assert( !value0 || !value1 );
+ if ( value0 )
+ pFan1->fMark1 = 1;
+ else if ( value1 )
+ pFan0->fMark1 = 1;
+ else // if ( !value0 && !value1 )
+ {
+ pFan0->fMark1 = 1;
+ pFan1->fMark1 = 1;
+ }
+ }
+ Vec_IntReverseOrder( vRes );
+}
+void Txs_ManCollectJustPis( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vPiLits )
+{
+ Gia_Obj_t * pObj; int i;
+ Vec_IntClear( vPiLits );
+ Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+ if ( pObj->fMark1 && Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) );
+}
+void Txs_ManInitPrio( Gia_Man_t * p, Vec_Int_t * vCiObjs )
+{
+ Gia_Obj_t * pObj; int i;
+ Gia_ManConst0(p)->Value = 0x7FFFFFFF;
+ Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+ pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
+}
+void Txs_ManPropagatePrio( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vPrio )
+{
+ Gia_Obj_t * pObj, * pFan0, * pFan1;
+ int i, value0, value1;
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ {
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( pObj->fMark0 )
+ {
+// pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
+ if ( pFan0->Value == 0x7FFFFFFF )
+ pObj->Value = pFan1->Value;
+ else if ( pFan1->Value == 0x7FFFFFFF )
+ pObj->Value = pFan0->Value;
+ else if ( Vec_IntEntry(vPrio, pFan0->Value) < Vec_IntEntry(vPrio, pFan1->Value) )
+ pObj->Value = pFan0->Value;
+ else
+ pObj->Value = pFan1->Value;
+ continue;
+ }
+ value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
+ value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
+ assert( !value0 || !value1 );
+ if ( value0 )
+ pObj->Value = pFan1->Value;
+ else if ( value1 )
+ pObj->Value = pFan0->Value;
+ else // if ( value0 == 0 && value1 == 0 )
+ {
+// pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
+ if ( pFan0->Value == 0x7FFFFFFF || pFan1->Value == 0x7FFFFFFF )
+ pObj->Value = 0x7FFFFFFF;
+ else if ( Vec_IntEntry(vPrio, pFan0->Value) >= Vec_IntEntry(vPrio, pFan1->Value) )
+ pObj->Value = pFan0->Value;
+ else
+ pObj->Value = pFan1->Value;
+ }
+ assert( ~pObj->Value );
+ }
+}
+int Txs_ManFindMinId( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vPrio )
+{
+ Gia_Obj_t * pObj; int i, iMinId = -1;
+ Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+ if ( Gia_ObjFanin0(pObj)->Value != 0x7FFFFFFF )
+ {
+ if ( iMinId == -1 || Vec_IntEntry(vPrio, iMinId) > Vec_IntEntry(vPrio, Gia_ObjFanin0(pObj)->Value) )
+ iMinId = Gia_ObjFanin0(pObj)->Value;
+ }
+ return iMinId;
+}
+void Txs_ManFindCiReduction( Gia_Man_t * p,
+ Vec_Int_t * vPrio, Vec_Int_t * vCiObjs,
+ Vec_Int_t * vNodes, Vec_Int_t * vCoObjs,
+ Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vTemp )
+{
+ Gia_Obj_t * pObj;
+ int iPrioCi;
+ // propagate PI influence
+ Txs_ManSelectJustPath( p, vNodes, vCoObjs, vTemp );
+ Txs_ManCollectJustPis( p, vCiObjs, vPiLits );
+// printf( "%d -> %d ", Vec_IntSize(vNodes), Vec_IntSize(vTemp) );
+ // iteratively detect and remove smallest IDs
+ Vec_IntClear( vFfLits );
+ Txs_ManInitPrio( p, vCiObjs );
+ while ( 1 )
+ {
+ Txs_ManPropagatePrio( p, vTemp, vPrio );
+ iPrioCi = Txs_ManFindMinId( p, vCoObjs, vPrio );
+ if ( iPrioCi == -1 )
+ break;
+ pObj = Gia_ManCi( p, Gia_ManPiNum(p)+iPrioCi );
+ Vec_IntPush( vFfLits, Abc_Var2Lit(iPrioCi, !pObj->fMark0) );
+ pObj->Value = 0x7FFFFFFF;
+ }
+}
+void Txs_ManPrintFlopLits( Vec_Int_t * vFfLits, Vec_Int_t * vPrio )
+{
+ int i, Entry;
+ printf( "%3d : ", Vec_IntSize(vFfLits) );
+ Vec_IntForEachEntry( vFfLits, Entry, i )
+ printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "+":"-", Abc_Lit2Var(Entry), Vec_IntEntry(vPrio, Abc_Lit2Var(Entry)) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verify the result.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Txs_ManVerify( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
+{
+ Gia_Obj_t * pObj;
+ int i, iLit;
+ Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+ Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
+ Gia_ObjTerSimSetX( pObj );
+ Vec_IntForEachEntry( vPiLits, iLit, i )
+ {
+ pObj = Gia_ManPi( p, Abc_Lit2Var(iLit) );
+ assert( Gia_ObjTerSimGetX(pObj) );
+ if ( Abc_LitIsCompl(iLit) )
+ Gia_ObjTerSimSet0( pObj );
+ else
+ Gia_ObjTerSimSet1( pObj );
+ }
+ Vec_IntForEachEntry( vFfLits, iLit, i )
+ {
+ pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Abc_Lit2Var(iLit) );
+ assert( Gia_ObjTerSimGetX(pObj) );
+ if ( Abc_LitIsCompl(iLit) )
+ Gia_ObjTerSimSet0( pObj );
+ else
+ Gia_ObjTerSimSet1( pObj );
+ }
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ Gia_ObjTerSimAnd( pObj );
+ Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
+ {
+ Gia_ObjTerSimCo( pObj );
+ if ( Vec_IntEntry(vCoVals, i) )
+ assert( Gia_ObjTerSimGet1(pObj) );
+ else
+ assert( Gia_ObjTerSimGet0(pObj) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Shrinks values using ternary simulation.]
+
+ Description [The cube contains the set of flop index literals which,
+ when converted into a clause and applied to the combinational outputs,
+ led to a satisfiable SAT run in frame k (values stored in the SAT solver).
+ If the cube is NULL, it is assumed that the first property output was
+ asserted and failed.
+ The resulting array is a set of flop index literals that asserts the COs.
+ Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube )
+{
+ int fTryNew = 1;
+ Pdr_Set_t * pRes;
+ Gia_Obj_t * pObj;
+ // collect CO objects
+ Vec_IntClear( p->vCoObjs );
+ if ( pCube == NULL ) // the target is the property output
+ {
+ pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
+ Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
+ }
+ else // the target is the cube
+ {
+ int i;
+ for ( i = 0; i < pCube->nLits; i++ )
+ {
+ if ( pCube->Lits[i] == -1 )
+ continue;
+ pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
+ Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
+ }
+ }
+if ( 0 )
+{
+Abc_Print( 1, "Trying to justify cube " );
+if ( pCube )
+ Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
+else
+ Abc_Print( 1, "<prop=fail>" );
+Abc_Print( 1, " in frame %d.\n", k );
+}
+
+ // collect CI objects
+ Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
+ // collect values
+ Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
+ Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
+
+ // perform two passes
+ Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
+ if ( fTryNew )
+ Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp );
+ else
+ Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
+ Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
+
+ // derive the final set
+ pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
+ //ZH: Disabled assertion because this invariant doesn't hold with down
+ //because of the join operation which can bring in initial states
+ //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+ return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 53a8a54a..986697ac 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -260,6 +260,85 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
SeeAlso []
***********************************************************************/
+void ZPdr_SetPrint( Pdr_Set_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nLits; i++)
+ printf ("%d ", p->Lits[i]);
+ printf ("\n");
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Return the intersection of p1 and p2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep )
+{
+ Pdr_Set_t * pIntersection;
+ Vec_Int_t * vCommonLits, * vPiLits;
+ int i, j, nLits;
+ nLits = p1->nLits;
+ if ( p2->nLits < nLits )
+ nLits = p2->nLits;
+ vCommonLits = Vec_IntAlloc( nLits );
+ vPiLits = Vec_IntAlloc( 1 );
+ for ( i = 0, j = 0; i < p1->nLits && j < p2->nLits; )
+ {
+ if ( p1->Lits[i] > p2->Lits[j] )
+ {
+ if ( Hash_IntExists( keep, p2->Lits[j] ) )
+ {
+ //about to drop a literal that should not be dropped
+ Vec_IntFree( vCommonLits );
+ Vec_IntFree( vPiLits );
+ return NULL;
+ }
+ j++;
+ }
+ else if ( p1->Lits[i] < p2->Lits[j] )
+ {
+ if ( Hash_IntExists( keep, p1->Lits[i] ) )
+ {
+ //about to drop a literal that should not be dropped
+ Vec_IntFree( vCommonLits );
+ Vec_IntFree( vPiLits );
+ return NULL;
+ }
+ i++;
+ }
+ else
+ {
+ Vec_IntPush( vCommonLits, p1->Lits[i] );
+ i++;
+ j++;
+ }
+ }
+ pIntersection = Pdr_SetCreate( vCommonLits, vPiLits );
+ Vec_IntFree( vCommonLits );
+ Vec_IntFree( vPiLits );
+ return pIntersection;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
{
char * pBuff;
@@ -284,7 +363,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
}
Vec_StrPushBuffer( vStr, pBuff, k );
Vec_StrPush( vStr, ' ' );
- Vec_StrPush( vStr, '0' );
+ Vec_StrPush( vStr, '1' );
Vec_StrPush( vStr, '\n' );
ABC_FREE( pBuff );
}
@@ -674,8 +753,6 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
pNode->fMarkA = Value;
if ( Aig_ObjIsCi(pNode) )
{
-// if ( vSuppLits )
-// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
if ( Saig_ObjIsLo(pAig, pNode) )
{
// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
@@ -714,60 +791,6 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
}
-/**Function*************************************************************
-
- Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- Aig_Obj_t * pNode;
- int i, v, fCompl;
-// return 0;
- for ( i = 0; i < 4; i++ )
- {
- // derive new assignment
- p->pCubeJust->nLits = 0;
- p->pCubeJust->Sign = 0;
- Aig_ManIncrementTravId( p->pAig );
- for ( v = 0; v < pCube->nLits; v++ )
- {
- if ( pCube->Lits[v] == -1 )
- continue;
- pNode = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) );
- fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode);
- if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) )
- break;
- }
- if ( v < pCube->nLits )
- continue;
- // figure this out!!!
- if ( p->pCubeJust->nLits == 0 )
- continue;
- // successfully derived new assignment
- Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits );
- // check assignment against this cube
- if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) )
- continue;
-//printf( "\n" );
-//Pdr_SetPrint( stdout, pCube, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
-//Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
- // check assignment against the clauses
- if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) )
- continue;
- // find good assignment
- return 1;
- }
- return 0;
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 13:44:57 +0000