diff options
| author | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
| commit | 08c8433e4ab849024930a8c4dbe8756e13d08099 (patch) | |
| tree | 2515d746c9b190e8770c5c690046410449900d7a /src/proof/sat_proof.h | |
| parent | 000f574406c29df4c60947169ef527ee5316beb7 (diff) | |
fixed uf proof bug: now storing deleted theory lemmas
Diffstat (limited to 'src/proof/sat_proof.h')
| -rw-r--r-- | src/proof/sat_proof.h | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 5a1fa4680..c4936fd88 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -81,14 +81,14 @@ public: LitSet* getRedundant() { return d_redundantLits; } };/* class ResChain */ -typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap; +typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap; typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; typedef std::vector < ResChain* > ResStack; - +typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; @@ -116,11 +116,12 @@ class SatProof { protected: ::Minisat::Solver* d_solver; // clauses - IdClauseMap d_idClause; + IdCRefMap d_idClause; ClauseIdMap d_clauseId; IdUnitMap d_idUnit; UnitIdMap d_unitId; IdHashSet d_deleted; + IdToSatClause d_deletedTheoryLemmas; IdHashSet d_inputClauses; IdHashSet d_lemmaClauses; // resolutions @@ -136,7 +137,7 @@ protected: // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdClauseMap d_temp_idClause; + IdCRefMap d_temp_idClause; // unit conflict ClauseId d_unitConflictId; @@ -223,6 +224,7 @@ public: * @param clause */ void markDeleted(::Minisat::CRef clause); + bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause |