diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
commit | e91abd6307e15d9d4a4985146025e12ae6780cff (patch) | |
tree | c4425a5f5686587b6fcf29a582412363537e23a1 /src | |
parent | f14ee271abe8d38a6dad8789d4b4dbc207fe23c4 (diff) | |
download | abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.gz abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.bz2 abc-e91abd6307e15d9d4a4985146025e12ae6780cff.zip |
Improvements to inductive generalization in IC3/PDR by Zyad Hassan.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 35 | ||||
-rw-r--r-- | src/proof/pdr/pdr.h | 3 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 255 | ||||
-rw-r--r-- | src/proof/pdr/pdrInt.h | 4 | ||||
-rw-r--r-- | src/proof/pdr/pdrSat.c | 6 | ||||
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 4 | ||||
-rw-r--r-- | src/proof/pdr/pdrUtil.c | 79 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 120 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
9 files changed, 495 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 806a5de7..7ff404b0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26008,7 +26008,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, "MFCDRTHGaxrmsipdegovwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmsipdegoncvwzh" ) ) != EOF ) { switch ( c ) { @@ -26100,6 +26100,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nTimeOutGap < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRandomSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRandomSeed < 0 ) + goto usage; + break; case 'a': pPars->fSolveAll ^= 1; break; @@ -26133,6 +26144,12 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fUsePropOut ^= 1; break; + case 'n': + pPars->fSkipDown ^= 1; + break; + case 'c': + pPars->fCtgs ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -26174,9 +26191,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdegovwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmsipdegoncvwzh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); - Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/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" ); Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle ); Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); @@ -26186,6 +26203,7 @@ usage: Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); + Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); @@ -26197,10 +26215,19 @@ usage: 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-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" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-h : print the command usage\n\n"); + Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n"); + Abc_Print( -2, "\t The theory and experiments supporting this work can be found in the following paper:\n"); + Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n"); + Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n"); + + + return 1; } diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 529a161f..b73a54df 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -49,6 +49,7 @@ 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 fDumpInv; // dump inductive invariant @@ -57,6 +58,8 @@ struct Pdr_Par_t_ int fShiftStart; // allows clause pushing to start from an intermediate frame int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe int fSkipGeneral; // skips expensive generalization step + int fSkipDown; // skips the application of down + int fCtgs; // handle CTGs in down 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 b81a1a2a..71a61c81 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,7 +58,10 @@ 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->fSkipDown = 1; // apply down in generalization + pPars->fCtgs = 0; // handle CTGs in down pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant pPars->fUseSupp = 1; // using support variables in the invariant @@ -296,6 +300,190 @@ 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, n, 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 ); + if ( RetValue == -1 ) + return -1; + (*ppCube)->Lits[i] = Lit; + if ( RetValue == 0 ) + continue; + + // remove j-th entry + for ( n = j; n < (*ppCube)->nLits-1; n++ ) + pOrder[n] = pOrder[n+1]; + j--; + + // success - update the cube + *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i ); + Pdr_SetDeref( pCubeTmp ); + assert( (*ppCube)->nLits > 0 ); + i--; + + // get the ordering by decreasing priorit + pOrder = Pdr_ManSortByPriority( p, *ppCube ); + } + 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 ); + 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 ) ) + 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) ); + Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); + } + + Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref + p->nCubes++; + // add clause + for ( i = 1; i <= l; i++ ) + Pdr_ManSolverAddClause( p, i, pCubeMin ); + RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 ); + 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 ); + 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 [Returns 1 if the state could be blocked.] Description [] @@ -307,10 +495,12 @@ 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; + Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL; int i, j, n, 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 ); @@ -318,9 +508,11 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP 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 ); @@ -340,13 +532,22 @@ 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 ); + else + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -354,7 +555,39 @@ 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; + } + added = 0; // remove j-th entry for ( n = j; n < pCubeMin->nLits-1; n++ ) @@ -383,7 +616,7 @@ 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; + Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) { @@ -411,8 +644,18 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP } 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; } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 6a08a150..9c1e9840 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -30,6 +30,7 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver.h" #include "pdr.h" +#include "misc/hash/hashInt.h" ABC_NAMESPACE_HEADER_START @@ -196,10 +197,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 ); diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 2e6130aa..eb94a826 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 diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 32d1c857..37f84667 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -476,7 +476,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); assert( Vec_IntSize(vRes) > 0 ); p->tTsim += Abc_Clock() - clk; 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/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 32e97772..8fb83fd2 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; diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 88a05093..3295fc6f 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1085,6 +1085,77 @@ sat_solver* sat_solver_new(void) return s; } +sat_solver* zsat_solver_new_seed(double seed) +{ + sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver)); + +// Vec_SetAlloc_(&s->Mem, 15); + Sat_MemAlloc_(&s->Mem, 15); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit + s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit + s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit + s->nLearntMax = s->nLearntStart; + + // initialize vectors + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); +// veci_new(&s->learned); + veci_new(&s->act_clas); + veci_new(&s->stack); +// veci_new(&s->model); + veci_new(&s->act_vars); + veci_new(&s->unit_lits); + veci_new(&s->temp_clause); + veci_new(&s->conf_final); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->orderpos = 0; + s->reasons = 0; + s->trail = 0; + + // initialize other vars + s->size = 0; + s->cap = 0; + s->qhead = 0; + s->qtail = 0; +#ifdef USE_FLOAT_ACTIVITY + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999); +#else + s->var_inc = (1 << 5); + s->cla_inc = (1 << 11); +#endif + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = seed; + s->progress_estimate = 0; +// s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); +// s->binary->size_learnt = (2 << 1); + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + return s; +} + void sat_solver_setnvars(sat_solver* s,int n) { int var; @@ -1248,6 +1319,55 @@ void sat_solver_restart( sat_solver* s ) s->stats.tot_literals = 0; } +void zsat_solver_restart_seed( sat_solver* s, double seed ) +{ + int i; + Sat_MemRestart( &s->Mem ); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + veci_resize(&s->act_clas, 0); + veci_resize(&s->trail_lim, 0); + veci_resize(&s->order, 0); + for ( i = 0; i < s->size*2; i++ ) + s->wlists[i].size = 0; + + s->nDBreduces = 0; + + // initialize other vars + s->size = 0; +// s->cap = 0; + s->qhead = 0; + s->qtail = 0; +#ifdef USE_FLOAT_ACTIVITY + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999 ); +#else + s->var_inc = (1 << 5); + s->cla_inc = (1 << 11); +#endif + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = seed; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; +} + // returns memory in bytes used by the SAT solver double sat_solver_memory( sat_solver* s ) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 162b91e5..6ed611e1 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -42,6 +42,7 @@ struct sat_solver_t; typedef struct sat_solver_t sat_solver; extern sat_solver* sat_solver_new(void); +extern sat_solver* zsat_solver_new_seed(double seed); extern void sat_solver_delete(sat_solver* s); extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end); @@ -54,6 +55,7 @@ extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern void sat_solver_restart( sat_solver* s ); +extern void zsat_solver_restart_seed( sat_solver* s, double seed ); extern void sat_solver_rollback( sat_solver* s ); extern int sat_solver_nvars(sat_solver* s); |