diff options
Diffstat (limited to 'src/proof/sat_proof.cpp')
| -rw-r--r-- | src/proof/sat_proof.cpp | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 3077f08ed..7867f1ddc 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -21,7 +21,7 @@ #include "prop/minisat/minisat.h" using namespace std; -using namespace Minisat; +using namespace CVC4::Minisat; using namespace CVC4::prop; namespace CVC4 { @@ -259,7 +259,7 @@ bool SatProof::checkResolution(ClauseId id) { /// helper methods -ClauseId SatProof::getClauseId(::Minisat::CRef ref) { +ClauseId SatProof::getClauseId(Minisat::CRef ref) { if(d_clauseId.find(ref) == d_clauseId.end()) { Debug("proof:sat") << "Missing clause \n"; } @@ -268,7 +268,7 @@ ClauseId SatProof::getClauseId(::Minisat::CRef ref) { } -ClauseId SatProof::getClauseId(::Minisat::Lit lit) { +ClauseId SatProof::getClauseId(Minisat::Lit lit) { Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); return d_unitId[toInt(lit)]; } @@ -298,11 +298,11 @@ bool SatProof::isUnit(ClauseId id) { return d_idUnit.find(id) != d_idUnit.end(); } -bool SatProof::isUnit(::Minisat::Lit lit) { +bool SatProof::isUnit(Minisat::Lit lit) { return d_unitId.find(toInt(lit)) != d_unitId.end(); } -ClauseId SatProof::getUnitId(::Minisat::Lit lit) { +ClauseId SatProof::getUnitId(Minisat::Lit lit) { Assert(isUnit(lit)); return d_unitId[toInt(lit)]; } @@ -363,7 +363,7 @@ void SatProof::printRes(ResChain* res) { /// registration methods -ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) { +ClauseId SatProof::registerClause(Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) { Debug("cores") << "registerClause " << proof_id << std::endl; Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); @@ -385,7 +385,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6 return d_clauseId[clause]; } -ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) { +ClauseId SatProof::registerUnitClause(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) { Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl; UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { @@ -407,7 +407,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6 return d_unitId[toInt(lit)]; } -void SatProof::removedDfs(::Minisat::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; @@ -483,13 +483,13 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) { /// recording resolutions -void SatProof::startResChain(::Minisat::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(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { +void SatProof::addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign) { ClauseId id = registerClause(clause, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); res->addStep(lit, id, sign); @@ -504,7 +504,7 @@ void SatProof::endResChain(CRef clause) { } -void SatProof::endResChain(::Minisat::Lit lit) { +void SatProof::endResChain(Minisat::Lit lit) { Assert(d_resStack.size() > 0); ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); @@ -512,7 +512,7 @@ void SatProof::endResChain(::Minisat::Lit lit) { d_resStack.pop_back(); } -void SatProof::storeLitRedundant(::Minisat::Lit lit) { +void SatProof::storeLitRedundant(Minisat::Lit lit) { Assert(d_resStack.size() > 0); ResChain* res = d_resStack.back(); res->addRedundantLit(lit); @@ -520,18 +520,18 @@ void SatProof::storeLitRedundant(::Minisat::Lit lit) { /// constructing resolutions -void SatProof::resolveOutUnit(::Minisat::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(::Minisat::Lit lit) { +void SatProof::storeUnitResolution(Minisat::Lit lit) { Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; resolveUnit(lit); } -ClauseId SatProof::resolveUnit(::Minisat::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); @@ -566,7 +566,7 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) { +void SatProof::storeUnitConflict(Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) { Debug("cores") << "STORE UNIT CONFLICT" << std::endl; Assert(!d_storedUnitConflict); d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id); @@ -574,11 +574,11 @@ void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, u Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n"; } -void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { +void SatProof::finalizeProof(Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); - Assert(conflict_ref != ::Minisat::CRef_Undef); + Assert(conflict_ref != Minisat::CRef_Undef); ClauseId conflict_id; - if (conflict_ref == ::Minisat::CRef_Lazy) { + if (conflict_ref == Minisat::CRef_Lazy) { Assert(d_storedUnitConflict); conflict_id = d_unitConflictId; @@ -616,7 +616,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { /// CRef manager -void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) { +void SatProof::updateCRef(Minisat::CRef oldref, Minisat::CRef newref) { if (d_clauseId.find(oldref) == d_clauseId.end()) { return; } |