From 653828ccb09cdbd80dd8f3b40e4b664a8745081b Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 26 Apr 2016 14:51:04 -0700 Subject: [PATCH] Fixing memory leaks for garbage collection of ResChains in the sat proof implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this. --- src/proof/sat_proof.h | 396 +++++++++-------- src/proof/sat_proof_implementation.h | 641 +++++++++++++++------------ 2 files changed, 574 insertions(+), 463 deletions(-) diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index d94b61bf3..54ad28377 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -34,175 +34,99 @@ #include "util/proof.h" #include "util/statistics_registry.h" +// Forward declarations. namespace CVC4 { - class CnfProof; +template +class ProofProxy; +} /* namespace CVC4 */ +namespace CVC4 { /** * Helper debugging functions */ -template void printDebug(typename Solver::TLit l); -template void printDebug(typename Solver::TClause& c); +template +void printDebug(typename Solver::TLit l); +template +void printDebug(typename Solver::TClause& c); enum ClauseKind { INPUT, - THEORY_LEMMA, // we need to distinguish because we must reprove deleted theory lemmas + THEORY_LEMMA, // we need to distinguish because we must reprove deleted + // theory lemmas LEARNT -};/* enum ClauseKind */ - +}; /* enum ClauseKind */ template struct ResStep { typename Solver::TLit lit; ClauseId id; bool sign; - ResStep(typename Solver::TLit l, ClauseId i, bool s) : - lit(l), - id(i), - sign(s) - {} -};/* struct ResStep */ + ResStep(typename Solver::TLit l, ClauseId i, bool s) + : lit(l), id(i), sign(s) {} +}; /* struct ResStep */ template class ResChain { -public: - typedef std::vector< ResStep > ResSteps; - typedef std::set < typename Solver::TLit> LitSet; - -private: - ClauseId d_start; - ResSteps d_steps; - LitSet* d_redundantLits; -public: + public: + typedef std::vector > ResSteps; + typedef std::set LitSet; + ResChain(ClauseId start); + ~ResChain(); + void addStep(typename Solver::TLit, ClauseId, bool); - bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } + bool redundantRemoved() { + return (d_redundantLits == NULL || d_redundantLits->empty()); + } void addRedundantLit(typename Solver::TLit lit); - ~ResChain(); - // accessor methods - ClauseId getStart() { return d_start; } - ResSteps& getSteps() { return d_steps; } - LitSet* getRedundant() { return d_redundantLits; } -};/* class ResChain */ -template class ProofProxy; + // accessor methods + ClauseId getStart() const { return d_start; } + const ResSteps& getSteps() const { return d_steps; } + LitSet* getRedundant() const { return d_redundantLits; } -class CnfProof; + private: + ClauseId d_start; + ResSteps d_steps; + LitSet* d_redundantLits; +}; /* class ResChain */ -template +template class TSatProof { -protected: - typedef std::set < typename Solver::TLit> LitSet; - typedef std::set < typename Solver::TVar> VarSet; - typedef std::hash_map < ClauseId, typename Solver::TCRef > IdCRefMap; - typedef std::hash_map < typename Solver::TCRef, ClauseId > ClauseIdMap; - typedef std::hash_map < ClauseId, typename Solver::TLit> IdUnitMap; - typedef std::hash_map < int, ClauseId> UnitIdMap; - typedef std::hash_map < ClauseId, ResChain* > IdResMap; - typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; - typedef std::vector < ResChain* > ResStack; - //typedef std::hash_map IdToSatClause; - typedef std::set < ClauseId > IdSet; - typedef std::vector < typename Solver::TLit > LitVector; - typedef __gnu_cxx::hash_map IdToMinisatClause; - typedef __gnu_cxx::hash_map IdToConflicts; - - typename Solver::Solver* d_solver; - CnfProof* d_cnfProof; - - // clauses - IdCRefMap d_idClause; - ClauseIdMap d_clauseId; - IdUnitMap d_idUnit; - UnitIdMap d_unitId; - IdHashSet d_deleted; - IdToSatClause d_deletedTheoryLemmas; - -protected: - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; - VarSet d_assumptions; // assumption literals for bv solver - IdHashSet d_assumptionConflicts; // assumption conflicts not actually added to SAT solver - IdToConflicts d_assumptionConflictsDebug; - - // resolutions - IdResMap d_resChains; - ResStack d_resStack; - bool d_checkRes; - - const ClauseId d_emptyClauseId; - const ClauseId d_nullId; - // proxy class to break circular dependencies - ProofProxy* d_proxy; - - // temporary map for updating CRefs - ClauseIdMap d_temp_clauseId; - IdCRefMap d_temp_idClause; - - // unit conflict - ClauseId d_unitConflictId; - bool d_storedUnitConflict; - - ClauseId d_trueLit; - ClauseId d_falseLit; - - std::string d_name; -public: + protected: + typedef ResChain ResolutionChain; + + typedef std::set LitSet; + typedef std::set VarSet; + typedef std::hash_map IdCRefMap; + typedef std::hash_map ClauseIdMap; + typedef std::hash_map IdUnitMap; + typedef std::hash_map UnitIdMap; + typedef std::hash_map IdResMap; + typedef std::hash_map IdProofRuleMap; + typedef std::vector ResStack; + typedef std::set IdSet; + typedef std::vector LitVector; + typedef __gnu_cxx::hash_map + IdToMinisatClause; + typedef __gnu_cxx::hash_map IdToConflicts; + + public: TSatProof(Solver* solver, const std::string& name, bool checkRes = false); virtual ~TSatProof(); void setCnfProof(CnfProof* cnf_proof); -protected: - void print(ClauseId id); - void printRes(ClauseId id); - void printRes(ResChain* res); - - bool isInputClause(ClauseId id); - bool isLemmaClause(ClauseId id); - bool isAssumptionConflict(ClauseId id); - bool isUnit(ClauseId id); - bool isUnit(typename Solver::TLit lit); - bool hasResolution(ClauseId id); - void createLitSet(ClauseId id, LitSet& set); - void registerResolution(ClauseId id, ResChain* res); - - ClauseId getClauseId(typename Solver::TCRef clause); - ClauseId getClauseId(typename Solver::TLit lit); - typename Solver::TCRef getClauseRef(ClauseId id); - typename Solver::TLit getUnit(ClauseId id); - ClauseId getUnitId(typename Solver::TLit lit); - typename Solver::TClause& getClause(typename Solver::TCRef ref); - void getLitVec(ClauseId id, LitVector& vec); - virtual void toStream(std::ostream& out); - bool checkResolution(ClauseId id); - /** - * Constructs a resolution tree that proves lit - * and returns the ClauseId for the unit clause lit - * @param lit the literal we are proving - * - * @return - */ - ClauseId resolveUnit(typename Solver::TLit lit); - /** - * Does a depth first search on removed literals and adds the literals - * to be removed in the proper order to the stack. - * - * @param lit the literal we are recursing on - * @param removedSet the previously computed set of redundant literals - * @param removeStack the stack of literals in reverse order of resolution - */ - void removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); - void removeRedundantFromRes(ResChain* res, ClauseId id); -public: void startResChain(typename Solver::TLit start); void startResChain(typename Solver::TCRef start); - void addResolutionStep(typename Solver::TLit lit, typename Solver::TCRef clause, bool sign); + void addResolutionStep(typename Solver::TLit lit, + typename Solver::TCRef clause, bool sign); /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter * @param clause the clause the resolution is proving */ - //void endResChain(typename Solver::TCRef clause); + // void endResChain(typename Solver::TCRef clause); void endResChain(typename Solver::TLit lit); void endResChain(ClauseId id); @@ -219,7 +143,8 @@ public: void storeLitRedundant(typename Solver::TLit lit); /// update the CRef Id maps when Minisat does memory reallocation x - void updateCRef(typename Solver::TCRef old_ref, typename Solver::TCRef new_ref); + void updateCRef(typename Solver::TCRef old_ref, + typename Solver::TCRef new_ref); void finishUpdateCRef(); /** @@ -231,25 +156,22 @@ public: /// clause registration methods - ClauseId registerClause(const typename Solver::TCRef clause, - ClauseKind kind); - ClauseId registerUnitClause(const typename Solver::TLit lit, - ClauseKind kind); + ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind); + ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind); void registerTrueLit(const typename Solver::TLit lit); void registerFalseLit(const typename Solver::TLit lit); ClauseId getTrueUnit() const; ClauseId getFalseUnit() const; - void registerAssumption(const typename Solver::TVar var); ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); - ClauseId storeUnitConflict(typename Solver::TLit lit, - ClauseKind kind); + ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind); /** - * Marks the deleted clauses as deleted. Note we may still use them in the final + * Marks the deleted clauses as deleted. Note we may still use them in the + * final * resolution. * @param clause */ @@ -268,43 +190,157 @@ public: */ void storeUnitResolution(typename Solver::TLit lit); - ProofProxy* getProxy() {return d_proxy; } + ProofProxy* getProxy() { return d_proxy; } /** * Constructs the SAT proof for the given clause, * by collecting the needed clauses in the d_seen * data-structures, also notifying the proofmanager. */ void constructProof(ClauseId id); - void constructProof() { - constructProof(d_emptyClauseId); - } + void constructProof() { constructProof(d_emptyClauseId); } void collectClauses(ClauseId id); prop::SatClause* buildClause(ClauseId id); -protected: - IdSet d_seenLearnt; - IdToSatClause d_seenInputs; - IdToSatClause d_seenLemmas; + + virtual void printResolution(ClauseId id, std::ostream& out, + std::ostream& paren) = 0; + virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; + virtual void printResolutionEmptyClause(std::ostream& out, + std::ostream& paren) = 0; + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, + std::ostream& paren) = 0; + + void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); + + void storeClauseGlue(ClauseId clause, int glue); + + protected: + void print(ClauseId id) const; + void printRes(ClauseId id) const; + void printRes(const ResolutionChain& res) const; + + bool isInputClause(ClauseId id) const; + bool isLemmaClause(ClauseId id) const; + bool isAssumptionConflict(ClauseId id) const; + + bool isUnit(ClauseId id) const; + typename Solver::TLit getUnit(ClauseId id) const; + + bool isUnit(typename Solver::TLit lit) const; + ClauseId getUnitId(typename Solver::TLit lit) const; + + + + bool hasResolutionChain(ClauseId id) const; + + /** Returns the resolution chain associated with id. Assert fails if + * hasResolution(id) does not hold. */ + const ResolutionChain& getResolutionChain(ClauseId id) const; + + /** Returns a mutable pointer to the resolution chain associated with id. + * Assert fails if hasResolution(id) does not hold. */ + ResolutionChain* getMutableResolutionChain(ClauseId id); + + void createLitSet(ClauseId id, LitSet& set); + + /** + * Registers a ClauseId with a resolution chain res. + * Takes ownership of the memory associated with res. + */ + void registerResolution(ClauseId id, ResolutionChain* res); + + + bool hasClauseIdForCRef(typename Solver::TCRef clause) const; + ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const; + + bool hasClauseIdForLiteral(typename Solver::TLit lit) const; + ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const; + + bool hasClauseRef(ClauseId id) const; + typename Solver::TCRef getClauseRef(ClauseId id) const; + + + const typename Solver::TClause& getClause(typename Solver::TCRef ref) const; + typename Solver::TClause* getMutableClause(typename Solver::TCRef ref); + + void getLitVec(ClauseId id, LitVector& vec); + virtual void toStream(std::ostream& out); + + bool checkResolution(ClauseId id); + + /** + * Constructs a resolution tree that proves lit + * and returns the ClauseId for the unit clause lit + * @param lit the literal we are proving + * + * @return + */ + ClauseId resolveUnit(typename Solver::TLit lit); + + /** + * Does a depth first search on removed literals and adds the literals + * to be removed in the proper order to the stack. + * + * @param lit the literal we are recursing on + * @param removedSet the previously computed set of redundant literals + * @param removeStack the stack of literals in reverse order of resolution + */ + void removedDfs(typename Solver::TLit lit, LitSet* removedSet, + LitVector& removeStack, LitSet& inClause, LitSet& seen); + void removeRedundantFromRes(ResChain* res, ClauseId id); std::string varName(typename Solver::TLit lit); std::string clauseName(ClauseId id); - void addToProofManager(ClauseId id, ClauseKind kind); void addToCnfProof(ClauseId id); -public: - virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; - virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; - virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren) = 0; - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; - void collectClausesUsed(IdToSatClause& inputs, - IdToSatClause& lemmas); + // Internal data. + typename Solver::Solver* d_solver; + CnfProof* d_cnfProof; - void storeClauseGlue(ClauseId clause, int glue); + // clauses + IdCRefMap d_idClause; + ClauseIdMap d_clauseId; + IdUnitMap d_idUnit; + UnitIdMap d_unitId; + IdHashSet d_deleted; + IdToSatClause d_deletedTheoryLemmas; + + IdHashSet d_inputClauses; + IdHashSet d_lemmaClauses; + VarSet d_assumptions; // assumption literals for bv solver + IdHashSet d_assumptionConflicts; // assumption conflicts not actually added + // to SAT solver + IdToConflicts d_assumptionConflictsDebug; + + // resolutions + IdResMap d_resolutionChains; + ResStack d_resStack; + bool d_checkRes; + const ClauseId d_emptyClauseId; + const ClauseId d_nullId; + // proxy class to break circular dependencies + ProofProxy* d_proxy; + // temporary map for updating CRefs + ClauseIdMap d_temp_clauseId; + IdCRefMap d_temp_idClause; -private: + // unit conflict + ClauseId d_unitConflictId; + bool d_storedUnitConflict; + + ClauseId d_trueLit; + ClauseId d_falseLit; + + std::string d_name; + + IdSet d_seenLearnt; + IdToSatClause d_seenInputs; + IdToSatClause d_seenLemmas; + + private: __gnu_cxx::hash_map d_glueMap; struct Statistics { IntStat d_numLearnedClauses; @@ -320,49 +356,47 @@ private: }; Statistics d_statistics; -};/* class TSatProof */ +}; /* class TSatProof */ template class ProofProxy { -private: + private: TSatProof* d_proof; -public: + + public: ProofProxy(TSatProof* pf); void updateCRef(typename S::TCRef oldref, typename S::TCRef newref); -};/* class ProofProxy */ - +}; /* class ProofProxy */ template class LFSCSatProof : public TSatProof { -private: - -public: - LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false) - : TSatProof(solver, name, checkRes) - {} - virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); + private: + public: + LFSCSatProof(SatSolver* solver, const std::string& name, + bool checkRes = false) + : TSatProof(solver, name, checkRes) {} + virtual void printResolution(ClauseId id, std::ostream& out, + std::ostream& paren); virtual void printResolutions(std::ostream& out, std::ostream& paren); - virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren); - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren); -};/* class LFSCSatProof */ - - + virtual void printResolutionEmptyClause(std::ostream& out, + std::ostream& paren); + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, + std::ostream& paren); +}; /* class LFSCSatProof */ -template +template prop::SatLiteral toSatLiteral(typename Solver::TLit lit); - /** * Convert from minisat clause to SatClause * * @param minisat_cl * @param sat_cl */ -template +template void toSatClause(const typename Solver::TClause& minisat_cl, prop::SatClause& sat_cl); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index e773e4b47..a22e38f72 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -32,29 +32,28 @@ namespace CVC4 { template -void printLit (typename Solver::TLit l) { +void printLit(typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; } template -void printClause (typename Solver::TClause& c) { +void printClause(const typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } template -void printClause (std::vector& c) { +void printClause(const std::vector& c) { for (unsigned i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } - template void printLitSet(const std::set& s) { - typename std::set < typename Solver::TLit>::const_iterator it = s.begin(); - for(; it != s.end(); ++it) { + typename std::set::const_iterator it = s.begin(); + for (; it != s.end(); ++it) { printLit(*it); Debug("proof:sat") << " "; } @@ -63,18 +62,17 @@ void printLitSet(const std::set& s) { // purely debugging functions template -void printDebug (typename Solver::TLit l) { +void printDebug(typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; } template -void printDebug (typename Solver::TClause& c) { +void printDebug(typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } Debug("proof:sat") << std::endl; } - /** * Converts the clause associated to id to a set of literals * @@ -84,11 +82,11 @@ void printDebug (typename Solver::TClause& c) { template void TSatProof::createLitSet(ClauseId id, LitSet& set) { Assert(set.empty()); - if(isUnit(id)) { + if (isUnit(id)) { set.insert(getUnit(id)); return; } - if ( id == d_emptyClauseId) { + if (id == d_emptyClauseId) { return; } // if it's an assumption @@ -101,13 +99,12 @@ void TSatProof::createLitSet(ClauseId id, LitSet& set) { } typename Solver::TCRef ref = getClauseRef(id); - typename Solver::TClause& c = getClause(ref); + const typename Solver::TClause& c = getClause(ref); for (int i = 0; i < c.size(); i++) { set.insert(c[i]); } } - /** * Resolves clause1 and clause2 on variable var and stores the * result in clause1 @@ -124,8 +121,8 @@ bool resolve(const typename Solver::TLit v, typename Solver::TLit var = sign(v) ? ~v : v; if (s) { // literal appears positive in the first clause - if( !clause2.count(~var)) { - if(Debug.isOn("proof:sat")) { + if (!clause2.count(~var)) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof:resolve: Missing literal "; printLit(var); Debug("proof:sat") << std::endl; @@ -135,13 +132,13 @@ bool resolve(const typename Solver::TLit v, clause1.erase(var); clause2.erase(~var); typename std::set::iterator it = clause2.begin(); - for (; it!= clause2.end(); ++it) { + for (; it != clause2.end(); ++it) { clause1.insert(*it); } } else { // literal appears negative in the first clause - if( !clause1.count(~var) || !clause2.count(var)) { - if(Debug.isOn("proof:sat")) { + if (!clause1.count(~var) || !clause2.count(var)) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof:resolve: Missing literal "; printLit(var); Debug("proof:sat") << std::endl; @@ -151,7 +148,7 @@ bool resolve(const typename Solver::TLit v, clause1.erase(~var); clause2.erase(var); typename std::set::iterator it = clause2.begin(); - for (; it!= clause2.end(); ++it) { + for (; it != clause2.end(); ++it) { clause1.insert(*it); } } @@ -160,13 +157,19 @@ bool resolve(const typename Solver::TLit v, /// ResChain template -ResChain::ResChain(ClauseId start) : - d_start(start), - d_steps(), - d_redundantLits(NULL) - {} +ResChain::ResChain(ClauseId start) + : d_start(start), d_steps(), d_redundantLits(NULL) {} + +template +ResChain::~ResChain() { + if (d_redundantLits != NULL) { + delete d_redundantLits; + } +} + template -void ResChain::addStep(typename Solver::TLit lit, ClauseId id, bool sign) { +void ResChain::addStep(typename Solver::TLit lit, ClauseId id, + bool sign) { ResStep step(lit, id, sign); d_steps.push_back(step); } @@ -181,50 +184,47 @@ void ResChain::addRedundantLit(typename Solver::TLit lit) { } } - /// ProxyProof template -ProofProxy::ProofProxy(TSatProof* proof): - d_proof(proof) -{} +ProofProxy::ProofProxy(TSatProof* proof) : d_proof(proof) {} template -void ProofProxy::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { +void ProofProxy::updateCRef(typename Solver::TCRef oldref, + typename Solver::TCRef newref) { d_proof->updateCRef(oldref, newref); } - /// SatProof template -TSatProof::TSatProof(Solver* solver, const std::string& name, bool checkRes) - : d_solver(solver) - , d_cnfProof(NULL) - , d_idClause() - , d_clauseId() - , d_idUnit() - , d_deleted() - , d_inputClauses() - , d_lemmaClauses() - , d_assumptions() - , d_assumptionConflicts() - , d_assumptionConflictsDebug() - , d_resChains() - , d_resStack() - , d_checkRes(checkRes) - , d_emptyClauseId(ClauseIdEmpty) - , d_nullId(-2) - , d_temp_clauseId() - , d_temp_idClause() - , d_unitConflictId() - , d_storedUnitConflict(false) - , d_trueLit(ClauseIdUndef) - , d_falseLit(ClauseIdUndef) - , d_name(name) - , d_seenLearnt() - , d_seenInputs() - , d_seenLemmas() - , d_statistics(name) -{ +TSatProof::TSatProof(Solver* solver, const std::string& name, + bool checkRes) + : d_solver(solver), + d_cnfProof(NULL), + d_idClause(), + d_clauseId(), + d_idUnit(), + d_deleted(), + d_inputClauses(), + d_lemmaClauses(), + d_assumptions(), + d_assumptionConflicts(), + d_assumptionConflictsDebug(), + d_resolutionChains(), + d_resStack(), + d_checkRes(checkRes), + d_emptyClauseId(ClauseIdEmpty), + d_nullId(-2), + d_temp_clauseId(), + d_temp_idClause(), + d_unitConflictId(), + d_storedUnitConflict(false), + d_trueLit(ClauseIdUndef), + d_falseLit(ClauseIdUndef), + d_name(name), + d_seenLearnt(), + d_seenInputs(), + d_seenLemmas(), + d_statistics(name) { d_proxy = new ProofProxy(this); } @@ -233,34 +233,52 @@ TSatProof::~TSatProof() { delete d_proxy; // FIXME: double free if deleted clause also appears in d_seenLemmas? - IdToSatClause::iterator it = d_deletedTheoryLemmas.begin(); - IdToSatClause::iterator end = d_deletedTheoryLemmas.end(); + IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin(); + IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end(); for (; it != end; ++it) { ClauseId id = it->first; // otherwise deleted in next loop - if (d_seenLemmas.find(id) == d_seenLemmas.end()) + if (d_seenLemmas.find(id) == d_seenLemmas.end()) { delete it->second; + } } - IdToSatClause::iterator seen_it = d_seenLemmas.begin(); - IdToSatClause::iterator seen_end = d_seenLemmas.end(); + IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin(); + IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end(); - for (; seen_it != seen_end; ++seen_it) { - delete seen_it->second; + for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) { + delete seen_lemma_it->second; } - seen_it = d_seenInputs.begin(); - seen_end = d_seenInputs.end(); + IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin(); + IdToSatClause::const_iterator seen_input_end = d_seenInputs.end(); - for (; seen_it != seen_end; ++seen_it) { - delete seen_it->second; + for (; seen_input_it != seen_input_end; ++seen_input_it) { + delete seen_input_it->second; + } + + // TODO: Have an expert check this. + typedef typename IdResMap::const_iterator ResolutionChainIterator; + ResolutionChainIterator resolution_it = d_resolutionChains.begin(); + ResolutionChainIterator resolution_it_end = d_resolutionChains.end(); + for (; resolution_it != resolution_it_end; ++resolution_it) { + ResChain* current = resolution_it->second; + delete current; + } + + typename ResStack::const_iterator resolution_stack_it = d_resStack.begin(); + typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end(); + for (; resolution_stack_it != resolution_stack_it_end; + ++resolution_stack_it) { + ResChain* current = *resolution_stack_it; + delete current; } } template void TSatProof::setCnfProof(CnfProof* cnf_proof) { - Assert (d_cnfProof == NULL); + Assert(d_cnfProof == NULL); d_cnfProof = cnf_proof; } @@ -273,19 +291,19 @@ void TSatProof::setCnfProof(CnfProof* cnf_proof) { */ template bool TSatProof::checkResolution(ClauseId id) { - if(d_checkRes) { + if (d_checkRes) { bool validRes = true; - Assert(d_resChains.find(id) != d_resChains.end()); - ResChain* res = d_resChains[id]; + Assert(hasResolutionChain(id)); + const ResolutionChain& res = getResolutionChain(id); LitSet clause1; - createLitSet(res->getStart(), clause1); - typename ResChain::ResSteps& steps = res->getSteps(); + createLitSet(res.getStart(), clause1); + const typename ResolutionChain::ResSteps& steps = res.getSteps(); for (unsigned i = 0; i < steps.size(); i++) { - typename Solver::TLit var = steps[i].lit; + typename Solver::TLit var = steps[i].lit; LitSet clause2; - createLitSet (steps[i].id, clause2); - bool res = resolve (var, clause1, clause2, steps[i].sign); - if(res == false) { + createLitSet(steps[i].id, clause2); + bool res = resolve(var, clause1, clause2, steps[i].sign); + if (res == false) { validRes = false; break; } @@ -307,8 +325,9 @@ bool TSatProof::checkResolution(ClauseId id) { for (unsigned i = 0; i < c.size(); ++i) { int count = clause1.erase(c[i]); if (count == 0) { - if(Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + if (Debug.isOn("proof:sat")) { + Debug("proof:sat") + << "proof:checkResolution::literal not in computed result "; printLit(c[i]); Debug("proof:sat") << "\n"; } @@ -316,9 +335,10 @@ bool TSatProof::checkResolution(ClauseId id) { } } validRes = clause1.empty(); - if (! validRes) { - if(Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + if (!validRes) { + if (Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, " + "unremoved literals: \n"; printLitSet(clause1); Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; printClause(c); @@ -331,37 +351,54 @@ bool TSatProof::checkResolution(ClauseId id) { } } - - - /// helper methods template -ClauseId TSatProof::getClauseId(typename Solver::TCRef ref) { - if(d_clauseId.find(ref) == d_clauseId.end()) { +bool TSatProof::hasClauseIdForCRef(typename Solver::TCRef ref) const { + return d_clauseId.find(ref) != d_clauseId.end(); +} + +template +ClauseId TSatProof::getClauseIdForCRef( + typename Solver::TCRef ref) const { + if (d_clauseId.find(ref) == d_clauseId.end()) { Debug("proof:sat") << "Missing clause \n"; } - Assert(d_clauseId.find(ref) != d_clauseId.end()); - return d_clauseId[ref]; + Assert(hasClauseIdForCRef(ref)); + return d_clauseId.find(ref)->second; +} + +template +bool TSatProof::hasClauseIdForLiteral(typename Solver::TLit lit) const { + return d_unitId.find(toInt(lit)) != d_unitId.end(); +} + +template +ClauseId TSatProof::getClauseIdForLiteral( + typename Solver::TLit lit) const { + Assert(hasClauseIdForLiteral(lit)); + return d_unitId.find(toInt(lit))->second; } template -ClauseId TSatProof::getClauseId(typename Solver::TLit lit) { - Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); - return d_unitId[toInt(lit)]; +bool TSatProof::hasClauseRef(ClauseId id) const { + return d_idClause.find(id) != d_idClause.end(); } + template -typename Solver::TCRef TSatProof::getClauseRef(ClauseId id) { - if (d_idClause.find(id) == d_idClause.end()) { - Debug("proof:sat") << "proof:getClauseRef cannot find clause "<::getClauseRef(ClauseId id) const { + if (!hasClauseRef(id)) { + Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " " + << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" + : "") + << (isUnit(id) ? "Unit" : "") << std::endl; } - Assert(d_idClause.find(id) != d_idClause.end()); - return d_idClause[id]; + Assert(hasClauseRef(id)); + return d_idClause.find(id)->second; } template -typename Solver::TClause& TSatProof::getClause(typename Solver::TCRef ref) { +const typename Solver::TClause& TSatProof::getClause( + typename Solver::TCRef ref) const { Assert(ref != Solver::TCRef_Undef); Assert(ref >= 0 && ref < d_solver->ca.size()); return d_solver->ca[ref]; @@ -379,85 +416,106 @@ void TSatProof::getLitVec(ClauseId id, LitVector& vec) { return; } typename Solver::TCRef cref = getClauseRef(id); - typename Solver::TClause& cl = getClause(cref); + const typename Solver::TClause& cl = getClause(cref); for (int i = 0; i < cl.size(); ++i) { vec.push_back(cl[i]); } } - template -typename Solver::TLit TSatProof::getUnit(ClauseId id) { - Assert(d_idUnit.find(id) != d_idUnit.end()); - return d_idUnit[id]; +bool TSatProof::isUnit(ClauseId id) const { + return d_idUnit.find(id) != d_idUnit.end(); } + template -bool TSatProof::isUnit(ClauseId id) { - return d_idUnit.find(id) != d_idUnit.end(); +typename Solver::TLit TSatProof::getUnit(ClauseId id) const { + Assert(isUnit(id)); + return d_idUnit.find(id)->second; } + template -bool TSatProof::isUnit(typename Solver::TLit lit) { +bool TSatProof::isUnit(typename Solver::TLit lit) const { return d_unitId.find(toInt(lit)) != d_unitId.end(); } + template -ClauseId TSatProof::getUnitId(typename Solver::TLit lit) { +ClauseId TSatProof::getUnitId(typename Solver::TLit lit) const { Assert(isUnit(lit)); - return d_unitId[toInt(lit)]; + return d_unitId.find(toInt(lit))->second; } + template -bool TSatProof::hasResolution(ClauseId id) { - return d_resChains.find(id) != d_resChains.end(); +bool TSatProof::hasResolutionChain(ClauseId id) const { + return d_resolutionChains.find(id) != d_resolutionChains.end(); } + template -bool TSatProof::isInputClause(ClauseId id) { - return (d_inputClauses.find(id) != d_inputClauses.end()); +const typename TSatProof::ResolutionChain& +TSatProof::getResolutionChain(ClauseId id) const { + Assert(hasResolutionChain(id)); + const ResolutionChain* chain = d_resolutionChains.find(id)->second; + return *chain; } + template -bool TSatProof::isLemmaClause(ClauseId id) { - return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); +typename TSatProof::ResolutionChain* +TSatProof::getMutableResolutionChain(ClauseId id) { + Assert(hasResolutionChain(id)); + ResolutionChain* chain = d_resolutionChains.find(id)->second; + return chain; } template -bool TSatProof::isAssumptionConflict(ClauseId id) { - return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +bool TSatProof::isInputClause(ClauseId id) const { + return d_inputClauses.find(id) != d_inputClauses.end(); } +template +bool TSatProof::isLemmaClause(ClauseId id) const { + return d_lemmaClauses.find(id) != d_lemmaClauses.end(); +} + +template +bool TSatProof::isAssumptionConflict(ClauseId id) const { + return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +} template -void TSatProof::print(ClauseId id) { +void TSatProof::print(ClauseId id) const { if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del"<(getUnit(id)); } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty "<< std::endl; - } - else { + Debug("proof:sat") << "empty " << std::endl; + } else { typename Solver::TCRef ref = getClauseRef(id); printClause(getClause(ref)); } } + template -void TSatProof::printRes(ClauseId id) { - Assert(hasResolution(id)); - Debug("proof:sat") << "id "<< id <<": "; - printRes(d_resChains[id]); +void TSatProof::printRes(ClauseId id) const { + Assert(hasResolutionChain(id)); + Debug("proof:sat") << "id " << id << ": "; + printRes(getResolutionChain(id)); } + template -void TSatProof::printRes(ResChain* res) { - ClauseId start_id = res->getStart(); +void TSatProof::printRes(const ResolutionChain& res) const { + ClauseId start_id = res.getStart(); - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "("; print(start_id); } - typename ResChain::ResSteps& steps = res->getSteps(); - for(unsigned i = 0; i < steps.size(); i++ ) { + const typename ResolutionChain::ResSteps& steps = res.getSteps(); + for (unsigned i = 0; i < steps.size(); i++) { typename Solver::TLit v = steps[i].lit; ClauseId id = steps[i].id; - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "["; printLit(v); Debug("proof:sat") << "] "; @@ -469,8 +527,8 @@ void TSatProof::printRes(ResChain* res) { /// registration methods template - ClauseId TSatProof::registerClause(typename Solver::TCRef clause, - ClauseKind kind) { +ClauseId TSatProof::registerClause(typename Solver::TCRef clause, + ClauseKind kind) { Assert(clause != Solver::TCRef_Undef); typename ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { @@ -484,10 +542,11 @@ template if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); d_lemmaClauses.insert(newId); - Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " - << newId << " = " << *buildClause(newId) - << ". Explainer theory: " << d_cnfProof->getExplainerTheory() - << std::endl; + Debug("pf::sat") + << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; d_cnfProof->registerExplanationLemma(newId); } } @@ -496,15 +555,16 @@ template Assert(kind != INPUT || d_inputClauses.count(id)); Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); - Debug("proof:sat:detailed") << "registerClause CRef: " << clause << " id: " << d_clauseId[clause] - <<" kind: " << kind << "\n"; - //ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); + Debug("proof:sat:detailed") << "registerClause CRef: " << clause + << " id: " << d_clauseId[clause] + << " kind: " << kind << "\n"; + // ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); return id; } template ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, - ClauseKind kind) { + ClauseKind kind) { Debug("cores") << "registerUnitClause " << kind << std::endl; typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { @@ -518,10 +578,10 @@ ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " - << lit - << ". Explainer theory: " << d_cnfProof->getExplainerTheory() - << std::endl; + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "lemma (UNIT CLAUSE): " + << lit << ". Explainer theory: " + << d_cnfProof->getExplainerTheory() << std::endl; d_lemmaClauses.insert(newId); d_cnfProof->registerExplanationLemma(newId); } @@ -530,48 +590,48 @@ ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, Assert(kind != INPUT || d_inputClauses.count(id)); Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); Debug("proof:sat:detailed") << "registerUnitClause id: " << id - <<" kind: " << kind << "\n"; + << " kind: " << kind << "\n"; // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); return id; } template void TSatProof::registerTrueLit(const typename Solver::TLit lit) { - Assert (d_trueLit == ClauseIdUndef); + Assert(d_trueLit == ClauseIdUndef); d_trueLit = registerUnitClause(lit, INPUT); } template void TSatProof::registerFalseLit(const typename Solver::TLit lit) { - Assert (d_falseLit == ClauseIdUndef); + Assert(d_falseLit == ClauseIdUndef); d_falseLit = registerUnitClause(lit, INPUT); } template ClauseId TSatProof::getTrueUnit() const { - Assert (d_trueLit != ClauseIdUndef); + Assert(d_trueLit != ClauseIdUndef); return d_trueLit; } template ClauseId TSatProof::getFalseUnit() const { - Assert (d_falseLit != ClauseIdUndef); + Assert(d_falseLit != ClauseIdUndef); return d_falseLit; } - template void TSatProof::registerAssumption(const typename Solver::TVar var) { - Assert (d_assumptions.find(var) == d_assumptions.end()); + Assert(d_assumptions.find(var) == d_assumptions.end()); d_assumptions.insert(var); } template -ClauseId TSatProof::registerAssumptionConflict(const typename Solver::TLitVec& confl) { +ClauseId TSatProof::registerAssumptionConflict( + const typename Solver::TLitVec& confl) { Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; // Uniqueness is checked in the bit-vector proof // should be vars for (int i = 0; i < confl.size(); ++i) { - Assert (d_assumptions.find(var(confl[i])) != d_assumptions.end()); + Assert(d_assumptions.find(var(confl[i])) != d_assumptions.end()); } ClauseId new_id = ProofManager::currentPM()->nextId(); d_assumptionConflicts.insert(new_id); @@ -588,9 +648,10 @@ ClauseId TSatProof::registerAssumptionConflict(const typename Solver::TL return new_id; } - template -void TSatProof::removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { +void TSatProof::removedDfs(typename Solver::TLit lit, + LitSet* removedSet, LitVector& removeStack, + LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { return; @@ -604,20 +665,21 @@ void TSatProof::removedDfs(typename Solver::TLit lit, LitSet* removedSet } int size = getClause(reason_ref).size(); - for (int i = 1; i < size; i++ ) { + for (int i = 1; i < size; i++) { typename Solver::TLit v = getClause(reason_ref)[i]; - if(inClause.count(v) == 0 && seen.count(v) == 0) { + if (inClause.count(v) == 0 && seen.count(v) == 0) { removedDfs(v, removedSet, removeStack, inClause, seen); } } - if(seen.count(lit) == 0) { + if (seen.count(lit) == 0) { seen.insert(lit); removeStack.push_back(lit); } } template -void TSatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { +void TSatProof::removeRedundantFromRes(ResChain* res, + ClauseId id) { LitSet* removed = res->getRedundant(); if (removed == NULL) { return; @@ -628,11 +690,12 @@ void TSatProof::removeRedundantFromRes(ResChain* res, ClauseId i LitVector removeStack; LitSet seen; - for (typename LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { + for (typename LitSet::iterator it = removed->begin(); it != removed->end(); + ++it) { removedDfs(*it, removed, removeStack, inClause, seen); } - for (int i = removeStack.size()-1; i >= 0; --i) { + for (int i = removeStack.size() - 1; i >= 0; --i) { typename Solver::TLit lit = removeStack[i]; typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); ClauseId reason_id; @@ -655,41 +718,48 @@ void TSatProof::registerResolution(ClauseId id, ResChain* res) { removeRedundantFromRes(res, id); Assert(res->redundantRemoved()); - d_resChains[id] = res; - if(Debug.isOn("proof:sat")) { + // TODO: Have someone with a clue check this. + if (hasResolutionChain(id)) { + ResChain* current = d_resolutionChains.find(id)->second; + delete current; + d_resolutionChains.erase(id); + } + Assert(!hasResolutionChain(id)); + + d_resolutionChains.insert(std::make_pair(id, res)); + if (Debug.isOn("proof:sat")) { printRes(id); } - if(d_checkRes) { + if (d_checkRes) { Assert(checkResolution(id)); } - PSTATS( - d_statistics.d_resChainLengths << ((uint64_t)res->getSteps().size()); - d_statistics.d_avgChainLength.addEntry((uint64_t)res->getSteps().size()); - ++(d_statistics.d_numLearnedClauses); - ) + PSTATS(uint64_t resolutionSteps = + static_cast(res.getSteps().size()); + d_statistics.d_resChainLengths << resolutionSteps; + d_statistics.d_avgChainLength.addEntry(resolutionSteps); + ++(d_statistics.d_numLearnedClauses);) } - /// recording resolutions template void TSatProof::startResChain(typename Solver::TCRef start) { - ClauseId id = getClauseId(start); - ResChain* res = new ResChain(id); + ClauseId id = getClauseIdForCRef(start); + ResolutionChain* res = new ResolutionChain(id); d_resStack.push_back(res); } template void TSatProof::startResChain(typename Solver::TLit start) { ClauseId id = getUnitId(start); - ResChain* res = new ResChain(id); + ResolutionChain* res = new ResolutionChain(id); d_resStack.push_back(res); } - template void TSatProof::addResolutionStep(typename Solver::TLit lit, - typename Solver::TCRef clause, bool sign) { + typename Solver::TCRef clause, + bool sign) { ClauseId id = registerClause(clause, LEARNT); ResChain* res = d_resStack.back(); res->addStep(lit, id, sign); @@ -697,14 +767,13 @@ void TSatProof::addResolutionStep(typename Solver::TLit lit, template void TSatProof::endResChain(ClauseId id) { - Debug("proof:sat:detailed") <<"endResChain " << id << "\n"; + Debug("proof:sat:detailed") << "endResChain " << id << "\n"; Assert(d_resStack.size() > 0); ResChain* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); } - // template // void TSatProof::endResChain(typename Solver::TCRef clause) { // Assert(d_resStack.size() > 0); @@ -718,25 +787,26 @@ template void TSatProof::endResChain(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); ClauseId id = registerUnitClause(lit, LEARNT); - Debug("proof:sat:detailed") <<"endResChain unit " << id << "\n"; - ResChain* res = d_resStack.back(); + Debug("proof:sat:detailed") << "endResChain unit " << id << "\n"; + ResolutionChain* res = d_resStack.back(); d_glueMap[id] = 1; registerResolution(id, res); d_resStack.pop_back(); } - template void TSatProof::cancelResChain() { Assert(d_resStack.size() > 0); + // TODO: Expert check. + ResolutionChain* back = d_resStack.back(); + delete back; d_resStack.pop_back(); } - template void TSatProof::storeLitRedundant(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); - ResChain* res = d_resStack.back(); + ResolutionChain* res = d_resStack.back(); res->addRedundantLit(lit); } @@ -755,9 +825,9 @@ void TSatProof::storeUnitResolution(typename Solver::TLit lit) { template ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { // first check if we already have a resolution for lit - if(isUnit(lit)) { - ClauseId id = getClauseId(lit); - Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + if (isUnit(lit)) { + ClauseId id = getClauseIdForLiteral(lit); + Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id)); return id; } typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); @@ -768,12 +838,13 @@ ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { ResChain* res = new ResChain(reason_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload reason ptr each time. - typename Solver::TClause* reason = &getClause(reason_ref); - for (int i = 0; - i < reason->size(); - i++, reason = &getClause(reason_ref)) { - typename Solver::TLit l = (*reason)[i]; - if(lit != l) { + const typename Solver::TClause& initial_reason = getClause(reason_ref); + size_t current_reason_size = initial_reason.size(); + for (int i = 0; i < current_reason_size; i++) { + const typename Solver::TClause& current_reason = getClause(reason_ref); + current_reason_size = current_reason.size(); + typename Solver::TLit l = current_reason[i]; + if (lit != l) { ClauseId res_id = resolveUnit(~l); res->addStep(l, res_id, !sign(l)); } @@ -787,16 +858,19 @@ void TSatProof::toStream(std::ostream& out) { Debug("proof:sat") << "TSatProof::printProof\n"; Unimplemented("native proof printing not supported yet"); } + template -ClauseId TSatProof::storeUnitConflict(typename Solver::TLit conflict_lit, - ClauseKind kind) { +ClauseId TSatProof::storeUnitConflict( + typename Solver::TLit conflict_lit, ClauseKind kind) { Debug("cores") << "STORE UNIT CONFLICT" << std::endl; Assert(!d_storedUnitConflict); d_unitConflictId = registerUnitClause(conflict_lit, kind); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId + << "\n"; return d_unitConflictId; } + template void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { Assert(d_resStack.size() == 0); @@ -816,24 +890,25 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { return; } else { Assert(!d_storedUnitConflict); - conflict_id = registerClause(conflict_ref, LEARNT); //FIXME + conflict_id = registerClause(conflict_ref, LEARNT); // FIXME } - if(Debug.isOn("proof:sat")) { + if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof::finalizeProof Final Conflict "; print(conflict_id); } + // TODO: Run this rotation by someone. ResChain* res = new ResChain(conflict_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. - typename Solver::TClause* conflict = &getClause(conflict_ref); - for (int i = 0; - i < conflict->size(); - ++i, conflict = &getClause(conflict_ref)) { - typename Solver::TLit lit = (*conflict)[i]; + size_t conflict_size = getClause(conflict_ref).size(); + for (int i = 0; i < conflict_size; ++i) { + const typename Solver::TClause& conflict = getClause(conflict_ref); + typename Solver::TLit lit = conflict[i]; ClauseId res_id = resolveUnit(~lit); res->addStep(lit, res_id, !sign(lit)); + conflict_size = conflict.size(); } registerResolution(d_emptyClauseId, res); } @@ -845,12 +920,13 @@ void TSatProof::updateCRef(typename Solver::TCRef oldref, if (d_clauseId.find(oldref) == d_clauseId.end()) { return; } - ClauseId id = getClauseId(oldref); + ClauseId id = getClauseIdForCRef(oldref); Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); d_temp_clauseId[newref] = id; d_temp_idClause[id] = newref; } + template void TSatProof::finishUpdateCRef() { d_clauseId.swap(d_temp_clauseId); @@ -859,10 +935,11 @@ void TSatProof::finishUpdateCRef() { d_idClause.swap(d_temp_idClause); d_temp_idClause.clear(); } + template void TSatProof::markDeleted(typename Solver::TCRef clause) { - if (d_clauseId.find(clause) != d_clauseId.end()) { - ClauseId id = getClauseId(clause); + if (hasClauseIdForCRef(clause)) { + ClauseId id = getClauseIdForCRef(clause); Assert(d_deleted.find(id) == d_deleted.end()); d_deleted.insert(id); if (isLemmaClause(id)) { @@ -875,14 +952,13 @@ void TSatProof::markDeleted(typename Solver::TCRef clause) { } // template<> -// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, +// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& +// minisat_cl, // prop::SatClause& sat_cl) { // prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); // } - - template void TSatProof::constructProof(ClauseId conflict) { collectClauses(conflict); @@ -894,11 +970,10 @@ std::string TSatProof::clauseName(ClauseId id) { if (isInputClause(id)) { os << ProofManager::getInputClauseName(id, d_name); return os.str(); - } else - if (isLemmaClause(id)) { + } else if (isLemmaClause(id)) { os << ProofManager::getLemmaClauseName(id, d_name); return os.str(); - }else { + } else { os << ProofManager::getLearntClauseName(id, d_name); return os.str(); } @@ -944,17 +1019,15 @@ void TSatProof::collectClauses(ClauseId id) { d_seenLearnt.insert(id); } - Assert(d_resChains.find(id) != d_resChains.end()); - ResChain* res = d_resChains[id]; - PSTATS( - d_statistics.d_usedResChainLengths << ((uint64_t)res->getSteps().size()); - d_statistics.d_usedClauseGlue << ((uint64_t) d_glueMap[id]); - ); - ClauseId start = res->getStart(); + const ResolutionChain& res = getResolutionChain(id); + const typename ResolutionChain::ResSteps& steps = res.getSteps(); + PSTATS(d_statistics.d_usedResChainLengths + << ((uint64_t)steps.size()); + d_statistics.d_usedClauseGlue << ((uint64_t)d_glueMap[id]);); + ClauseId start = res.getStart(); collectClauses(start); - typename ResChain::ResSteps steps = res->getSteps(); - for(size_t i = 0; i < steps.size(); i++) { + for (size_t i = 0; i < steps.size(); i++) { collectClauses(steps[i].id); } } @@ -964,28 +1037,27 @@ void TSatProof::collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas) { inputs = d_seenInputs; lemmas = d_seenLemmas; - PSTATS ( - d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); - d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size()); - ); + PSTATS(d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); + d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size());); } template void TSatProof::storeClauseGlue(ClauseId clause, int glue) { - Assert (d_glueMap.find(clause) == d_glueMap.end()); + Assert(d_glueMap.find(clause) == d_glueMap.end()); d_glueMap.insert(std::make_pair(clause, glue)); } template TSatProof::Statistics::Statistics(const std::string& prefix) - : d_numLearnedClauses("satproof::"+prefix+"::NumLearnedClauses", 0) - , d_numLearnedInProof("satproof::"+prefix+"::NumLearnedInProof", 0) - , d_numLemmasInProof("satproof::"+prefix+"::NumLemmasInProof", 0) - , d_avgChainLength("satproof::"+prefix+"::AvgResChainLength") - , d_resChainLengths("satproof::"+prefix+"::ResChainLengthsHist") - , d_usedResChainLengths("satproof::"+prefix+"::UsedResChainLengthsHist") - , d_clauseGlue("satproof::"+prefix+"::ClauseGlueHist") - , d_usedClauseGlue("satproof::"+prefix+"::UsedClauseGlueHist") { + : d_numLearnedClauses("satproof::" + prefix + "::NumLearnedClauses", 0), + d_numLearnedInProof("satproof::" + prefix + "::NumLearnedInProof", 0), + d_numLemmasInProof("satproof::" + prefix + "::NumLemmasInProof", 0), + d_avgChainLength("satproof::" + prefix + "::AvgResChainLength"), + d_resChainLengths("satproof::" + prefix + "::ResChainLengthsHist"), + d_usedResChainLengths("satproof::" + prefix + + "::UsedResChainLengthsHist"), + d_clauseGlue("satproof::" + prefix + "::ClauseGlueHist"), + d_usedClauseGlue("satproof::" + prefix + "::UsedClauseGlueHist") { smtStatisticsRegistry()->registerStat(&d_numLearnedClauses); smtStatisticsRegistry()->registerStat(&d_numLearnedInProof); smtStatisticsRegistry()->registerStat(&d_numLemmasInProof); @@ -1008,73 +1080,78 @@ TSatProof::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); } - /// LFSCSatProof class template -void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { +void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, + std::ostream& paren) { out << "(satlem_simplify _ _ _ "; - ResChain* res = this->d_resChains[id]; - typename ResChain::ResSteps& steps = res->getSteps(); + const ResChain& res = this->getResolutionChain(id); + const typename ResChain::ResSteps& steps = res.getSteps(); - for (int i = steps.size()-1; i >= 0; i--) { + for (int i = steps.size() - 1; i >= 0; i--) { out << "("; - out << (steps[i].sign? "R" : "Q") << " _ _ "; + out << (steps[i].sign ? "R" : "Q") << " _ _ "; } - ClauseId start_id = res->getStart(); + ClauseId start_id = res.getStart(); out << this->clauseName(start_id) << " "; - for(unsigned i = 0; i < steps.size(); i++) { - prop::SatVariable v = prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); - out << this->clauseName(steps[i].id) << " "<d_name) <<")"; + for (unsigned i = 0; i < steps.size(); i++) { + prop::SatVariable v = + prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); + out << this->clauseName(steps[i].id) << " " + << ProofManager::getVarName(v, this->d_name) << ")"; } if (id == this->d_emptyClauseId) { - out <<"(\\empty empty)"; + out << "(\\empty empty)"; return; } - out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name - paren << "))"; // closing parethesis for lemma binding and satlem + out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem } /// LFSCSatProof class template -void LFSCSatProof::printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) { - Assert (this->isAssumptionConflict(id)); +void LFSCSatProof::printAssumptionsResolution(ClauseId id, + std::ostream& out, + std::ostream& paren) { + Assert(this->isAssumptionConflict(id)); // print the resolution proving the assumption conflict printResolution(id, out, paren); // resolve out assumptions to prove empty clause out << "(satlem_simplify _ _ _ "; - std::vector& confl = *(this->d_assumptionConflictsDebug[id]); + std::vector& confl = + *(this->d_assumptionConflictsDebug[id]); - Assert (confl.size()); + Assert(confl.size()); for (unsigned i = 0; i < confl.size(); ++i) { prop::SatLiteral lit = toSatLiteral(confl[i]); - out <<"("; - out << (lit.isNegated() ? "Q" : "R") <<" _ _ "; + out << "("; + out << (lit.isNegated() ? "Q" : "R") << " _ _ "; } - out << this->clauseName(id)<< " "; + out << this->clauseName(id) << " "; for (int i = confl.size() - 1; i >= 0; --i) { prop::SatLiteral lit = toSatLiteral(confl[i]); prop::SatVariable v = lit.getSatVariable(); - out << "unit"<< v <<" "; - out << ProofManager::getVarName(v, this->d_name) <<")"; + out << "unit" << v << " "; + out << ProofManager::getVarName(v, this->d_name) << ")"; } - out <<"(\\ e e)\n"; - paren <<")"; + out << "(\\ e e)\n"; + paren << ")"; } - template -void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { +void LFSCSatProof::printResolutions(std::ostream& out, + std::ostream& paren) { Debug("bv-proof") << "; print resolutions" << std::endl; std::set::iterator it = this->d_seenLearnt.begin(); - for(; it!= this->d_seenLearnt.end(); ++it) { - if(*it != this->d_emptyClauseId) { + for (; it != this->d_seenLearnt.end(); ++it) { + if (*it != this->d_emptyClauseId) { Debug("bv-proof") << "; print resolution for " << *it << std::endl; printResolution(*it, out, paren); } @@ -1083,29 +1160,29 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& par } template -void LFSCSatProof::printResolutionEmptyClause(std::ostream& out, std::ostream& paren) { +void LFSCSatProof::printResolutionEmptyClause(std::ostream& out, + std::ostream& paren) { printResolution(this->d_emptyClauseId, out, paren); } - inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { - switch(k) { - case CVC4::INPUT: - out << "INPUT"; - break; - case CVC4::THEORY_LEMMA: - out << "THEORY_LEMMA"; - break; - case CVC4::LEARNT: - out << "LEARNT"; - break; - default: - out << "ClauseKind Unknown! [" << unsigned(k) << "]"; + switch (k) { + case CVC4::INPUT: + out << "INPUT"; + break; + case CVC4::THEORY_LEMMA: + out << "THEORY_LEMMA"; + break; + case CVC4::LEARNT: + out << "LEARNT"; + break; + default: + out << "ClauseKind Unknown! [" << unsigned(k) << "]"; } return out; } -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */ -- 2.30.2