21 #ifndef _cvc3__sat__minisat_derivation_h_
22 #define _cvc3__sat__minisat_derivation_h_
42 typedef std::vector<std::pair<Lit, int> >
TSteps;
59 d_steps.push_back(std::make_pair(lit, clauseID));
63 add(lit, clause->
id());
135 "MiniSat::Derivation::registerClause: new clause of different size than old clause of same id");
138 for (
int i = 0; i < old->
size(); ++i) {
139 oldS.insert((*old)[i]);
142 for (
int i = 0; i < clause->
size(); ++i) {
144 "MiniSat::Derivation::registerClause: new clause not subset of old clause of same id");
145 oldS.erase((*clause)[i]);
148 "MiniSat::Derivation::registerClause: old clause not subset of new clause of same id");
163 FatalAssert(clause != NULL,
"MiniSat::derivation:removedClause: NULL");
170 "MiniSat::Derivation::registerInference: inference for clauseID already registered");
227 void push(
int clauseID);
230 void pop(
int clauseID);