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.

1 files changed, 215 insertions, 181 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 Solver>
+class ProofProxy;
+} /* namespace CVC4 */
 
+namespace CVC4 {
 /**
  * Helper debugging functions
  */
-template <class Solver> void printDebug(typename Solver::TLit l);
-template <class Solver> void printDebug(typename Solver::TClause& c);
+template <class Solver>
+void printDebug(typename Solver::TLit l);
+template <class Solver>
+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 <class Solver>
 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 Solver>
 class ResChain {
-public:
-  typedef std::vector< ResStep<Solver> > ResSteps;
-  typedef std::set < typename Solver::TLit> LitSet;
-
-private:
-  ClauseId       d_start;
-  ResSteps       d_steps;
-  LitSet*        d_redundantLits;
-public:
+ public:
+  typedef std::vector<ResStep<Solver> > ResSteps;
+  typedef std::set<typename Solver::TLit> 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 Solver> 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<class Solver>
+template <class Solver>
 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<Solver>* >      IdResMap;
-  typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
-  typedef std::vector   < ResChain<Solver>* >       ResStack;
-  //typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
-  typedef std::set < ClauseId > IdSet;
-  typedef std::vector < typename Solver::TLit > LitVector;
-  typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause& > IdToMinisatClause;
-  typedef __gnu_cxx::hash_map<ClauseId, LitVector* > 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<Solver>*         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<Solver> ResolutionChain;
+
+  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, ResolutionChain*> IdResMap;
+  typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap;
+  typedef std::vector<ResolutionChain*> ResStack;
+  typedef std::set<ClauseId> IdSet;
+  typedef std::vector<typename Solver::TLit> LitVector;
+  typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&>
+      IdToMinisatClause;
+  typedef __gnu_cxx::hash_map<ClauseId, LitVector*> 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<Solver>* 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<Solver>* 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<Solver>* 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<Solver>* getProxy() {return d_proxy; }
+  ProofProxy<Solver>* 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<Solver>* 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<Solver>* 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<ClauseId, int> d_glueMap;
   struct Statistics {
     IntStat d_numLearnedClauses;
@@ -320,49 +356,47 @@ private:
   };
 
   Statistics d_statistics;
-};/* class TSatProof */
+}; /* class TSatProof */
 
 template <class S>
 class ProofProxy {
-private:
+ private:
   TSatProof<S>* d_proof;
-public:
+
+ public:
   ProofProxy(TSatProof<S>* pf);
   void updateCRef(typename S::TCRef oldref, typename S::TCRef newref);
-};/* class ProofProxy */
-
+}; /* class ProofProxy */
 
 template <class SatSolver>
 class LFSCSatProof : public TSatProof<SatSolver> {
-private:
-
-public:
-  LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false)
-    : TSatProof<SatSolver>(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<SatSolver>(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<class Solver>
+template <class Solver>
 prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
 
-
 /**
  * Convert from minisat clause to SatClause
  *
  * @param minisat_cl
  * @param sat_cl
  */
-template<class Solver>
+template <class Solver>
 void toSatClause(const typename Solver::TClause& minisat_cl,
                  prop::SatClause& sat_cl);
 
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
 
 #endif /* __CVC4__SAT__PROOF_H */