diff options
Diffstat (limited to 'src/proof/sat_proof.cpp')
-rw-r--r-- | src/proof/sat_proof.cpp | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 2c86d45a4..3077f08ed 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -167,6 +167,7 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_idClause(), d_clauseId(), d_idUnit(), + d_unitId(), d_deleted(), d_inputClauses(), d_lemmaClauses(), @@ -185,6 +186,9 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : { d_proxy = new ProofProxy(this); } +SatProof::~SatProof() { + delete d_proxy; +} /** * Returns true if the resolution chain corresponding to id @@ -365,15 +369,15 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6 ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); - d_clauseId[clause] = newId; - d_idClause[newId] = clause; + d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); + d_idClause.insert(IdCRefMap::value_type(newId, clause)); if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses[newId] = proof_id; + d_inputClauses.insert(IdProofRuleMap::value_type(newId, proof_id)); } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses[newId] = proof_id; + d_lemmaClauses.insert(IdProofRuleMap::value_type(newId, proof_id)); } } Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n"; @@ -386,15 +390,16 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6 UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); - d_unitId[toInt(lit)] = newId; - d_idUnit[newId] = lit; + d_unitId.insert(UnitIdMap::value_type(toInt(lit), newId)); + d_idUnit.insert(IdUnitMap::value_type(newId, lit)); + if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses[newId] = proof_id; + d_inputClauses.insert(IdProofRuleMap::value_type(newId, proof_id)); } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses[newId] = proof_id; + d_lemmaClauses.insert(IdProofRuleMap::value_type(newId, proof_id)); } } Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n"; |