Lines Matching defs:Proof
0 /*****************************************************************************************[Proof.C]
20 #include "Proof.h"
63 // Proof logging:
65 Proof::Proof()
75 Proof::Proof(ProofTraverser& t)
83 ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id)
109 void Proof::beginChain(ClauseId start)
118 void Proof::resolve(ClauseId next, Var x)
126 void Proof::resolve(ClauseId next, Lit p)
134 ClauseId Proof::endChain()
162 void Proof::deleted(ClauseId gone)
178 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) {
180 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp) {
219 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var,
222 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var,
255 void Proof::compress(Proof& dst, ClauseId goal)
340 bool Proof::save(cchar* filename)
364 void Proof::traverse(ProofTraverser& trav, int& res_count, ClauseId goal)