summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c37
-rw-r--r--src/proof/pdr/pdrInt.h2
-rw-r--r--src/proof/pdr/pdrSat.c4
5 files changed, 34 insertions, 18 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index af5d0ccf..44e4bc16 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26171,7 +26171,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctvwzh" ) ) != EOF )
{
switch ( c )
{
@@ -26313,6 +26313,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
pPars->fSkipGeneral ^= 1;
break;
+ case 'j':
+ pPars->fSimpleGeneral ^= 1;
+ break;
case 'o':
pPars->fUsePropOut ^= 1;
break;
@@ -26366,7 +26369,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
+ Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26392,6 +26395,7 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Abc_Print( -2, "\t-e : toggle using only support variables in the invariant [default = %s]\n", pPars->fUseSupp? "yes": "no" );
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
+ Abc_Print( -2, "\t-j : toggle using simplified generalization step [default = %s]\n", pPars->fSimpleGeneral? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using property output as inductive hypothesis [default = %s]\n", pPars->fUsePropOut? "yes": "no" );
Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" );
Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" );
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 33397588..534e8e4b 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -60,6 +60,7 @@ struct Pdr_Par_t_
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
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 45dbfc9f..58735f28 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -125,7 +125,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 );
}
*/
@@ -172,7 +172,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 )
@@ -336,7 +336,7 @@ int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
continue;
// try removing this literal
Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0 );
+ RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
return -1;
(*ppCube)->Lits[i] = Lit;
@@ -392,7 +392,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
*added = 1;
}
ctgAttempts++;
- CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0 );
+ CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0, 1 );
if ( CtgRetValue != 1 )
{
Pdr_SetDeref( pCtg );
@@ -403,7 +403,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
pCubeMin = Pdr_SetDup ( pCtg );
for ( l = k; l < kMax; l++ )
- if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0 ) )
+ if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0, 1 ) )
break;
micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
assert ( micResult != -1 );
@@ -430,7 +430,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
// add clause
for ( i = 1; i <= l; i++ )
Pdr_ManSolverAddClause( p, i, pCubeMin );
- RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
+ RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
assert( RetValue >= 0 );
Pdr_SetDeref( pCtg );
if ( RetValue == 1 )
@@ -464,7 +464,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
printf ("Failed initiation\n");
return 0;
}
- RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
+ RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
return -1;
if ( RetValue == 1 )
@@ -530,7 +530,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
*ppCubeMin = NULL;
if ( p->pPars->fFlopOrder )
Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
- RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
+ 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 )
@@ -552,6 +552,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
@@ -571,12 +581,13 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// check init state
if ( Pdr_SetIsInit(pCubeMin, i) )
continue;
+
// try removing this literal
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
if ( p->pPars->fSkipDown )
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
+ 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 );
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
if ( RetValue == -1 )
{
Pdr_SetDeref( pCubeMin );
@@ -641,7 +652,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
continue;
// try removing this literal
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 );
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
{
Pdr_SetDeref( pCubeMin );
@@ -759,7 +770,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 );
@@ -940,7 +951,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = iFrame;
return -1;
}
- RetValue = Pdr_ManCheckCube( p, iFrame, 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 )
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index a6d249e8..e5b04339 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -199,7 +199,7 @@ 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 ==========================================================*/
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index b9403e6f..ab582d9e 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -287,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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-10 00:55:28 +0000