| add_assumption(int) | CaDiCaL::Proof | |
| add_assumption_clause(int64_t, const vector< int > &, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_assumption_clause(int64_t, int, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_constraint(const vector< int > &) | CaDiCaL::Proof | |
| add_derived_clause(Clause *c, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_derived_clause(int64_t, bool, const vector< int > &, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_derived_empty_clause(int64_t, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_derived_unit_clause(int64_t, int unit, const vector< int64_t > &) | CaDiCaL::Proof | |
| add_external_original_clause(int64_t, bool, const vector< int > &, bool restore=false) | CaDiCaL::Proof | |
| add_original_clause(int64_t, bool, const vector< int > &) | CaDiCaL::Proof | |
| begin_proof(int64_t) | CaDiCaL::Proof | |
| conclude_sat(const vector< int > &model) | CaDiCaL::Proof | |
| conclude_unknown(const vector< int > &trace) | CaDiCaL::Proof | |
| conclude_unsat(ConclusionType, const vector< int64_t > &) | CaDiCaL::Proof | |
| connect(Tracer *t) | CaDiCaL::Proof | inline |
| delete_clause(int64_t, bool, const vector< int > &) | CaDiCaL::Proof | |
| delete_clause(Clause *) | CaDiCaL::Proof | |
| delete_external_original_clause(int64_t, bool, const vector< int > &) | CaDiCaL::Proof | |
| delete_unit_clause(int64_t id, const int lit) | CaDiCaL::Proof | |
| disconnect(Tracer *t) | CaDiCaL::Proof | |
| finalize_clause(int64_t, const vector< int > &c) | CaDiCaL::Proof | |
| finalize_clause(Clause *) | CaDiCaL::Proof | |
| finalize_external_unit(int64_t, int) | CaDiCaL::Proof | |
| finalize_unit(int64_t, int) | CaDiCaL::Proof | |
| flush() | CaDiCaL::Proof | |
| flush_clause(Clause *) | CaDiCaL::Proof | |
| otfs_strengthen_clause(Clause *, const vector< int > &, const vector< int64_t > &) | CaDiCaL::Proof | |
| Proof(Internal *) | CaDiCaL::Proof | |
| report_status(int, int64_t) | CaDiCaL::Proof | |
| reset_assumptions() | CaDiCaL::Proof | |
| solve_query() | CaDiCaL::Proof | |
| strengthen(int64_t) | CaDiCaL::Proof | |
| strengthen_clause(Clause *, int, const vector< int64_t > &) | CaDiCaL::Proof | |
| weaken_minus(int64_t, const vector< int > &) | CaDiCaL::Proof | |
| weaken_minus(Clause *) | CaDiCaL::Proof | |
| weaken_plus(int64_t, const vector< int > &) | CaDiCaL::Proof | |
| weaken_plus(Clause *) | CaDiCaL::Proof | |
| ~Proof() | CaDiCaL::Proof | |