diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
commit | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (patch) | |
tree | 6a3608afa6276e11e1a72504c439a4991e9dea41 /src/proof/proof_manager.cpp | |
parent | 08c8433e4ab849024930a8c4dbe8756e13d08099 (diff) |
cleaned up proof code
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 56 |
1 files changed, 32 insertions, 24 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 0c3c597da..23ba0e4e7 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -47,7 +47,15 @@ ProofManager::~ProofManager() { delete d_satProof; delete d_cnfProof; delete d_theoryProof; - delete d_fullProof; + delete d_fullProof; + 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; + } + // FIXME: memory leak because there are deleted theory lemmas that were not used in the + // SatProof } ProofManager* ProofManager::currentPM() { @@ -106,12 +114,29 @@ void ProofManager::initTheoryProof() { } -std::string ProofManager::printInputClauseName(ClauseId id) {return append("pb", id); } -std::string ProofManager::printLemmaClauseName(ClauseId id) { return append("lem", id); } -std::string ProofManager::printLearntClauseName(ClauseId id) { return append("cl", id); } -std::string ProofManager::printVarName(prop::SatVariable var) { return append("v", var); } -std::string ProofManager::printAtomName(prop::SatVariable var) { return append("a", var); } -std::string ProofManager::printLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } +std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); } +std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); } +std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); } +std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); } +std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } + +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()); + } + if (kind == INPUT) { + d_inputClauses.insert(std::make_pair(id, clause)); + return; + } + Assert (kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); +} + +void ProofManager::addAssertion(Expr formula) { + d_inputFormulas.insert(formula); +} LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) @@ -119,18 +144,12 @@ LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theo , d_cnfProof(cnf) , d_theoryProof(theory) { - // link the proofs - d_satProof->setCnfProof(d_cnfProof); - d_cnfProof->setTheoryProof(d_theoryProof); - // build the resolution proof out of the traces - // this sets up the other proofs with the necessary information d_satProof->constructProof(); } void LFSCProof::toStream(std::ostream& out) { std::ostringstream paren; out << "(check \n"; - d_theoryProof->printDeclarations(out, paren); d_theoryProof->printAssertions(out, paren); out << "(: (holds cln) \n"; d_cnfProof->printAtomMapping(out, paren); @@ -140,16 +159,5 @@ void LFSCProof::toStream(std::ostream& out) { out << paren.str(); } -// void ProofManager::declareAtom(Expr atom, SatLiteral lit) { -// ::Minisat::Lit mlit = toMinisatLit(lit); -// d_satProof->addLiteral(mlit); -// d_cnfProof->declareAtom(atom, mlit); -// } - -// void ProofManager::addInputClause(SatClause clause) { -// d_satProof->registerClause(clause, true); -// d_cnfProof->registerClause(clause, true); -// } - } /* CVC4 namespace */ |