diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-07-19 14:08:21 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-07-19 14:08:21 -0700 |
| commit | 35273eaebaf9b8594c30898dad055578dfa81538 (patch) | |
| tree | 21fdaed942ea29642fa728297564a423e60ce43c /src/proof/pdr/pdrInt.h | |
| parent | 9e384d5ca9338467c2df8f4a0dda2d7800979a80 (diff) | |
| download | abc-35273eaebaf9b8594c30898dad055578dfa81538.tar.gz abc-35273eaebaf9b8594c30898dad055578dfa81538.tar.bz2 abc-35273eaebaf9b8594c30898dad055578dfa81538.zip | |
Small data-structure improvements in 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 8e5f55bd..9267ef1e 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -26,6 +26,7 @@ //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" +#include "misc/vec/vecWec.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver.h" #include "pdr.h" @@ -73,8 +74,9 @@ struct Pdr_Man_t_ Vec_Int_t * vVar2Reg; // mapping of SAT var into registers // dynamic CNF representation Cnf_Dat_t * pCnf2; // CNF for this AIG - Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var - Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId + Vec_Int_t * pvId2Vars; // for each used ObjId, maps frame into SAT var + Vec_Ptr_t vVar2Ids; // for each used frame, maps SAT var into ObjId + Vec_Wec_t * vVLits; // CNF literals // data representation int iOutCur; // current output Vec_Ptr_t * vCexes; // counter-examples for each output |