00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__sat__minisat_derivation_h_
00022 #define _cvc3__sat__minisat_derivation_h_
00023
00024
00025 #include "minisat_types.h"
00026 #include <hash_map.h>
00027 #include <hash_set.h>
00028 #include <vector>
00029 #include <deque>
00030 #include <algorithm>
00031 #include <string>
00032
00033 namespace MiniSat {
00034
00035 class Inference {
00036 public:
00037 typedef std::vector<std::pair<Lit, int> > TSteps;
00038
00039 private:
00040
00041 int d_start;
00042
00043
00044
00045
00046 TSteps d_steps;
00047
00048 public:
00049 Inference(int clauseID) : d_start(clauseID) {};
00050
00051 void add(Lit lit, int clauseID) {
00052 d_steps.push_back(std::make_pair(lit, clauseID));
00053 };
00054
00055 void add(Lit lit, Clause* clause) {
00056 add(lit, clause->id());
00057 };
00058
00059 int getStart() const {
00060 return d_start;
00061 }
00062
00063 const TSteps& getSteps() const {
00064 return d_steps;
00065 }
00066
00067
00068 std::string toString() const;
00069 };
00070
00071
00072
00073 class Solver;
00074
00075
00076
00077
00078
00079
00080
00081 class Derivation {
00082 public:
00083 typedef Hash::hash_map<int, Clause*> TClauses;
00084 typedef Hash::hash_set<int> TInputClauses;
00085 typedef Hash::hash_map<int, Inference*> TInferences;
00086
00087 private:
00088
00089 TClauses d_clauses;
00090
00091
00092
00093
00094
00095
00096 TInputClauses d_inputClauses;
00097
00098
00099
00100 TClauses d_unitClauses;
00101
00102
00103 TInferences d_inferences;
00104
00105
00106 std::deque<Clause*> d_removedClauses;
00107
00108
00109 Clause* d_emptyClause;
00110
00111 public:
00112 Derivation() : d_emptyClause(NULL) {};
00113 ~Derivation();
00114
00115
00116
00117
00118
00119
00120 void registerClause(Clause* clause) {
00121
00122
00123 IF_DEBUG (
00124 if (d_clauses.contains(clause->id())) {
00125 Clause* old = d_clauses[clause->id()];
00126 DebugAssert(old->size() == clause->size(),
00127 "MiniSat::Derivation::registerClause: two clauses of different size registered with same id");
00128
00129 std::vector<int> oldLiterals;
00130 for (int i = 0; i < old->size(); ++i) {
00131 oldLiterals.push_back((*old)[i].index());
00132 }
00133
00134 std::vector<int> newLiterals;
00135 for (int i = 0; i < clause->size(); ++i) {
00136 newLiterals.push_back((*clause)[i].index());
00137 }
00138
00139 std::sort(oldLiterals.begin(), oldLiterals.end());
00140 std::sort(newLiterals.begin(), newLiterals.end());
00141 for (std::vector<int>::size_type i = 0; i < oldLiterals.size(); ++i) {
00142 DebugAssert(oldLiterals[i] == newLiterals[i],
00143 "MiniSat::Derivation::registerClause: two clauses with different literals registered with same id");
00144 }
00145 }
00146 )
00147
00148 d_clauses[clause->id()] = clause;
00149 };
00150
00151
00152 void registerInputClause(int clauseID) {
00153 d_inputClauses.insert(clauseID);
00154 };
00155
00156
00157
00158 void removedClause(Clause* clause) {
00159 DebugAssert(clause != NULL, "MiniSat::derivation:removedClause: NULL");
00160 d_removedClauses.push_back(clause);
00161 };
00162
00163
00164 void registerInference(int clauseID, Inference* inference) {
00165 DebugAssert(!d_inferences.contains(clauseID),
00166 "MiniSat::Derivation::registerInference: inference for clauseID already registered");
00167 d_inferences[clauseID] = inference;
00168 };
00169
00170
00171
00172
00173
00174
00175
00176
00177 int computeRootReason(Lit implied, Solver* solver);
00178
00179
00180
00181
00182
00183
00184
00185 void finish(Clause* clause, Solver* solver);
00186
00187
00188
00189
00190
00191
00192
00193
00194
00195
00196
00197
00198
00199
00200
00201
00202
00203
00204
00205
00206
00207
00208
00209 void printProof(Clause* clause);
00210
00211
00212 void printProof();
00213
00214
00215 void push(int clauseID);
00216
00217
00218 void pop(int clauseID);
00219 };
00220 }
00221
00222
00223 #endif