diff options
| -rw-r--r-- | src/proof/proof_manager.cpp | 7 | ||||
| -rw-r--r-- | src/proof/sat_proof.cpp | 21 | ||||
| -rw-r--r-- | src/proof/sat_proof.h | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
4 files changed, 24 insertions, 9 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 4bff66b92..0f9cfa710 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -45,6 +45,13 @@ ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), d_theoryProof(NULL), + d_inputClauses(), + d_theoryLemmas(), + d_theoryPropagations(), + d_inputFormulas(), + d_inputCoreFormulas(), + d_outputCoreFormulas(), + d_nextId(0), d_fullProof(NULL), d_format(format), d_deps(), 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"; diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index ef4e7a5aa..7c195c83d 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -139,7 +139,7 @@ protected: bool d_storedUnitConflict; public: SatProof(::Minisat::Solver* solver, bool checkRes = false); - virtual ~SatProof() {} + virtual ~SatProof(); protected: void print(ClauseId id); void printRes(ClauseId id); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index eb7792d2c..3e4afc0c9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -864,6 +864,9 @@ SmtEngine::~SmtEngine() throw() { delete d_decisionEngine; d_decisionEngine = NULL; + PROOF(delete d_proofManager;); + PROOF(d_proofManager = NULL;); + delete d_stats; d_stats = NULL; delete d_statisticsRegistry; |