summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrInt.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-02-10 18:53:39 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-02-10 18:53:39 -0800
commitdd96bb7477fc568ef8fc8d86d330af22c8fa2f26 (patch)
tree33744ec4f77423b3d117fd0788bd9062583f6365 /src/proof/pdr/pdrInt.h
parent5d717256d3b856d8f29c4a5e442af624f0b0bb69 (diff)
downloadabc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.gz
abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.bz2
abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.zip
Adding PDR with abstraction.
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
-rw-r--r--src/proof/pdr/pdrInt.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 2ee4ae09..a6d249e8 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -96,6 +96,8 @@ struct Pdr_Man_t_
Vec_Int_t * vAbsFlops; // flops currently used
Vec_Int_t * vMapFf2Ppi;
Vec_Int_t * vMapPpi2Ff;
+ int nCexes;
+ int nCexesTotal;
// terminary simulation
Txs_Man_t * pTxs;
// internal use
@@ -142,6 +144,7 @@ struct Pdr_Man_t_
abctime tTsim;
abctime tContain;
abctime tCnf;
+ abctime tAbs;
abctime tTotal;
};