diff options
| author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
| commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
| tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/proof/sat_proof.h | |
| parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) | |
squash-merge from proof branch
Diffstat (limited to 'src/proof/sat_proof.h')
| -rw-r--r-- | src/proof/sat_proof.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index ccb81b9ad..9160ebcfb 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -124,7 +124,7 @@ protected: 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; @@ -241,13 +241,13 @@ public: 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); - + /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. @@ -297,12 +297,13 @@ public: 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); + + private: __gnu_cxx::hash_map<ClauseId, int> d_glueMap; struct Statistics { @@ -321,7 +322,6 @@ private: Statistics d_statistics; };/* class TSatProof */ - template <class S> class ProofProxy { private: |