diff options
author | Liana Hadarean <lianahady@gmail.com> | 2011-10-28 19:24:38 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2011-10-28 19:24:38 +0000 |
commit | b084a7efa9d65ec2f7475caa8486f8fd4cbafbd5 (patch) | |
tree | e118097c88787b7f2899bb8b2cbf865d058ef6bf /src/proof/proof_manager.cpp | |
parent | 9547a48a7cdab8786c080779930de9c39655c52b (diff) |
merged the proofgen3 branch into trunk:
- can now output LFSC checkable resolution proofs
- added configuration option --enable-proof
- added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp new file mode 100644 index 000000000..d6dd7b73d --- /dev/null +++ b/src/proof/proof_manager.cpp @@ -0,0 +1,70 @@ +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" +#include "proof/cnf_proof.h" +#include "util/Assert.h" + +namespace CVC4 { + +bool ProofManager::isInitialized = false; +ProofManager* ProofManager::proofManager = NULL; + +ProofManager::ProofManager(ProofFormat format = LFSC): + d_satProof(NULL), + d_cnfProof(NULL), + d_format(format) +{} + +ProofManager* ProofManager::currentPM() { + if (isInitialized) { + return proofManager; + } else { + proofManager = new ProofManager(); + isInitialized = true; + return proofManager; + } +} + +SatProof* ProofManager::getSatProof() { + Assert (currentPM()->d_satProof); + return currentPM()->d_satProof; +} + +CnfProof* ProofManager::getCnfProof() { + Assert (currentPM()->d_cnfProof); + return currentPM()->d_cnfProof; +} + +void ProofManager::initSatProof(Minisat::Solver* solver) { + Assert (currentPM()->d_satProof == NULL); + switch(currentPM()->d_format) { + case LFSC : + currentPM()->d_satProof = new LFSCSatProof(solver); + break; + case NATIVE : + currentPM()->d_satProof = new SatProof(solver); + break; + default: + Assert(false); + } + +} + +void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { + Assert (currentPM()->d_cnfProof == NULL); + + switch(currentPM()->d_format) { + case LFSC : + currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME + break; + case NATIVE : + currentPM()->d_cnfProof = new CnfProof(cnfStream); + break; + default: + Assert(false); + } + +} + + + +} /* CVC4 namespace */ |