summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c35
-rw-r--r--src/proof/pdr/pdr.h3
-rw-r--r--src/proof/pdr/pdrCore.c255
-rw-r--r--src/proof/pdr/pdrInt.h4
-rw-r--r--src/proof/pdr/pdrSat.c6
-rw-r--r--src/proof/pdr/pdrTsim.c4
-rw-r--r--src/proof/pdr/pdrUtil.c79
-rw-r--r--src/sat/bsat/satSolver.c120
-rw-r--r--src/sat/bsat/satSolver.h2
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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 23:42:52 +0000