From 653828ccb09cdbd80dd8f3b40e4b664a8745081b Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 26 Apr 2016 14:51:04 -0700 Subject: 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 +++++++++++++++++++++++++++----------------------- 1 file changed, 215 insertions(+), 181 deletions(-) (limited to 'src/proof/sat_proof.h') 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 */ -- cgit v1.2.3