summaryrefslogtreecommitdiff
path: root/src/proof/sat_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/sat_proof.cpp')
-rw-r--r--src/proof/sat_proof.cpp466
1 files changed, 244 insertions, 222 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index da9df0d42..3b5509ffb 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -25,7 +25,7 @@ using namespace Minisat;
using namespace CVC4::prop;
namespace CVC4 {
-/// some helper functions
+/// some helper functions
void printLit (Minisat::Lit l) {
Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
@@ -33,16 +33,16 @@ void printLit (Minisat::Lit l) {
void printClause (Minisat::Clause& c) {
for (int i = 0; i < c.size(); i++) {
- Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
+ Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
}
}
void printLitSet(const LitSet& s) {
for(LitSet::iterator it = s.begin(); it != s.end(); ++it) {
printLit(*it);
- Debug("proof:sat") << " ";
+ Debug("proof:sat") << " ";
}
- Debug("proof:sat") << endl;
+ Debug("proof:sat") << endl;
}
// purely debugging functions
@@ -52,39 +52,38 @@ void printDebug (Minisat::Lit l) {
void printDebug (Minisat::Clause& c) {
for (int i = 0; i < c.size(); i++) {
- Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
+ Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
}
Debug("proof:sat") << endl;
}
-int SatProof::d_idCounter = 0;
+int SatProof::d_idCounter = 0;
-/**
+/**
* Converts the clause associated to id to a set of literals
- *
+ *
* @param id the clause id
- * @param set the clause converted to a set of literals
+ * @param set the clause converted to a set of literals
*/
void SatProof::createLitSet(ClauseId id, LitSet& set) {
- Assert (set.empty());
+ Assert(set.empty());
if(isUnit(id)) {
set.insert(getUnit(id));
return;
}
if ( id == d_emptyClauseId) {
- return;
+ return;
}
CRef ref = getClauseRef(id);
- Assert (ref != CRef_Undef);
- Clause& c = d_solver->ca[ref];
+ Clause& c = getClause(ref);
for (int i = 0; i < c.size(); i++) {
- set.insert(c[i]);
+ set.insert(c[i]);
}
}
-/**
+/**
* Resolves clause1 and clause2 on variable var and stores the
* result in clause1
* @param v
@@ -93,36 +92,40 @@ void SatProof::createLitSet(ClauseId id, LitSet& set) {
*/
bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) {
Assert(!clause1.empty());
- Assert(!clause2.empty());
- Lit var = sign(v) ? ~v : v;
+ Assert(!clause2.empty());
+ Lit var = sign(v) ? ~v : v;
if (s) {
// literal appears positive in the first clause
if( !clause2.count(~var)) {
- Debug("proof:sat") << "proof:resolve: Missing literal ";
- printLit(var);
- Debug("proof:sat") << endl;
- return false;
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "proof:resolve: Missing literal ";
+ printLit(var);
+ Debug("proof:sat") << endl;
+ }
+ return false;
}
clause1.erase(var);
clause2.erase(~var);
for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
- clause1.insert(*it);
+ clause1.insert(*it);
}
} else {
// literal appears negative in the first clause
if( !clause1.count(~var) || !clause2.count(var)) {
- Debug("proof:sat") << "proof:resolve: Missing literal ";
- printLit(var);
- Debug("proof:sat") << endl;
- return false;
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "proof:resolve: Missing literal ";
+ printLit(var);
+ Debug("proof:sat") << endl;
+ }
+ return false;
}
clause1.erase(~var);
clause2.erase(var);
for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
- clause1.insert(*it);
+ clause1.insert(*it);
}
}
- return true;
+ return true;
}
/// ResChain
@@ -135,16 +138,16 @@ ResChain::ResChain(ClauseId start) :
void ResChain::addStep(Lit lit, ClauseId id, bool sign) {
ResStep step(lit, id, sign);
- d_steps.push_back(step);
+ d_steps.push_back(step);
}
void ResChain::addRedundantLit(Lit lit) {
if (d_redundantLits) {
- d_redundantLits->insert(lit);
+ d_redundantLits->insert(lit);
} else {
d_redundantLits = new LitSet();
- d_redundantLits->insert(lit);
+ d_redundantLits->insert(lit);
}
}
@@ -156,7 +159,7 @@ ProofProxy::ProofProxy(SatProof* proof):
{}
void ProofProxy::updateCRef(CRef oldref, CRef newref) {
- d_proof->updateCRef(oldref, newref);
+ d_proof->updateCRef(oldref, newref);
}
@@ -183,27 +186,27 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
d_seenInput(),
d_seenLemmas()
{
- d_proxy = new ProofProxy(this);
+ d_proxy = new ProofProxy(this);
}
-/**
+/**
* Returns true if the resolution chain corresponding to id
* does resolve to the clause associated to id
- * @param id
- *
- * @return
+ * @param id
+ *
+ * @return
*/
bool SatProof::checkResolution(ClauseId id) {
if(d_checkRes) {
- bool validRes = true;
- Assert (d_resChains.find(id) != d_resChains.end());
+ bool validRes = true;
+ Assert(d_resChains.find(id) != d_resChains.end());
ResChain* res = d_resChains[id];
LitSet clause1;
createLitSet(res->getStart(), clause1);
- ResSteps& steps = res->getSteps();
+ ResSteps& steps = res->getSteps();
for (unsigned i = 0; i < steps.size(); i++) {
Lit var = steps[i].lit;
- LitSet clause2;
+ LitSet clause2;
createLitSet (steps[i].id, clause2);
bool res = resolve (var, clause1, clause2, steps[i].sign);
if(res == false) {
@@ -215,35 +218,38 @@ bool SatProof::checkResolution(ClauseId id) {
if (isUnit(id)) {
// special case if it was a unit clause
Lit unit = getUnit(id);
- validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
- return validRes;
+ validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
+ return validRes;
}
if (id == d_emptyClauseId) {
- return clause1.empty();
+ return clause1.empty();
}
CRef ref = getClauseRef(id);
- Assert (ref != CRef_Undef);
- Clause& c = d_solver->ca[ref];
+ Clause& c = getClause(ref);
for (int i = 0; i < c.size(); ++i) {
int count = clause1.erase(c[i]);
if (count == 0) {
- Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
- printLit(c[i]);
- Debug("proof:sat") << "\n";
- validRes = false;
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
+ printLit(c[i]);
+ Debug("proof:sat") << "\n";
+ }
+ validRes = false;
}
}
validRes = clause1.empty();
if (! validRes) {
- Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
- printLitSet(clause1);
- Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
- printClause(c);
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
+ printLitSet(clause1);
+ Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
+ printClause(c);
+ }
}
- return validRes;
-
+ return validRes;
+
} else {
- return true;
+ return true;
}
}
@@ -254,16 +260,16 @@ bool SatProof::checkResolution(ClauseId id) {
ClauseId SatProof::getClauseId(::Minisat::CRef ref) {
if(d_clauseId.find(ref) == d_clauseId.end()) {
- Debug("proof:sat") << "Missing clause \n";
+ Debug("proof:sat") << "Missing clause \n";
}
Assert(d_clauseId.find(ref) != d_clauseId.end());
- return d_clauseId[ref];
+ return d_clauseId[ref];
}
ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
- return d_unitId[toInt(lit)];
+ return d_unitId[toInt(lit)];
}
Minisat::CRef SatProof::getClauseRef(ClauseId id) {
@@ -273,79 +279,85 @@ Minisat::CRef SatProof::getClauseRef(ClauseId id) {
<< (isUnit(id)? "Unit" : "") << endl;
}
Assert(d_idClause.find(id) != d_idClause.end());
- return d_idClause[id];
+ return d_idClause[id];
}
Clause& SatProof::getClause(CRef ref) {
- return d_solver->ca[ref];
+ Assert(ref != CRef_Undef);
+ Assert(ref >= 0 && ref < d_solver->ca.size());
+ return d_solver->ca[ref];
}
+
Minisat::Lit SatProof::getUnit(ClauseId id) {
- Assert (d_idUnit.find(id) != d_idUnit.end());
- return d_idUnit[id];
+ Assert(d_idUnit.find(id) != d_idUnit.end());
+ return d_idUnit[id];
}
bool SatProof::isUnit(ClauseId id) {
- return d_idUnit.find(id) != d_idUnit.end();
+ return d_idUnit.find(id) != d_idUnit.end();
}
bool SatProof::isUnit(::Minisat::Lit lit) {
- return d_unitId.find(toInt(lit)) != d_unitId.end();
+ return d_unitId.find(toInt(lit)) != d_unitId.end();
}
ClauseId SatProof::getUnitId(::Minisat::Lit lit) {
- Assert(isUnit(lit));
- return d_unitId[toInt(lit)];
+ Assert(isUnit(lit));
+ return d_unitId[toInt(lit)];
}
bool SatProof::hasResolution(ClauseId id) {
- return d_resChains.find(id) != d_resChains.end();
+ return d_resChains.find(id) != d_resChains.end();
}
bool SatProof::isInputClause(ClauseId id) {
- return (d_inputClauses.find(id) != d_inputClauses.end());
+ return (d_inputClauses.find(id) != d_inputClauses.end());
}
bool SatProof::isLemmaClause(ClauseId id) {
- return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
+ return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
}
void SatProof::print(ClauseId id) {
if (d_deleted.find(id) != d_deleted.end()) {
- Debug("proof:sat") << "del"<<id;
+ Debug("proof:sat") << "del"<<id;
} else if (isUnit(id)) {
- printLit(getUnit(id));
+ printLit(getUnit(id));
} else if (id == d_emptyClauseId) {
- Debug("proof:sat") << "empty "<< endl;
+ Debug("proof:sat") << "empty "<< endl;
}
else {
- CRef ref = getClauseRef(id);
- Assert (ref != CRef_Undef);
- printClause(d_solver->ca[ref]);
+ CRef ref = getClauseRef(id);
+ printClause(getClause(ref));
}
}
void SatProof::printRes(ClauseId id) {
Assert(hasResolution(id));
Debug("proof:sat") << "id "<< id <<": ";
- printRes(d_resChains[id]);
+ printRes(d_resChains[id]);
}
void SatProof::printRes(ResChain* res) {
ClauseId start_id = res->getStart();
- Debug("proof:sat") << "(";
- print(start_id);
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "(";
+ print(start_id);
+ }
ResSteps& steps = res->getSteps();
for(unsigned i = 0; i < steps.size(); i++ ) {
Lit v = steps[i].lit;
ClauseId id = steps[i].id;
- Debug("proof:sat") << "[";
- printLit(v);
- Debug("proof:sat") << "] ";
- print(id);
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "[";
+ printLit(v);
+ Debug("proof:sat") << "] ";
+ print(id);
+ }
}
Debug("proof:sat") << ") \n";
}
@@ -353,23 +365,23 @@ void SatProof::printRes(ResChain* res) {
/// registration methods
ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
- Assert(clause != CRef_Undef);
+ Assert(clause != CRef_Undef);
ClauseIdMap::iterator it = d_clauseId.find(clause);
- if (it == d_clauseId.end()) {
- ClauseId newId = d_idCounter++;
- d_clauseId[clause]= newId;
- d_idClause[newId] =clause;
- if (kind == INPUT) {
- Assert (d_inputClauses.find(newId) == d_inputClauses.end());
- d_inputClauses.insert(newId);
- }
- if (kind == THEORY_LEMMA) {
- Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- d_lemmaClauses.insert(newId);
- }
- }
- Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
- return d_clauseId[clause];
+ if (it == d_clauseId.end()) {
+ ClauseId newId = d_idCounter++;
+ d_clauseId[clause] = newId;
+ d_idClause[newId] = clause;
+ if (kind == INPUT) {
+ Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+ d_inputClauses.insert(newId);
+ }
+ if (kind == THEORY_LEMMA) {
+ Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+ d_lemmaClauses.insert(newId);
+ }
+ }
+ Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
+ return d_clauseId[clause];
}
ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
@@ -377,44 +389,42 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
if (it == d_unitId.end()) {
ClauseId newId = d_idCounter++;
d_unitId[toInt(lit)] = newId;
- d_idUnit[newId] = lit;
+ d_idUnit[newId] = lit;
if (kind == INPUT) {
- Assert (d_inputClauses.find(newId) == d_inputClauses.end());
- d_inputClauses.insert(newId);
+ Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+ d_inputClauses.insert(newId);
}
if (kind == THEORY_LEMMA) {
- Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
- d_lemmaClauses.insert(newId);
+ Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+ d_lemmaClauses.insert(newId);
}
-
}
- Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
- return d_unitId[toInt(lit)];
+ Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
+ return d_unitId[toInt(lit)];
}
void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) {
// if we already added the literal return
if (seen.count(lit)) {
- return;
+ return;
}
CRef reason_ref = d_solver->reason(var(lit));
if (reason_ref == CRef_Undef) {
seen.insert(lit);
- removeStack.push_back(lit);
- return;
+ removeStack.push_back(lit);
+ return;
}
- Assert (reason_ref != CRef_Undef);
- int size = d_solver->ca[reason_ref].size();
+ int size = getClause(reason_ref).size();
for (int i = 1; i < size; i++ ) {
- Lit v = d_solver->ca[reason_ref][i];
+ Lit v = getClause(reason_ref)[i];
if(inClause.count(v) == 0 && seen.count(v) == 0) {
removedDfs(v, removedSet, removeStack, inClause, seen);
}
}
if(seen.count(lit) == 0) {
- seen.insert(lit);
+ seen.insert(lit);
removeStack.push_back(lit);
}
}
@@ -427,39 +437,41 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
}
LitSet inClause;
- createLitSet(id, inClause);
-
+ createLitSet(id, inClause);
+
LitVector removeStack;
- LitSet seen;
+ LitSet seen;
for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) {
- removedDfs(*it, removed, removeStack, inClause, seen);
+ removedDfs(*it, removed, removeStack, inClause, seen);
}
-
+
for (int i = removeStack.size()-1; i >= 0; --i) {
Lit lit = removeStack[i];
CRef reason_ref = d_solver->reason(var(lit));
- ClauseId reason_id;
+ ClauseId reason_id;
if (reason_ref == CRef_Undef) {
Assert(isUnit(~lit));
- reason_id = getUnitId(~lit);
+ reason_id = getUnitId(~lit);
} else {
reason_id = registerClause(reason_ref);
}
res->addStep(lit, reason_id, !sign(lit));
}
- removed->clear();
+ removed->clear();
}
void SatProof::registerResolution(ClauseId id, ResChain* res) {
Assert(res != NULL);
removeRedundantFromRes(res, id);
- Assert(res->redundantRemoved());
+ Assert(res->redundantRemoved());
d_resChains[id] = res;
- printRes(id);
- if (d_checkRes) {
+ if(Debug.isOn("proof:sat")) {
+ printRes(id);
+ }
+ if(d_checkRes) {
Assert(checkResolution(id));
}
}
@@ -468,48 +480,46 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) {
/// recording resolutions
void SatProof::startResChain(::Minisat::CRef start) {
- ClauseId id = getClauseId(start);
+ ClauseId id = getClauseId(start);
ResChain* res = new ResChain(id);
- d_resStack.push_back(res);
+ d_resStack.push_back(res);
}
void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
ClauseId id = registerClause(clause);
ResChain* res = d_resStack.back();
- res->addStep(lit, id, sign);
+ res->addStep(lit, id, sign);
}
void SatProof::endResChain(CRef clause) {
Assert(d_resStack.size() > 0);
- ClauseId id = registerClause(clause);
+ ClauseId id = registerClause(clause);
ResChain* res = d_resStack.back();
registerResolution(id, res);
- d_resStack.pop_back();
+ d_resStack.pop_back();
}
void SatProof::endResChain(::Minisat::Lit lit) {
Assert(d_resStack.size() > 0);
- ClauseId id = registerUnitClause(lit);
+ ClauseId id = registerUnitClause(lit);
ResChain* res = d_resStack.back();
-
-
registerResolution(id, res);
- d_resStack.pop_back();
+ d_resStack.pop_back();
}
void SatProof::storeLitRedundant(::Minisat::Lit lit) {
Assert(d_resStack.size() > 0);
ResChain* res = d_resStack.back();
- res->addRedundantLit(lit);
+ res->addRedundantLit(lit);
}
-/// constructing resolutions
+/// constructing resolutions
void SatProof::resolveOutUnit(::Minisat::Lit lit) {
ClauseId id = resolveUnit(~lit);
ResChain* res = d_resStack.back();
- res->addStep(lit, id, !sign(lit));
+ res->addStep(lit, id, !sign(lit));
}
void SatProof::storeUnitResolution(::Minisat::Lit lit) {
@@ -520,28 +530,30 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
// first check if we already have a resolution for lit
if(isUnit(lit)) {
ClauseId id = getClauseId(lit);
- if(hasResolution(id) || isInputClause(id)) {
- return id;
- }
- Assert (false);
+ Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id));
+ return id;
}
CRef reason_ref = d_solver->reason(var(lit));
- Assert (reason_ref != CRef_Undef);
-
- ClauseId reason_id = registerClause(reason_ref);
-
- ResChain* res = new ResChain(reason_id);
- Clause& reason = d_solver->ca[reason_ref];
- for (int i = 0; i < reason.size(); i++) {
- Lit l = reason[i];
- if(lit != l) {
+ Assert(reason_ref != CRef_Undef);
+
+ ClauseId reason_id = registerClause(reason_ref);
+
+ ResChain* res = new ResChain(reason_id);
+ // Here, the call to resolveUnit() can reallocate memory in the
+ // clause allocator. So reload reason ptr each time.
+ Clause* reason = &getClause(reason_ref);
+ for (int i = 0;
+ i < reason->size();
+ i++, reason = &getClause(reason_ref)) {
+ Lit l = (*reason)[i];
+ if(lit != l) {
ClauseId res_id = resolveUnit(~l);
res->addStep(l, res_id, !sign(l));
}
}
- ClauseId unit_id = registerUnitClause(lit);
+ ClauseId unit_id = registerUnitClause(lit);
registerResolution(unit_id, res);
- return unit_id;
+ return unit_id;
}
void SatProof::toStream(std::ostream& out) {
@@ -549,50 +561,62 @@ void SatProof::toStream(std::ostream& out) {
Unimplemented("native proof printing not supported yet");
}
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) {
- Assert (!d_storedUnitConflict);
- d_unitConflictId = registerUnitClause(conflict_lit);
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) {
+ Assert(!d_storedUnitConflict);
+ d_unitConflictId = registerUnitClause(conflict_lit, kind);
d_storedUnitConflict = true;
- Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n";
+ Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n";
}
void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
Assert(d_resStack.size() == 0);
- Assert (conflict_ref != ::Minisat::CRef_Undef);
- ClauseId conflict_id;
+ Assert(conflict_ref != ::Minisat::CRef_Undef);
+ ClauseId conflict_id;
if (conflict_ref == ::Minisat::CRef_Lazy) {
- Assert (d_storedUnitConflict);
- conflict_id = d_unitConflictId;
+ Assert(d_storedUnitConflict);
+ conflict_id = d_unitConflictId;
+
+ ResChain* res = new ResChain(conflict_id);
+ Lit lit = d_idUnit[conflict_id];
+ ClauseId res_id = resolveUnit(~lit);
+ res->addStep(lit, res_id, !sign(lit));
+
+ registerResolution(d_emptyClauseId, res);
+
+ return;
} else {
- Assert (!d_storedUnitConflict);
+ Assert(!d_storedUnitConflict);
conflict_id = registerClause(conflict_ref); //FIXME
}
- Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
- print(conflict_id);
-
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
+ print(conflict_id);
+ }
+
ResChain* res = new ResChain(conflict_id);
- Clause& conflict = d_solver->ca[conflict_ref] ;
- for (int i = 0; i < conflict.size(); ++i) {
- Lit lit = conflict[i];
+ // Here, the call to resolveUnit() can reallocate memory in the
+ // clause allocator. So reload conflict ptr each time.
+ Clause* conflict = &getClause(conflict_ref);
+ for (int i = 0;
+ i < conflict->size();
+ ++i, conflict = &getClause(conflict_ref)) {
+ Lit lit = (*conflict)[i];
ClauseId res_id = resolveUnit(~lit);
- res->addStep(lit, res_id, !sign(lit));
+ res->addStep(lit, res_id, !sign(lit));
}
registerResolution(d_emptyClauseId, res);
- // // FIXME: massive hack
- // Proof* proof = ProofManager::getProof();
- // proof->toStream(std::cout);
}
/// CRef manager
void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) {
if (d_clauseId.find(oldref) == d_clauseId.end()) {
- return;
+ return;
}
ClauseId id = getClauseId(oldref);
- Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end());
- Assert (d_temp_idClause.find(id) == d_temp_idClause.end());
+ Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end());
+ Assert(d_temp_idClause.find(id) == d_temp_idClause.end());
d_temp_clauseId[newref] = id;
d_temp_idClause[id] = newref;
}
@@ -602,39 +626,39 @@ void SatProof::finishUpdateCRef() {
d_temp_clauseId.clear();
d_idClause.swap(d_temp_idClause);
- d_temp_idClause.clear();
+ d_temp_idClause.clear();
}
void SatProof::markDeleted(CRef clause) {
if (d_clauseId.find(clause) != d_clauseId.end()) {
ClauseId id = getClauseId(clause);
- Assert (d_deleted.find(id) == d_deleted.end());
+ Assert(d_deleted.find(id) == d_deleted.end());
d_deleted.insert(id);
if (isLemmaClause(id)) {
const Clause& minisat_cl = getClause(clause);
- SatClause* sat_cl = new SatClause();
- MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);
- d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
+ SatClause* sat_cl = new SatClause();
+ MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);
+ d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
}
}
}
void SatProof::constructProof() {
- collectClauses(d_emptyClauseId);
+ collectClauses(d_emptyClauseId);
}
std::string SatProof::clauseName(ClauseId id) {
ostringstream os;
if (isInputClause(id)) {
- os << ProofManager::getInputClauseName(id);
- return os.str();
- } else
+ os << ProofManager::getInputClauseName(id);
+ return os.str();
+ } else
if (isLemmaClause(id)) {
- os << ProofManager::getLemmaClauseName(id);
- return os.str();
+ os << ProofManager::getLemmaClauseName(id);
+ return os.str();
}else {
os << ProofManager::getLearntClauseName(id);
- return os.str();
+ return os.str();
}
}
@@ -643,58 +667,56 @@ void SatProof::addToProofManager(ClauseId id, ClauseKind kind) {
Minisat::Lit lit = getUnit(id);
prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit);
prop::SatClause* clause = new SatClause();
- clause->push_back(sat_lit);
- ProofManager::currentPM()->addClause(id, clause, kind);
- return;
+ clause->push_back(sat_lit);
+ ProofManager::currentPM()->addClause(id, clause, kind);
+ return;
}
-
+
if (isDeleted(id)) {
- Assert (kind == THEORY_LEMMA);
+ Assert(kind == THEORY_LEMMA);
SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
- ProofManager::currentPM()->addClause(id, clause, kind);
- return;
+ ProofManager::currentPM()->addClause(id, clause, kind);
+ return;
}
-
+
CRef ref = getClauseRef(id);
const Clause& minisat_cl = getClause(ref);
SatClause* clause = new SatClause();
- MinisatSatSolver::toSatClause(minisat_cl, *clause);
- ProofManager::currentPM()->addClause(id, clause, kind);
+ MinisatSatSolver::toSatClause(minisat_cl, *clause);
+ ProofManager::currentPM()->addClause(id, clause, kind);
}
void SatProof::collectClauses(ClauseId id) {
if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
- return;
+ return;
}
if (d_seenInput.find(id) != d_seenInput.end()) {
- return;
+ return;
}
if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
- return;
+ return;
}
if (isInputClause(id)) {
- addToProofManager(id, INPUT);
+ addToProofManager(id, INPUT);
d_seenInput.insert(id);
- return;
- }
- else if (isLemmaClause(id)) {
- addToProofManager(id, THEORY_LEMMA);
+ return;
+ } else if (isLemmaClause(id)) {
+ addToProofManager(id, THEORY_LEMMA);
d_seenLemmas.insert(id);
- return;
- }
- else {
- d_seenLearnt.insert(id);
+ return;
+ } else {
+ d_seenLearnt.insert(id);
}
- Assert (d_resChains.find(id) != d_resChains.end());
+ Assert(d_resChains.find(id) != d_resChains.end());
ResChain* res = d_resChains[id];
ClauseId start = res->getStart();
collectClauses(start);
- ResSteps steps = res->getSteps();
- for(unsigned i = 0; i < steps.size(); i++) {
- collectClauses(steps[i].id);
+ ResSteps steps = res->getSteps();
+ for(size_t i = 0; i < steps.size(); i++) {
+ collectClauses(steps[i].id);
}
}
@@ -703,29 +725,29 @@ void SatProof::collectClauses(ClauseId id) {
void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
out << "(satlem_simplify _ _ _ ";
- ResChain* res = d_resChains[id];
+ ResChain* res = d_resChains[id];
ResSteps& steps = res->getSteps();
-
+
for (int i = steps.size()-1; i >= 0; i--) {
out << "(";
out << (steps[i].sign? "R" : "Q") << " _ _ ";
-
+
}
-
+
ClauseId start_id = res->getStart();
// WHY DID WE NEED THIS?
// if(isInputClause(start_id)) {
- // d_seenInput.insert(start_id);
+ // d_seenInput.insert(start_id);
// }
out << clauseName(start_id) << " ";
-
+
for(unsigned i = 0; i < steps.size(); i++) {
- out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
+ out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
}
-
+
if (id == d_emptyClauseId) {
out <<"(\\empty empty)";
- return;
+ return;
}
out << "(\\" << clauseName(id) << "\n"; // bind to lemma name
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback