diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 13:31:29 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 13:31:29 -0800 |
| commit | fce2b16a602dcdd3bef8529e51f9a06c2aaf1fec (patch) | |
| tree | ae372f6d7b959646f9b1a1dafab20c8680e2c53a /src/proof | |
| parent | f2d096c9f04acf95e959842d63b6febf2f8eb786 (diff) | |
| download | abc-fce2b16a602dcdd3bef8529e51f9a06c2aaf1fec.tar.gz abc-fce2b16a602dcdd3bef8529e51f9a06c2aaf1fec.tar.bz2 abc-fce2b16a602dcdd3bef8529e51f9a06c2aaf1fec.zip | |
Re-introducing floating-point activity in the SAT solver.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 3 |
3 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 66990bfb..33397588 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -63,6 +63,7 @@ struct Pdr_Par_t_ int fSkipGeneral; // skips expensive generalization step int fSkipDown; // skips the application of down int fCtgs; // handle CTGs in down + int fUseAbs; // use abstraction int fVerbose; // verbose output` int fVeryVerbose; // very verbose output int fNotVerbose; // not printing line by line progress diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index dae20f0c..fb671700 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -90,6 +90,7 @@ 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 + Vec_Int_t * vAbs; // abstraction (mapping abstracted flop ID into its PPIs number) // terminary simulation Txs_Man_t * pTxs; // internal use diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index f9a14a07..b2df5e01 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -286,6 +286,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result p->pCnfMan = Cnf_ManStart(); + if ( p->vAbs ) + p->vAbs = Vec_IntStart( Aig_ManRegNum(pAig) ); // ternary simulation p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL; // additional AIG data-members @@ -368,6 +370,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_WecFreeP( &p->vVLits ); // CNF manager Cnf_ManStop( p->pCnfMan ); + Vec_IntFreeP( &p->vAbs ); // terminary simulation if ( p->pPars->fNewXSim ) Txs_ManStop( p->pTxs ); |