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/pdr/pdrInt.h | |
| 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/pdr/pdrInt.h')
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 1 |
1 files changed, 1 insertions, 0 deletions
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 |