From 64143d6aa74c9a9140b11fa021c254910bf495a0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 29 Oct 2011 19:09:06 +0000 Subject: [PATCH] fix some doxygen warnings --- src/proof/sat_proof.cpp | 48 ++++++++++++++++++++--------------------- src/proof/sat_proof.h | 2 +- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 37a3a9706..581ee6d96 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -87,9 +87,9 @@ void SatProof::createLitSet(ClauseId id, LitSet& set) { /** * Resolves clause1 and clause2 on variable var and stores the * result in clause1 - * @param var - * @param clause1 - * @param clause2 + * @param v + * @param clause1 + * @param clause2 */ bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) { Assert(!clause1.empty()); @@ -247,7 +247,7 @@ bool SatProof::checkResolution(ClauseId id) { /// helper methods -ClauseId SatProof::getClauseId(CRef ref) { +ClauseId SatProof::getClauseId(::Minisat::CRef ref) { if(d_clauseId.find(ref) == d_clauseId.end()) { Debug("proof:sat") << "Missing clause \n"; } @@ -256,12 +256,12 @@ ClauseId SatProof::getClauseId(CRef ref) { } -ClauseId SatProof::getClauseId(Lit lit) { +ClauseId SatProof::getClauseId(::Minisat::Lit lit) { Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); return d_unitId[toInt(lit)]; } -CRef SatProof::getClauseRef(ClauseId id) { +::Minisat::CRef SatProof::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { Debug("proof:sat") << "proof:getClauseRef cannot find clause "<ca[id]; } -Lit SatProof::getUnit(ClauseId id) { +::Minisat::Lit SatProof::getUnit(ClauseId id) { Assert (d_idUnit.find(id) != d_idUnit.end()); return d_idUnit[id]; } @@ -283,11 +283,11 @@ bool SatProof::isUnit(ClauseId id) { return d_idUnit.find(id) != d_idUnit.end(); } -bool SatProof::isUnit(Lit lit) { +bool SatProof::isUnit(::Minisat::Lit lit) { return d_unitId.find(toInt(lit)) != d_unitId.end(); } -ClauseId SatProof::getUnitId(Lit lit) { +ClauseId SatProof::getUnitId(::Minisat::Lit lit) { Assert(isUnit(lit)); return d_unitId[toInt(lit)]; } @@ -343,7 +343,7 @@ void SatProof::printRes(ResChain* res) { /// registration methods -ClauseId SatProof::registerClause(CRef clause, bool isInput) { +ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) { Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { @@ -358,7 +358,7 @@ ClauseId SatProof::registerClause(CRef clause, bool isInput) { return d_clauseId[clause]; } -ClauseId SatProof::registerUnitClause(Lit lit, bool isInput) { +ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) { UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { ClauseId newId = d_idCounter++; @@ -372,7 +372,7 @@ ClauseId SatProof::registerUnitClause(Lit lit, bool isInput) { return d_unitId[toInt(lit)]; } -void SatProof::removedDfs(Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen){ +void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { return; @@ -447,13 +447,13 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) { /// recording resolutions -void SatProof::startResChain(CRef start) { +void SatProof::startResChain(::Minisat::CRef start) { ClauseId id = getClauseId(start); ResChain* res = new ResChain(id); d_resStack.push_back(res); } -void SatProof::addResolutionStep(Lit lit, CRef clause, bool sign) { +void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { ClauseId id = registerClause(clause); ResChain* res = d_resStack.back(); res->addStep(lit, id, sign); @@ -468,7 +468,7 @@ void SatProof::endResChain(CRef clause) { } -void SatProof::endResChain(Lit lit) { +void SatProof::endResChain(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); ClauseId id = registerUnitClause(lit); ResChain* res = d_resStack.back(); @@ -478,7 +478,7 @@ void SatProof::endResChain(Lit lit) { d_resStack.pop_back(); } -void SatProof::storeLitRedundant(Lit lit) { +void SatProof::storeLitRedundant(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); ResChain* res = d_resStack.back(); res->addRedundantLit(lit); @@ -486,17 +486,17 @@ void SatProof::storeLitRedundant(Lit lit) { /// constructing resolutions -void SatProof::resolveOutUnit(Lit lit) { +void SatProof::resolveOutUnit(::Minisat::Lit lit) { ClauseId id = resolveUnit(~lit); ResChain* res = d_resStack.back(); res->addStep(lit, id, !sign(lit)); } -void SatProof::storeUnitResolution(Lit lit) { +void SatProof::storeUnitResolution(::Minisat::Lit lit) { resolveUnit(lit); } -ClauseId SatProof::resolveUnit(Lit lit) { +ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { // first check if we already have a resolution for lit if(isUnit(lit)) { ClauseId id = getClauseId(lit); @@ -529,7 +529,7 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::finalizeProof(CRef conflict_ref) { +void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); //ClauseId conflict_id = getClauseId(conflict_ref); ClauseId conflict_id = registerClause(conflict_ref); //FIXME @@ -548,7 +548,7 @@ void SatProof::finalizeProof(CRef conflict_ref) { /// CRef manager -void SatProof::updateCRef(CRef oldref, CRef newref) { +void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) { if (d_clauseId.find(oldref) == d_clauseId.end()) { return; } @@ -577,7 +577,7 @@ void SatProof::markDeleted(CRef clause) { /// LFSCSatProof class -string LFSCSatProof::varName(Lit lit) { +std::string LFSCSatProof::varName(::Minisat::Lit lit) { ostringstream os; if (sign(lit)) { os << "(neg v"<