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/sat_proof.cpp | |
parent | 08c8433e4ab849024930a8c4dbe8756e13d08099 (diff) |
cleaned up proof code
Diffstat (limited to 'src/proof/sat_proof.cpp')
-rw-r--r-- | src/proof/sat_proof.cpp | 34 |
1 files changed, 11 insertions, 23 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index e1534a635..2ac468b47 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -16,7 +16,6 @@ **/ #include "proof/sat_proof.h" -#include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -182,22 +181,11 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_storedUnitConflict(false), d_seenLearnt(), d_seenInput(), - d_seenLemmas(), - d_cnfProof(NULL) + d_seenLemmas() { d_proxy = new ProofProxy(this); } -CnfProof* SatProof::getCnfProof() { - Assert (d_cnfProof); - return d_cnfProof; -} - -void SatProof::setCnfProof(CnfProof* cnfProof) { - Assert (d_cnfProof == NULL); - d_cnfProof = cnfProof; -} - /** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id @@ -638,32 +626,32 @@ void SatProof::constructProof() { std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << ProofManager::printInputClauseName(id); + os << ProofManager::getInputClauseName(id); return os.str(); } else if (isLemmaClause(id)) { - os << ProofManager::printLemmaClauseName(id); + os << ProofManager::getLemmaClauseName(id); return os.str(); }else { - os << ProofManager::printLearntClauseName(id); + os << ProofManager::getLearntClauseName(id); return os.str(); } } -void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) { +void SatProof::addToProofManager(ClauseId id, ClauseKind kind) { if (isUnit(id)) { Minisat::Lit lit = getUnit(id); prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit); prop::SatClause* clause = new SatClause(); clause->push_back(sat_lit); - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); return; } if (isDeleted(id)) { Assert (kind == THEORY_LEMMA); SatClause* clause = d_deletedTheoryLemmas.find(id)->second; - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); return; } @@ -671,7 +659,7 @@ void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) { const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); MinisatSatSolver::toSatClause(minisat_cl, *clause); - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); } void SatProof::collectClauses(ClauseId id) { @@ -686,12 +674,12 @@ void SatProof::collectClauses(ClauseId id) { } if (isInputClause(id)) { - addClauseToCnfProof(id, INPUT); + addToProofManager(id, INPUT); d_seenInput.insert(id); return; } else if (isLemmaClause(id)) { - addClauseToCnfProof(id, THEORY_LEMMA); + addToProofManager(id, THEORY_LEMMA); d_seenLemmas.insert(id); return; } @@ -732,7 +720,7 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "<<ProofManager::printVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; + out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; } if (id == d_emptyClauseId) { |