diff options
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 73 |
1 files changed, 39 insertions, 34 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 110e6b79a..14a82b17b 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -28,14 +28,10 @@ namespace CVC4 { std::string append(const std::string& str, uint64_t num) { std::ostringstream os; - os << str << num; - return os.str(); + os << str << num; + return os.str(); } - -bool ProofManager::isInitialized = false; -ProofManager* ProofManager::proofManager = NULL; - ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), @@ -50,41 +46,43 @@ ProofManager::~ProofManager() { delete d_cnfProof; delete d_theoryProof; delete d_fullProof; - for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_inputClauses.begin(); + it != d_inputClauses.end(); + ++it) { + delete it->second; } - for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_theoryLemmas.begin(); + it != d_theoryLemmas.end(); + ++it) { + delete it->second; } - // FIXME: memory leak because there are deleted theory lemmas that were not used in the - // SatProof + + // FIXME: memory leak because there are deleted theory lemmas that + // were not used in the SatProof } ProofManager* ProofManager::currentPM() { - if (isInitialized) { - return proofManager; - } else { - proofManager = new ProofManager(); - isInitialized = true; - return proofManager; - } + return smt::currentProofManager(); } Proof* ProofManager::getProof(SmtEngine* smt) { - if (currentPM()->d_fullProof != NULL) + if (currentPM()->d_fullProof != NULL) { return currentPM()->d_fullProof; + } Assert (currentPM()->d_format == LFSC); currentPM()->d_fullProof = new LFSCProof(smt, (LFSCSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), - (LFSCTheoryProof*)getTheoryProof()); + (LFSCTheoryProof*)getTheoryProof()); return currentPM()->d_fullProof; } SatProof* ProofManager::getSatProof() { Assert (currentPM()->d_satProof); - return currentPM()->d_satProof; + return currentPM()->d_satProof; } CnfProof* ProofManager::getCnfProof() { @@ -107,7 +105,7 @@ void ProofManager::initSatProof(Minisat::Solver* solver) { void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { Assert (currentPM()->d_cnfProof == NULL); Assert (currentPM()->d_format == LFSC); - currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); + currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); } void ProofManager::initTheoryProof() { @@ -126,8 +124,8 @@ std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", l void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - d_propVars.insert(lit.getSatVariable()); + prop::SatLiteral lit = clause->operator[](i); + d_propVars.insert(lit.getSatVariable()); } if (kind == INPUT) { d_inputClauses.insert(std::make_pair(id, clause)); @@ -138,11 +136,11 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK } void ProofManager::addAssertion(Expr formula) { - d_inputFormulas.insert(formula); + d_inputFormulas.insert(formula); } void ProofManager::setLogic(const std::string& logic_string) { - d_logic = logic_string; + d_logic = logic_string; } @@ -158,17 +156,24 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; - out << "(check \n"; - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { - d_theoryProof->printAssertions(out, paren); + out << "(check\n"; + if (d_theoryProof == NULL) { + d_theoryProof = new LFSCTheoryProof(); + } + for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); + i != d_cnfProof->end_atom_mapping(); + ++i) { + d_theoryProof->addDeclaration(*i); } - out << "(: (holds cln) \n"; + d_theoryProof->printAssertions(out, paren); + out << "(: (holds cln)\n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); - d_satProof->printResolutions(out, paren); + d_satProof->printResolutions(out, paren); paren <<")))\n;;"; - out << paren.str(); + out << paren.str(); + out << "\n"; } -} /* CVC4 namespace */ +} /* CVC4 namespace */ |