d_idClause(),
d_clauseId(),
d_idUnit(),
+ d_unitId(),
d_deleted(),
d_inputClauses(),
d_lemmaClauses(),
{
d_proxy = new ProofProxy(this);
}
+SatProof::~SatProof() {
+ delete d_proxy;
+}
/**
* Returns true if the resolution chain corresponding to id
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";
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";