ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
CaDiCaL::Proof Member List

This is the complete list of members for CaDiCaL::Proof, including all inherited members.

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::Proofinline
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