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());
133 Clause* old = d_clauses[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");
151 d_clauses[clause->
id()] = clause;
157 d_inputClauses.
insert(clauseID);
163 FatalAssert(clause != NULL,
"MiniSat::derivation:removedClause: NULL");
164 d_removedClauses.push_back(clause);
170 "MiniSat::Derivation::registerInference: inference for clauseID already registered");
172 d_inferences[clauseID] = inference;
227 void push(
int clauseID);
230 void pop(
int clauseID);
std::string toString() const
int computeRootReason(Lit implied, Solver *solver)
TInputClauses d_inputClauses
void registerInputClause(int clauseID)
void registerClause(Clause *clause)
void add(Lit lit, int clauseID)
Hash::hash_set< int > TInputClauses
bool contains(const key_type &key) const
status
SAT::SatProof * createProof()
void registerInference(int clauseID, Inference *inference)
#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)
Hash::hash_map< int, Inference * > TInferences
const TSteps & getSteps() const
std::pair< iterator, bool > insert(const value_type &entry)
void removedClause(Clause *clause)
std::deque< Clause * > d_removedClauses
void add(Lit lit, Clause *clause)
std::vector< std::pair< Lit, int > > TSteps
Hash::hash_map< int, Clause * > TClauses