From 35273eaebaf9b8594c30898dad055578dfa81538 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Jul 2013 14:08:21 -0700 Subject: Small data-structure improvements in 'pdr'. --- src/proof/pdr/pdrInt.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/proof/pdr/pdrInt.h') 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 -- cgit v1.2.3