34 for (Inference::TSteps::const_iterator step = d_steps.begin(); step != d_steps.end(); ++step) {
35 buffer <<
" " << step->first.toString() <<
" " << step->second;
51 for (std::deque<Clause*>::iterator i = d_removedClauses.begin(); i != d_removedClauses.end(); ++i) {
66 "MiniSat::Derivation::computeRootReason: implied reason not registered");
68 "MiniSat::Derivation::computeRootReason: implied reason not same as registered");
69 FatalAssert(reason != NULL,
"MiniSat::Derivation::computeRootReason: implied reason is NULL");
71 FatalAssert((*reason)[0] == implied,
"MiniSat::Derivation::computeRootReason: implied is not in its reason");
74 "MiniSat::Derivation::computeRootReason: literal not implied (TRUE)");
75 for (
int i = 1; i < reason->
size(); ++i) {
77 "MiniSat::Derivation::computeRootReason: literal not implied (FALSE)");
82 if (reason->
size() == 1) {
88 if (iter != d_unitClauses.end()) {
89 return iter->second->id();
95 for (
int i = 1; i < reason->
size(); ++i) {
96 Lit lit((*reason)[i]);
97 inference->
add(lit, computeRootReason(~lit, solver));
102 vector<Lit> literals;
103 literals.push_back(implied);
106 d_unitClauses[implied.
index()] = unit;
108 registerClause(unit);
109 registerInference(unit->
id(), inference);
116 FatalAssert(clause != NULL,
"MiniSat::derivation:finish:");
119 if (clause->
size() == 0) {
120 d_emptyClause = clause;
125 for (
int i = 0; i < clause->
size(); ++i) {
126 Lit lit((*clause)[i]);
127 inference->
add(lit, computeRootReason(~lit, solver));
129 vector<Lit> literals;
131 removedClause(empty);
132 d_emptyClause = empty;
133 registerClause(empty);
134 registerInference(empty->
id(), inference);
137 checkDerivation(clause);
153 std::set<int> relevant;
154 std::set<int> regress;
156 regress.insert(clause->
id());
157 while (!regress.empty()) {
159 int clauseID = *(regress.rbegin());
160 regress.erase(clauseID);
163 FatalAssert(relevant.count(clauseID) == 0,
"Solver::printProof: already in relevant");
164 relevant.insert(clauseID);
169 if (iter == d_inferences.end()) {
171 "Solver::printProof: clause without antecedents is not marked as input clause");
176 regress.insert(inference->
getStart());
178 for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
179 regress.insert(step->second);
186 for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
189 "MiniSat::Derivation::printProof: clause id in proof is not in clauses");
190 Clause* clause = d_clauses.find(clauseID)->second;
194 if (j != d_inferences.end()) {
195 inference = j->second;
198 FatalAssert(inference != NULL || d_inputClauses.contains(clauseID),
199 "MiniSat::Derivation::printProof: derivation of input clause");
200 FatalAssert(inference == NULL || !d_inputClauses.contains(clauseID),
201 "MiniSat::Derivation::printProof: no derivation for derived clause");
203 if (inference != NULL) {
206 "MiniSat::Derivation::printProof: first not in clauses");
212 for (
int i = 0; i < first->size(); ++i) {
213 derived.insert((*first)[i]);
217 for (Inference::TSteps::const_iterator step = inference->
getSteps().begin();
218 step != inference->
getSteps().end(); ++step) {
219 Lit lit = step->first;
223 FatalAssert(d_clauses.find(step->second) != d_clauses.end(),
224 "MiniSat::Derivation::printProof: next not in clauses");
225 Clause* next = d_clauses.find(step->second)->second;
228 "MiniSat::Derivation::printProof: lit not in derived");
230 "MiniSat::Derivation::printProof: ~lit not in next");
233 for (
int i = 0; i < next->size(); ++i) {
234 if ((*next)[i] != ~lit) {
235 derived.insert((*next)[i]);
241 for (
int i = 0; i < clause->size(); ++i) {
242 FatalAssert(derived.find((*clause)[i]) != derived.end(),
243 "MiniSat::Derivation::printProof: didn't derive expected clause");
244 derived.erase((*clause)[i]);
247 "MiniSat::Derivation::printProof: didn't derive expected clause 2");
254 FatalAssert(d_emptyClause != NULL,
"MiniSat::Derivation:createProof: no empty clause");
256 "MiniSat::Derivation:createProof: empty clause is not empty");
257 return createProof(d_emptyClause);
261 checkDerivation(clause);
268 std::set<int> relevant;
269 std::set<int> regress;
270 regress.insert(clause->
id());
271 while (!regress.empty()) {
273 int clauseID = *(regress.rbegin());
274 regress.erase(clauseID);
275 relevant.insert(clauseID);
280 if (iter != d_inferences.end()) {
282 regress.insert(inference->
getStart());
284 for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
285 regress.insert(step->second);
294 for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
296 Clause* clause = d_clauses.find(clauseID)->second;
300 if (j == d_inferences.end()) {
319 inference = j->second;
323 for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
328 proofNodes[clause->
id()] =
left;
331 proof->
setRoot(proofNodes[clause->
id()]);
337 FatalAssert(d_emptyClause != NULL,
"MiniSat::Derivation:printDerivation: no empty clause");
339 "MiniSat::Derivation:printDerivation: empty clause is not empty");
340 printDerivation(d_emptyClause);
350 std::set<int> relevant;
351 std::set<int> regress;
353 regress.insert(clause->
id());
354 while (!regress.empty()) {
356 int clauseID = *(regress.rbegin());
357 regress.erase(clauseID);
360 relevant.insert(clauseID);
365 if (iter != d_inferences.end()) {
367 regress.insert(inference->
getStart());
369 for (Inference::TSteps::const_iterator step = steps.begin(); step != steps.end(); ++step) {
370 regress.insert(step->second);
377 for (std::set<int>::iterator i = relevant.begin(); i != relevant.end(); ++i) {
379 Clause* clause = d_clauses.find(clauseID)->second;
383 if (j != d_inferences.end()) {
384 inference = j->second;
390 if (d_inputClauses.contains(clauseID)) {
395 cout <<
": " << clause->
toString() <<
" : ";
396 if (inference != NULL) cout << inference->
toString();
410 while (i != d_clauses.end()) {
411 Clause* clause = (*i).second;
421 clause->
pushID() > clauseID) {
422 int id = clause->
id();
424 d_inputClauses.erase(
id);
425 d_inferences.erase(
id);
427 if (clause->
size() == 1) {
428 int index = (*clause)[0].index();
429 if (d_unitClauses.contains(index) && d_unitClauses[index] == clause) {
430 d_unitClauses.erase(index);
431 FatalAssert(!d_unitClauses.contains(index),
"AHA");
435 i = d_clauses.erase(i);
443 if (d_emptyClause != NULL && d_emptyClause->pushID() > clauseID)
444 d_emptyClause = NULL;
447 std::deque<Clause*>::iterator j = d_removedClauses.begin();
448 while (j != d_removedClauses.end()) {
449 if ((*j)->pushID() > clauseID) {
451 j = d_removedClauses.erase(j);
_hash_table::iterator iterator
std::string toString() const
Clause * getReason(Var var) const
std::string toString() const
int computeRootReason(Lit implied, Solver *solver)
static void xfree(T *ptr)
_hash_table::const_iterator const_iterator
void add(Lit lit, int clauseID)
iterator find(const key_type &key)
operations
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool contains(const key_type &key) const
status
Sat solver proof representation.
CVC3::Theorem getTheorem() const
Clause * Clause_new(const vector< Lit > &ps, CVC3::Theorem theorem, int id)
SAT::SatProof * createProof()
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
void finish(Clause *clause, Solver *solver)
void checkDerivation(Clause *clause)
SAT::Var miniSatToCVC(Var var)
const TSteps & getSteps() const
void setRoot(SatProofNode *root)
SatProofNode * registerNode(SatProofNode *left, SatProofNode *right, SAT::Lit l)
static Clause * Decision()
SatProofNode * registerLeaf(CVC3::Theorem theorem)
std::vector< std::pair< Lit, int > > TSteps
Adaptation of MiniSat to DPLL(T)
lbool getValue(Var x) const
clauses / assignment