summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrInt.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-09-14 21:20:37 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-09-14 21:20:37 -0700
commit117bc0dbcd4265eb04ed0c47979ec5953a983879 (patch)
treeb71bba56a80267c691cfa62a7a59757441b8006e /src/proof/pdr/pdrInt.h
parentf64bb36fd5081853e0c35ce3d525f2e7041c07ea (diff)
downloadabc-117bc0dbcd4265eb04ed0c47979ec5953a983879.tar.gz
abc-117bc0dbcd4265eb04ed0c47979ec5953a983879.tar.bz2
abc-117bc0dbcd4265eb04ed0c47979ec5953a983879.zip
Prepared &gla to try abstracting and proving concurrently.
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
-rw-r--r--src/proof/pdr/pdrInt.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index f24cb81d..36cea069 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -68,6 +68,7 @@ struct Pdr_Man_t_
Pdr_Par_t * pPars; // parameters
Aig_Man_t * pAig; // user's AIG
// static CNF representation
+ Cnf_Man_t * pCnfMan; // CNF manager
Cnf_Dat_t * pCnf1; // CNF for this AIG
Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
// dynamic CNF representation